Smart contracts written in Solidity are programs used in blockchain networks, such as Etherium, for performing transactions. However, as with any piece of software, they are prone to errors and may present vulnerabilities, which malicious attackers could then use. This paper proposes a solidity frontend for the efficient SMT-based context-bounded model checker (ESBMC), named ESBMC-Solidity, which provides a way of verifying such contracts with its framework. A benchmark suite with vulnerable smart contracts was also developed for evaluation and comparison with other verification tools. The experiments performed here showed that ESBMC-Solidity detected all vulnerabilities, was the fastest tool, and provided a counterexample for each benchmark. A demonstration is available at https://youtu.be/3UH8_1QAVN0.
翻译:以 " 团结 " 书写的智能合同是用于诸如Etherium等链链式网络进行交易的程序,然而,与任何软件一样,它们容易出错,并可能造成脆弱性,恶意攻击者然后可以使用。本文件建议为高效的SMT基于背景的模型核对器(ESBMC)提供一个坚实的前端,名为ESBMC-Solidity,它提供了使用其框架核实此类合同的方法。还开发了一个带有脆弱智能合同的基准套件,用于与其他核查工具进行评价和比较。在这里进行的实验表明,ESBMC-团结性检测了所有脆弱性,是最快的工具,为每个基准提供了对应示例。在https://youtu.be/3UH8_QAVN0上可以找到一个演示。