Theorem-Carrying-Transaction: Runtime Certification to Ensure Safety for Smart Contract Transactions
<|reference_start|>Theorem-Carrying-Transaction: Runtime Certification to Ensure Safety for Smart Contract Transactions: 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 reference-topology between the contracts. Can the Ethereum community be assured that this gigantic program conforms to its design-level safety properties, despite unforeseeable code-level intricacies? Static code verification is inadequate due to the program's gigantic scale and high polymorphism. In this paper, we present a viable technological roadmap for the community toward this ambitious goal. Our technology, called Theorem-Carrying-Transaction (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 property is specified in a contract, it can be treated confidently as an unconditional guarantee made by the contract. As case studies, we demonstrate that TCT secures token contracts without foreseeing code-level intricacies like integer overflow and reentrancy. TCT is also successfully applied to a Uniswap codebase, showcasing a complex decentralized finance (DeFi) scenario. Our prototype incurs a negligible runtime overhead, two orders of magnitude lower than a state-of-the-art approach.<|reference_end|>
@article{bjørner2024theorem-carrying-transaction:,
    title={Theorem-Carrying-Transaction: Runtime Certification to Ensure Safety for
  Smart Contract Transactions},
    author={Nikolaj S. Bj{o}rner (1), Ashley J. Chen (2), Shuo Chen (1), Yang
  Chen (1), Zhongxin Guo (1), Tzu-Han Hsu (3), Peng Liu (4), Nanqing Luo (4)
  ((1) Microsoft Research, (2) New York University Shanghai, (3) Michigan State
  University, (4) Pennsylvania State University)},
    journal={arXiv preprint arXiv:2408.06478},
    year={2024},
    archivePrefix={arXiv},
    eprint={2408.06478},
    primaryClass={cs.CR cs.PL}
}