JPYC.updateMinterAdmin

名称・種別

名称: JPYC.updateMinterAdmin
種別: def
モジュール: JpycFormalVerification.AccessControl
ソース: JpycFormalVerification/AccessControl.lean:203-208
概要: updateMinterAdmin(newMinterAdmin)：minterAdmin ロールを付け替える関数（owner 限定）。
仕様: 対象外

型シグネチャ

lean

JPYC.State → JPYC.CallContext → JPYC.Address → Except JPYC.Error JPYC.State

State・CallContext・新管理者 newMinterAdmin を受け取り、オーナーだけがミンター管理者を交代させる関数です。

和訳 docstring

ミンター管理者を newMinterAdmin に交代する（v2/FiatTokenV2.sol:356-363）。

解説

何を述べているか。 FiatTokenV2.updateMinterAdmin です。onlyOwner を要求し、newMinterAdmin ≠ address(0) を確かめてから、minterAdmin を書き換えます。

直感。 「誰がミンターを登録・削除できるか」という管理者を、オーナーが付け替えます。

なぜ安全性に効くか。 発行権限の 管理者 の交代を、さらに上位のオーナー権限に限定します。これにより「ミンター ⊂ minterAdmin ⊂ owner」という二段の権限階層ができ、鍵漏洩時の封じ込めが容易になります。権限は updateMinterAdmin_auth が保証します。

図解

Lean ソースコード

lean

/-- `updateMinterAdmin(newMinterAdmin)` — `v2/FiatTokenV2.sol:356-363`. -/
def updateMinterAdmin (s : State) (ctx : CallContext) (newMinterAdmin : Address) :
    Except Error State := do
  onlyOwner s ctx
  req (newMinterAdmin ≠ Address.zero) .newMinterAdminZero
  pure (s.setMinterAdmin newMinterAdmin)

対応 Solidity ソースコード

reference/JPYCv2/contracts/v2/FiatTokenV2.sol:356-363

solidity

function updateMinterAdmin(address _newMinterAdmin) external onlyOwner {
    require(
        _newMinterAdmin != address(0),
        "FiatToken: new minterAdmin is the zero address"
    );
    minterAdmin = _newMinterAdmin;
    emit MinterAdminChanged(minterAdmin);
}

JPYC.updateMinterAdmin ​

名称・種別 ​

型シグネチャ ​

和訳 docstring ​

解説 ​

図解 ​

Lean ソースコード ​

対応 Solidity ソースコード ​

依存 ​