Formally Verifying OpenZeppelin’s ERC-20 Implementation
HuoBi
发表于 2023-2-23 16:14:03
382
0
0
In Part One of this series on formal verification, we explained how CertiK uses formal verification to mathematically prove the correctness of ERC-20 contracts that we audit. Let’s dive in and see what happens when we apply it to OpenZeppelin’s code.In Part One of this series on formal verification, we explained how CertiK uses formal verification to mathematically prove the correctness of ERC-20 contracts that we audit. Let’s dive in and see what happens when we apply it to OpenZeppelin’s code.
ERC-20 Standard PropertiesAt CertiK, we have written property templates that precisely describe the expected behaviors of ERC-20 token contracts. These templates are generic: our tools analyze the implementation details of each smart contract and adapt the templates accordingly. We have 38 property templates.
Let's look at some of the properties that we regularly verify on incoming ERC-20 token contracts. For the sake of readability, the formulas that follow are slightly simplified and omit some technical details that do not contribute to the overall understanding of the approach. CertiK's audit reports contain an appendix that reproduces the formulas that have been used during model checking. A list with all the formulas used in our ERC-20 verification approach is publicly available here.
The transferFrom() function in ERC-20 contracts requires special attention, as it needs to distinguish between the initiator of the transaction (the address is msg.sender), the accounts that spend and receive tokens, and because it needs to observe the limits imposed by the entries in _balances and _allowances.
Specifying Correct Allowance UpdatesWhen transferFrom() succeeds, it must deduct the amount of tokens that have been transferred from the allowance that the sender has over the spender's account. However, many ERC-20 token contracts also allow the token owner to grant infinite allowance to another account. This is reflected by setting that account's allowance to the maximum value, i.e. to ((2^256)-1). Taking that exception into account, a correct allowance update can be specified by the following LTL formula
成为第一个吐槽的人