Constructing Trustworthy Smart Contracts
- URL: http://arxiv.org/abs/2411.14563v1
- Date: Thu, 21 Nov 2024 20:26:18 GMT
- Title: Constructing Trustworthy Smart Contracts
- Authors: Devora Chait-Roth, Kedar S. Namjoshi,
- Abstract summary: We introduce ASP, a system aimed at easing the construction of provably secure contracts.
The language semantics guarantee that Asp contracts are free of commonly exploited vulnerabilities.
The defensive compiler enforces the semantics and translates Asp to Solidity, the most popular contract language.
- Score: 1.7495213911983416
- License:
- 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.
Related papers
- COBRA: Interaction-Aware Bytecode-Level Vulnerability Detector for Smart Contracts [4.891180928768215]
We propose COBRA, a framework that integrates semantic context and function interfaces to detect vulnerabilities in smart contracts.
To infer the function signatures that are not present in signature databases, we present SRIF, which automatically learns the rules of function signatures from the smart contract bytecodes.
Experimental results demonstrate that SRIF can achieve 94.76% F1-score for function signature inference.
arXiv Detail & Related papers (2024-10-28T03:55:09Z) - ContractTinker: LLM-Empowered Vulnerability Repair for Real-World Smart Contracts [8.756175353426304]
Smart contracts are susceptible to being exploited by attackers, especially when facing real-world vulnerabilities.
To mitigate this risk, developers often rely on third-party audit services to identify potential vulnerabilities before project deployment.
Existing pattern-based repair tools mostly fail to address real-world vulnerabilities due to their lack of high-level semantic understanding.
arXiv Detail & Related papers (2024-09-15T08:24:01Z) - SCIF: A Language for Compositional Smart Contract Security [3.2707122129201975]
We introduce SCIF, a language for building smart contracts that are compositionally secure.
SCIF is based on the fundamentally compositional principle of secure information flow.
It supports a rich ecosystem of interacting principals with partial trust.
arXiv Detail & Related papers (2024-07-01T11:51:21Z) - Defending Large Language Models against Jailbreak Attacks via Semantic
Smoothing [107.97160023681184]
Aligned large language models (LLMs) are vulnerable to jailbreaking attacks.
We propose SEMANTICSMOOTH, a smoothing-based defense that aggregates predictions of semantically transformed copies of a given input prompt.
arXiv Detail & Related papers (2024-02-25T20:36:03Z) - HasTEE+ : Confidential Cloud Computing and Analytics with Haskell [50.994023665559496]
Confidential computing enables the protection of confidential code and data in a co-tenanted cloud deployment using specialized hardware isolation units called Trusted Execution Environments (TEEs)
TEEs offer low-level C/C++-based toolchains that are susceptible to inherent memory safety vulnerabilities and lack language constructs to monitor explicit and implicit information-flow leaks.
We address the above with HasTEE+, a domain-specific language (cla) embedded in Haskell that enables programming TEEs in a high-level language with strong type-safety.
arXiv Detail & Related papers (2024-01-17T00:56:23Z) - SyzTrust: State-aware Fuzzing on Trusted OS Designed for IoT Devices [67.65883495888258]
We present SyzTrust, the first state-aware fuzzing framework for vetting the security of resource-limited Trusted OSes.
SyzTrust adopts a hardware-assisted framework to enable fuzzing Trusted OSes directly on IoT devices.
We evaluate SyzTrust on Trusted OSes from three major vendors: Samsung, Tsinglink Cloud, and Ali Cloud.
arXiv Detail & Related papers (2023-09-26T08:11:38Z) - CONTRACTFIX: A Framework for Automatically Fixing Vulnerabilities in
Smart Contracts [12.68736241704817]
ContractFix is a framework that automatically generates security patches for vulnerable smart contracts.
Users can use it as a security fix-it tool that automatically applies patches and verifies the patched contracts.
arXiv Detail & Related papers (2023-07-18T01:14:31Z) - 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) - 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) - Robust Encodings: A Framework for Combating Adversarial Typos [85.70270979772388]
NLP systems are easily fooled by small perturbations of inputs.
Existing procedures to defend against such perturbations provide guaranteed robustness to worst-case attacks.
We introduce robust encodings (RobEn) that confer guaranteed robustness without making compromises on model architecture.
arXiv Detail & Related papers (2020-05-04T01:28:18Z)
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.