JPYCv2 形式検証

外観

JPYC.receiveWithAuthorization ​

名称・種別 ​

  • 名称: JPYC.receiveWithAuthorization
  • 種別: def
  • モジュール: JpycFormalVerification.Signatures
  • ソース: JpycFormalVerification/Signatures.lean:181-189
  • 概要: receiveWithAuthorization(...)：受取人自身が呼ぶ必要のある EIP-3009 送金関数。
  • 仕様: 対象外

型シグネチャ ​

lean
JPYC.SigOracle → JPYC.State → JPYC.CallContext → JPYC.Address → JPYC.Address → JPYC.U256 → JPYC.U256 → JPYC.U256 → JPYC.Bytes32 → JPYC.U8 → JPYC.Bytes32 → JPYC.Bytes32 → Except JPYC.Error JPYC.State

EIP-3009 の receiveWithAuthorization 関数です。transferWithAuthorization に 受取人チェック（to == msg.sender）を加えたもので、フロントランニングを防ぎます。署名オラクル O の下で定義されます。

和訳 docstring ​

receiveWithAuthorization(...) ― 受取人チェック（to == msg.sender）付きの署名送金（v2/FiatTokenV2.sol:489-517）。

解説 ​

何を述べているか。 receiveWithAuthorization(...)（v2/FiatTokenV2.sol:489-517）の写しです。modifier ガードと内部処理は transferWithAuthorization とほぼ同じですが、内部 _receiveWithAuthorization の 先頭に require(to == msg.sender) が追加されています（破れると callerMustBePayee で revert）。その後は有効性検査・署名検証・使用済みマーク・_transfer と続きます。

直感。 「受け取る本人だけが、自分宛ての署名付き送金を実行できる」操作です。transferWithAuthorization は誰でも実行できるため、攻撃者が他人の署名を先回りして別の文脈で実行する余地がありますが、receiveWithAuthorization は「実行者＝受取人」を強制することでそれを封じます。

なぜ安全性に効くか。 receiveWithAuthorization_payee（成功 ⇒ to == msg.sender）として、この フロントランニング対策ガード が定理化されています。これに加え、transferWithAuthorization と同じ一回限り性・有効期間・署名者・供給保存の保証をすべて持ちます。

図解 ​

Lean ソースコード ​

lean
/-- `receiveWithAuthorization(…)` — `v2/FiatTokenV2.sol:489-517`. -/
def receiveWithAuthorization (s : State) (ctx : CallContext) (frm dst : Address)
    (value validAfter validBefore : U256) (nonce : Bytes32) (v : U8) (r sig : Bytes32) :
    Except Error State := do
  whenNotPaused s
  notBlocklisted s frm
  notBlocklisted s dst
  checkAllowlist s frm value
  _receiveWithAuthorization O s ctx frm dst value validAfter validBefore nonce v r sig

対応 Solidity ソースコード ​

reference/JPYCv2/contracts/v2/FiatTokenV2.sol:489-517

solidity
function receiveWithAuthorization(
    address from, address to, uint256 value,
    uint256 validAfter, uint256 validBefore, bytes32 nonce,
    uint8 v, bytes32 r, bytes32 s
)
    external
    whenNotPaused
    notBlocklisted(from)
    notBlocklisted(to)
    checkAllowlist(from, value)
{
    _receiveWithAuthorization(
        from, to, value, validAfter, validBefore, nonce, v, r, s);
}

依存 ​