Smart contracts are distributed, self-enforcing programs executing on top of blockchain networks. They have the potential to revolutionize many industries such as financial institutes and supply chains. However, smart contracts are subject to code-based vulnerabilities, which casts a shadow on its applications. As smart contracts are unpatchable (due to the immutability of blockchain), it is essential that smart contracts are guaranteed to be free of vulnerabilities. Unfortunately, smart contract languages such as Solidity are Turing-complete, which implies that verifying them statically is infeasible. Thus, alternative approaches must be developed to provide the guarantee. In this work, we develop an approach which automatically transforms smart contracts so that they are provably free of 4 common kinds of vulnerabilities. The key idea is to apply runtime verification in an efficient and provably correct manner. Experiment results with 5000 smart contracts show that our approach incurs minor run-time overhead in terms of time (i.e., 14.79%) and gas (i.e., 0.79%).
翻译:智能合同是分布式的,可以自我强化,在连锁网络上实施智能合同。它们有可能使金融机构和供应链等许多行业发生革命性变革。然而,智能合同受制于基于代码的弱点,给其应用蒙上阴影。智能合同是无法实现的(由于连锁合同的不可移动性),保证智能合同不受脆弱性影响至关重要。不幸的是,Solidity等智能合同语言是图灵-完整的,这意味着静态核查是行不通的。因此,必须制定替代方法来提供担保。在这项工作中,我们开发一种自动转换智能合同的方法,以便它们能够不受四种常见的弱点的影响。关键的想法是以高效和准确的方式应用运行时间核查。以5000个智能合同的实验结果显示,我们的方法在时间(即14.79%)和气体(即0.79%)方面需要少量运行时的间接费用。