Theorem-Carrying Transactions: Runtime Verification to Ensure Interface Specifications for Smart Contract Safety

TL;DR

This paper introduces Theorem-Carrying Transactions (TCT), a runtime verification method for smart contracts that ensures safety specifications are met with minimal overhead by carrying and verifying theorems with each transaction.

Contribution

The paper proposes TCT, a novel approach combining concrete execution and symbolic proofs to verify smart contract safety at runtime efficiently.

Findings

TCT secures token contracts against common vulnerabilities.

TCT applied successfully to complex DeFi codebase.

Runtime overhead is negligible, much lower than existing methods.

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.