Theorem-Carrying Transactions: Runtime Verification to Ensure Interface Specifications for Smart Contract Safety
Fuente:
arXiv
Salvato in:
| Autori principali: | , , , , , , , , |
|---|---|
| Natura: | Preprint |
| Pubblicazione: |
2024
|
| Soggetti: | |
| Accesso online: | |
| Tags: |
Aggiungi Tag
Nessun Tag, puoi essere il primo ad aggiungerne!!
|
| _version_ | 1866915432864153600 |
|---|---|
| author | Ball, Thomas Bjørner, Nikolaj S. Chen, Ashley J. Chen, Shuo Chen, Yang Guo, Zhongxin Hsu, Tzu-Han Liu, Peng Luo, Nanqing |
| author_facet | Ball, Thomas Bjørner, Nikolaj S. Chen, Ashley J. Chen, Shuo Chen, Yang Guo, Zhongxin Hsu, Tzu-Han Liu, Peng Luo, Nanqing |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2408_06478 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Theorem-Carrying Transactions: Runtime Verification to Ensure Interface Specifications for Smart Contract Safety Ball, Thomas Bjørner, Nikolaj S. Chen, Ashley J. Chen, Shuo Chen, Yang Guo, Zhongxin Hsu, Tzu-Han Liu, Peng Luo, Nanqing Cryptography and Security Programming Languages 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. |
| title | Theorem-Carrying Transactions: Runtime Verification to Ensure Interface Specifications for Smart Contract Safety |
| topic | Cryptography and Security Programming Languages |
| url | https://arxiv.org/abs/2408.06478 |