Hi 游客

更多精彩,请登录!

比特池塘 Chain Develop 正文
Open Zeppelin’s ERC-20 reference implementation is widely used in Web3. A bug in it would be devastating for the many contracts that derive from it. But how do we know that it is correct? And how do we know contracts that derive from it do so correctly and do not introduce bugs?
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
BitMere.com 比特池塘系信息发布平台,比特池塘仅提供信息存储空间服务。
声明:该文观点仅代表作者本人,本文不代表比特池塘立场,且不构成建议,请谨慎对待。
您需要登录后才可以回帖 登录 | 立即注册

本版积分规则

成为第一个吐槽的人

HuoBi 小学生
  • 粉丝

    0

  • 关注

    0

  • 主题

    1