Constructing Trustworthy Smart Contracts
Devora Chait-Roth, Kedar S. Namjoshi

TL;DR
This paper presents ASP, a comprehensive system including a programming language, compiler, and proof checker, designed to create secure smart contracts that are resistant to common vulnerabilities and attacks.
Contribution
ASP introduces a new language and verification framework that ensures smart contracts are provably secure and free from typical exploits, bridging formal methods with practical deployment.
Findings
ASP guarantees contracts are free from arithmetic overflow and reentrancy vulnerabilities.
The system enables formal proofs of correctness and security properties.
ASP translates high-level secure contracts into Solidity for deployment.
Abstract
Smart contracts form the core of Web3 applications. Contracts mediate the transfer of cryptocurrency, making them irresistible targets for hackers. We introduce ASP, a system aimed at easing the construction of provably secure contracts. The Asp system consists of three closely-linked components: a programming language, a defensive compiler, and a proof checker. The language semantics guarantee that Asp contracts are free of commonly exploited vulnerabilities such as arithmetic overflow and reentrancy. The defensive compiler enforces the semantics and translates Asp to Solidity, the most popular contract language. Deductive proofs establish functional correctness and freedom from critical vulnerabilities such as unauthorized access.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Code & Models
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsBlockchain Technology Applications and Security · Insurance and Financial Risk Management · European and International Contract Law
