Theorem-Carrying Transactions: Runtime Verification to Ensure Interface Specifications for Smart Contract Safety
Abstract
Security bugs and trapdoors in smart contracts have been impacting the Ethereum community since its inception. Conceptually, the 1.45-million Ethereum's contracts form a single "gigantic program" whose behaviors are determined by the complex compositions of contracts. Can programmers be assured that this gigantic program conforms to high-level safety specifications, despite unforeseeable code-level intricacies? Static code verification cannot be faithful to this gigantic program due to its scale and high polymorphism. In this paper, we present a viable approach to achieve this goal. Our technology, called Theorem-Carrying Transactions (TCT), combines the benefits of concrete execution and symbolic proofs. Under the TCT protocol, every transaction carries a theorem that proves its adherence to the specified properties in the invoked contracts, and the runtime system checks the theorem before executing the transaction. Once a theorem is proven, it will be reused for future transactions, so TCT's runtime overhead is minimal. As case studies, we demonstrate that TCT secures token contracts without foreseeing code-level intricacies, such as integer overflow and reentrancy. TCT is also successfully applied to a Uniswap codebase, showcasing a complex decentralized finance (DeFi) scenario. Our evaluation shows a negligible runtime overhead, two orders of magnitude lower than a state-of-the-art approach for runtime checking of contract code safety.
Keywords
Cite
@article{arxiv.2408.06478,
title = {Theorem-Carrying Transactions: Runtime Verification to Ensure Interface Specifications for Smart Contract Safety},
author = {Thomas Ball and Nikolaj S. Bjørner and Ashley J. Chen and Shuo Chen and Yang Chen and Zhongxin Guo and Tzu-Han Hsu and Peng Liu and Nanqing Luo},
journal= {arXiv preprint arXiv:2408.06478},
year = {2025}
}