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

• URL: http://arxiv.org/abs/2408.06478v2
• Date: Wed, 06 Aug 2025 22:31:48 GMT
• Title: Theorem-Carrying Transactions: Runtime Verification to Ensure Interface Specifications for Smart Contract Safety
• Authors: Thomas Ball, Nikolaj S. Bjørner, Ashley J. Chen, Shuo Chen, Yang Chen, Zhongxin Guo, Tzu-Han Hsu, Peng Liu, Nanqing Luo,
• Abstract summary: 1.45-million contracts form a single "gigantic program"<n>Can programmers be assured that this gigantic program conforms to high-level safety specifications?<n> Static code verification cannot be faithful to this gigantic program due to its scale and high polymorphism.<n>Our technology, called Theorem-Carrying Transactions (TCT), combines the benefits of concrete execution and symbolic proofs.
• Score: 8.906268052552582
• License: http://creativecommons.org/licenses/by/4.0/
• 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.

Related papers

• Proof of Trusted Execution: A Consensus Paradigm for Deterministic Blockchain Finality [0.391985484065646]
  We propose Proof of Trusted Execution (PoTE), a consensus paradigm where agreement emerges from verifiable execution rather than replicated re-execution.<n>Because the execution is deterministic and the proposer is uniquely derived from public randomness, PoTE avoids forks, eliminates slot.time bottlenecks, and commits blocks in a single round of verification.
  arXiv  Detail & Related papers  (2025-12-10T08:04:38Z)
• Trace: Securing Smart Contract Repository Against Access Control Vulnerability [58.02691083789239]
  GitHub hosts numerous smart contract repositories containing source code, documentation, and configuration files.<n>Third-party developers often reference, reuse, or fork code from these repositories during custom development.<n>Existing tools for detecting smart contract vulnerabilities are limited in their ability to handle complex repositories.
  arXiv  Detail & Related papers  (2025-10-22T05:18:28Z)
• SIM-CoT: Supervised Implicit Chain-of-Thought [108.30049193668083]
  Implicit Chain-of-Thought (CoT) methods offer a token-efficient alternative to explicit CoT reasoning in Large Language Models.<n>We identify a core latent instability issue when scaling the computational budget of implicit CoT.<n>We propose SIM-CoT, a plug-and-play training module that introduces step-level supervision to stabilize and enrich the latent reasoning space.
  arXiv  Detail & Related papers  (2025-09-24T17:01:32Z)
• Decompiling Smart Contracts with a Large Language Model [51.49197239479266]
  Despite Etherscan's 78,047,845 smart contracts deployed on (as of May 26, 2025), a mere 767,520 ( 1%) are open source.<n>This opacity necessitates the automated semantic analysis of on-chain smart contract bytecode.<n>We introduce a pioneering decompilation pipeline that transforms bytecode into human-readable and semantically faithful Solidity code.
  arXiv  Detail & Related papers  (2025-06-24T13:42:59Z)
• SolBench: A Dataset and Benchmark for Evaluating Functional Correctness in Solidity Code Completion and Repair [51.0686873716938]
  We introduce SolBench, a benchmark for evaluating the functional correctness of Solidity smart contracts generated by code completion models. We propose a Retrieval-Augmented Code Repair framework to verify functional correctness of smart contracts. Results show that code repair and retrieval techniques effectively enhance the correctness of smart contract completion while reducing computational costs.
  arXiv  Detail & Related papers  (2025-03-03T01:55:20Z)
• Effective Targeted Testing of Smart Contracts [0.0]
  Since smart contracts are immutable, their bugs cannot be fixed, which may lead to significant monetary losses. Our framework, Griffin, tackles this deficiency by employing a targeted symbolic execution technique for generating test data. This paper discusses how smart contracts differ from legacy software in targeted symbolic execution and how these differences can affect the tool structure.
  arXiv  Detail & Related papers  (2024-07-05T04:38:11Z)
• Scalable UTXO Smart Contracts via Fine-Grained Distributed State [0.8192907805418581]
  UTXO-based smart contract platforms face an efficiency bottleneck. Any transaction sent to a contract must specify the entire updated contract state. We propose a technique to efficiently execute smart contracts on an extended UTXO blockchain.
  arXiv  Detail & Related papers  (2024-06-11T20:28:27Z)
• Specification Mining for Smart Contracts with Trace Slicing and Predicate Abstraction [10.723903783651537]
  We propose a specification mining approach to infer contract specifications from past transactionhistories. Our approach derives high-level behavioral automata of function invocations, accompanied byprogram invariants statistically inferred from the transaction histories.
  arXiv  Detail & Related papers  (2024-03-20T03:39:51Z)
• Contract Usage and Evolution in Android Mobile Applications [45.44831696628473]
  We present the first large-scale empirical study on the presence and use of contracts in Android applications, written in Java or Kotlin. We analyzed 2,390 Android applications from the F-Droid repository and processed more than 51,749 KLOC. Our findings show that it would be desirable to have libraries that standardize contract specifications in Java and Kotlin.
  arXiv  Detail & Related papers  (2024-01-25T15:36:49Z)
• Automated Invariant Generation for Solidity Smart Contracts [2.4181711081104282]
  We propose a novel invariant generation framework, INVCON+, for Solidity smart contracts. INVCON+ extends the existing invariant detector, InvCon, to automatically produce verified contract invariants. We evaluate INVCON+ on 361 ERC20 and 10 ERC721 real-world contracts, as well as common ERC20 vulnerability benchmarks.
  arXiv  Detail & Related papers  (2024-01-01T03:37:30Z)
• Blockchain Smart Contract Threat Detection Technology Based on Symbolic Execution [0.0]
  Reentrancy vulnerability, which is hidden and complex, poses a great threat to smart contracts. In this paper, we propose a smart contract threat detection technology based on symbolic execution. The experimental results show that this method significantly increases both detection efficiency and accuracy.
  arXiv  Detail & Related papers  (2023-12-24T03:27:03Z)
• Formally Verifying a Real World Smart Contract [52.30656867727018]
  We search for a tool capable of formally verifying a real-world smart contract written in a recent version of Solidity. In this article, we present our search for a tool capable of formally verifying a real-world smart contract written in a recent version of Solidity.
  arXiv  Detail & Related papers  (2023-07-05T14:30:21Z)
• Blockchain Large Language Models [65.7726590159576]
  This paper presents a dynamic, real-time approach to detecting anomalous blockchain transactions. The proposed tool, BlockGPT, generates tracing representations of blockchain activity and trains from scratch a large language model to act as a real-time Intrusion Detection System.
  arXiv  Detail & Related papers  (2023-04-25T11:56:18Z)
• Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
  We construct the first fully homomorphic encryption scheme with certified deletion. Our main technical ingredient is an interactive protocol by which a quantum prover can convince a classical verifier that a sample from the Learning with Errors distribution in the form of a quantum state was deleted.
  arXiv  Detail & Related papers  (2022-03-03T10:07:32Z)
• HCC: A Language-Independent Hardening Contract Compiler for Smart Contracts [5.379572824182189]
  We propose the first practical smart contract compiler, called HCC. HCC inserts security hardening checks at the source-code level based on a novel and language-independent code property graph (CPG) notation.
  arXiv  Detail & Related papers  (2022-03-01T11:25:32Z)
• ESCORT: Ethereum Smart COntRacTs Vulnerability Detection using Deep Neural Network and Transfer Learning [80.85273827468063]
  Existing machine learning-based vulnerability detection methods are limited and only inspect whether the smart contract is vulnerable. We propose ESCORT, the first Deep Neural Network (DNN)-based vulnerability detection framework for smart contracts. We show that ESCORT achieves an average F1-score of 95% on six vulnerability types and the detection time is 0.02 seconds per contract.
  arXiv  Detail & Related papers  (2021-03-23T15:04:44Z)
• Quantum copy-protection of compute-and-compare programs in the quantum random oracle model [48.94443749859216]
  We introduce a quantum copy-protection scheme for a class of evasive functions known as " compute-and-compare programs" We prove that our scheme achieves non-trivial security against fully malicious adversaries in the quantum random oracle model (QROM) As a complementary result, we show that the same scheme fulfils a weaker notion of software protection, called "secure software leasing"
  arXiv  Detail & Related papers  (2020-09-29T08:41:53Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.