eThor Provides Security for Smart Contracts
In their breakthrough work, a team at the research unit Security & Privacy developed sound static analysis for Ethereum smart contracts.
Ethereum has emerged as the most popular smart contract development platform, with hundreds of thousands of contracts stored on the blockchain and covering a variety of application scenarios, such as auctions, trading platforms, and so on. Given their financial nature, security vulnerabilities may lead to catastrophic consequences, and, even worse, they can be hardly fixed as data stored on the blockchain, including the smart contract code itself, are immutable. An automated security analysis of these contracts is thus of utmost interest, but at the same time technically challenging for a variety of reasons, such as the specific transaction-oriented programming mechanisms, which feature a subtle semantics, and the fact that the blockchain data which the contract under analysis interacts with, including the code of callers and callees, are not statically known.
In their work, Clara Schneidewind, Ilya Grishchenko, Markus Scherer, and Matteo Maffei present eThor, the first sound and automated static analyzer for EVM bytecode, which is based on an abstraction of the EVM bytecode semantics based on Horn clauses. In particular, their static analysis supports reachability properties, which they show to be sufficient for capturing interesting security properties for smart contracts (e.g., single-entrancy) as well as contract-specific functional properties. The team’s analysis is proven sound against a complete semantics of EVM bytecode and experimental large-scale evaluation on real-world contracts demonstrates that eThor is practical and outperforms the state-of-the-art static analyzers: specifically, eThor is the only one to provide soundness guarantees, terminates on 95% of a representative set of real-world contracts, and achieves an F-measure (which combines sensitivity and specificity) of 89%.
Resources
- Paper “eThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts”
- Research Unit Security & Privacy
Contact
Curious about our other news? Subscribe to our news feed, calendar, or newsletter, or follow us on social media.