Smart Contract Defense through Bytecode Rewriting

An Ethereum bytecode rewriting and validation architecture is proposed and evaluated for securing smart contracts in decentralized cryptocurrency systems without access to contract source code. This addresses a wave of smart contract vulnerabilities that have been exploited by cybercriminals in recent years to steal millions of dollars from victims. Such attacks have motivated various best practices proposals for helping developers write safer contracts; but as the number of programming languages used to develop smart contracts increases, implementing these best practices can be cumbersome and hard to enforce across the development tool chain. Automated hardening at the bytecode level bypasses this source-level heterogeneity to enforce safety and code integrity properties of contracts independently of the sources whence they were derived. In addition, a binary code verification tool implemented atop the Coq interactive theorem prover establishes input-output equivalence between the original code and the modified code. Evaluation demonstrates that the system can enforce policies that protect against integer overflow and underflow vulnerabilities in real Ethereum contract bytecode, and overhead is measured in terms of instruction counts.