Collaborative business processes can be seen as smart contracts, as they are oftentimes adopted to express agreements among different organizations. Indeed, they provide mechanisms to formalize the obligations of each involved party. For instance, collaborative business processes can specify when a certain task should be executed, under which conditions a service should be offered to the other participants, and how physical objects and information should be manipulated. In this setting, to prevent misuse of smart contracts and services and information provided, it is paramount to guarantee by design that security requirements are fulfilled. With the rise in popularity of blockchains, several approaches exploiting the trusted smart contract execution environment offered by this technology to enforce collaborative business processes have been proposed. Yet, the complexity of business processes, security requirements, and blockchain applications calls for an engineering approach that guides the design of secure business processes. Such an approach should both take advantage of the possibilities offered by blockchain technology to enforce some security requirements (e.g., non-repudiation), and take into account the limitations blockchain poses for other security requirements (e.g., confidentiality). However, we are not aware of any existing work that aims at addressing such issues following a similar approach. In this article, we propose SecBPMN2BC: a model-driven approach to designing business processes with security requirements that are meant to be deployed on blockchains. SecBPMN2BC consists of: (i) an extension of BPMN 2.0 that allows designing secure smart contracts; (ii) a set of algorithms and their implementation that check incompatible security requirements and help the design of smart contracts; (iii) a workflow that guides the application of the method. The method has been validated with a survey conducted on security and BPMN experts.
Smart contracts are digital contracts that rely on Blockchain technology to make their terms and execution conditions unforgeable. The purpose of a smart contract is to eliminate the need for a middleman in business and trade between anonymous and identified participants. Since 2016, smart contracts have been gaining traction in various areas, including public management, supply chain, energy, finance, communication, and healthcare. Anyone who interacts with a smart contract after it is launched on the blockchain system will be in danger if it contains vulnerabilities or faults. Therefore, the use of formal methods which are mathematical techniques for modeling, designing, and testing software and hardware systems to ensure they are constructed correctly, is highly required. In this paper, the applied state-of-the-art formal methods on smart contracts specification and verification have been reviewed with the aim of minimizing the risk of faults and bugs occurrence and avoiding possible resulting costs. Also, we have discussed several challenges and future research guidelines related to this emerging research tonic.
Abstract The Ethereum blockchain stores and executes complex logic via smart contracts written in Solidity, a high‐level programming language. The Solidity language (in its early versions) provides features to exercise fine‐grained control over smart contracts, whose usage is discouraged by later‐released Solidity documentation, but nonetheless supported in later versions for backward compatibility. We define these features as low‐level functions. However, the high‐volume of transactions and the improper use of low‐level functions lead to security exploits with heavy financial loss. Consequently, the documentation suggests secure alternatives to the use of low‐level functions. In this article, we first perform an empirical study on the use of low‐level functions in Ethereum smart contracts. We study a smart contract dataset consisting of over 2,100,000 real‐world smart contracts. We find that low‐level functions are widely used and that the majority of these uses are gratuitous. We then propose GoHigh, a source‐to‐source transformation tool to eliminate low‐level function‐related vulnerabilities, by replacing low‐level functions with secure alternatives. Our experimental evaluation on the dataset shows that GoHigh successfully replaces all low‐level functions with 4.9% fewer compiler warnings. Further, no unintended side‐effects are introduced in 80% of the contracts, and the remaining 20% are not verifiable due to their external dependency. GoHigh saves more than 5% of the gas cost of the contract. Finally, GoHigh takes 7 s on average per contract.
Most of the existing smart contract symbolic execution tools perform analysis on bytecode, which loses high-level semantic information presented in source code. This makes interactive analysis tasks—such as visualization and debugging—extremely challenging, and significantly limits the tool usability. In this paper, we present SolSEE, a source-level symbolic execution engine for Solidity smart contracts. We describe the design of SolSEE, highlight its key features, and demonstrate its usages through a Web-based user interface. SolSEE demonstrates advantages over other existing source-level analysis tools in the advanced Solidity language features it supports and analysis flexibility. A demonstration video is available at: https://sites.google.com/view/solsee/.
In this paper, we specify and verify the correctness of programs written in Bitcoin’s smart contract SCRIPT in the interactive theorem prover Agda. As in the previous article [1], we use weakest preconditions of Hoare logic to specify the security property of access control, and show how to develop human-readable specifications. In this article, we include conditionals into the language. For the operational semantics we use an additional stack, the ifstack, to deal with nested conditionals. This avoids the addition of extra jump instructions, which are usually used for the operational semantics of conditionals in Forth-style stack languages. The ifstack preserves the original nesting of conditionals, and we determine an ifthenselse-theorem which allows to derive verification conditions of conditionals by referring to conditions for the if- and else-case.
Lorenzo Grassi, Dmitry Khovratovich, Reinhard Lüftenegger, Christian Rechberger · 6 authors
We propose a new hash function Reinforced Concrete, which is the first generic purpose hash that is fast both for a zero-knowledge prover and in native x86 computations. It is suitable for a various range of zero-knowledge proofs and protocols, from set membership to generic purpose verifiable computation. Being up to 15x faster than its predecessor Poseidon hash, Reinforced Concrete inherits security from traditional time-tested schemes such as AES, whereas taking the zero-knowledge performance from a novel and efficient decomposition of a prime field into compact buckets.
Ning Luo, Timos Antonopoulos, William R. Harris, Ružica Piskač · 6 authors
Zero-knowledge (ZK) protocols enable one party to prove to others that it knows a fact without revealing any information about the evidence for such knowledge. There exist ZK protocols for all problems in NP, and recent works developed highly efficient protocols for proving knowledge of satisfying assignments to Boolean formulas, circuits and other NP formalisms. This work shows an efficient protocol for the converse: proving formula unsatisfiability in ZK (when the prover posses a non-ZK proof). An immediate practical application is efficiently proving safety of secret programs.
An accumulator is a cryptographic primitive that allows a prover to succinctly commit to a set of values while being able to provide proofs of (non-)membership. A batch proof is an accumulator proof that can be used to prove (non-)membership of multiple values simultaneously.
In the past few years, several attacks against the vulnerabilities of EOSIO smart contracts have caused severe financial losses to this prevalent blockchain platform. As a lightweight test-generation approach, grey-box fuzzing can open up the possibility of improving the security of EOSIO smart contracts. However, developing a practical grey-box fuzzer for EOSIO smart contracts from scratch is time-consuming and requires a deep understanding of EOSIO internals. In this work, we proposed AntFuzzer, the first highly extensible grey-box fuzzing framework for EOSIO smart contracts. AntFuzzer implements a novel approach that interfaces AFL to conduct AFL-style grey-box fuzzing on EOSIO smart contracts. Compared to black-box fuzzing tools, AntFuzzer can effectively trigger those hard-to-cover branches. It achieved an improvement in code coverage on 37.5% of smart contracts in our benchmark dataset. AntFuzzer provides unified interfaces for users to easily develop new detection plugins for continually emerging vulnerabilities. We have implemented 6 detection plugins on AntFuzzer to detect major vulnerabilities of EOSIO smart contracts. In our large-scale fuzzing experiments on 4,616 real-world smart contracts, AntFuzzer successfully detected 741 vulnerabilities. The results demonstrate the effectiveness and efficiency of AntFuzzer and our detection pl
SolSec Labs is a web-based application that provides interactive training labs for blockchain developers, especially students eager to learn more about smart contract security to gain practical knowledge ( <xref ref-type="fig" rid="fig1" xmlns:mml="http://www.w3.org/1998/Math/MathML" xmlns:xlink="http://www.w3.org/1999/xlink">Fig. 1</xref> ). It teaches solidity and smart contract security skills through hands-on experience. The easy-to-understand environment enables students and early developers to immediately apply newly learned secure coding practices to their ongoing projects. Currently, it consists of a total of 10 labs crafted using examples taken from the most severe real-world vulnerabilities. Every lab teaches developers about the related vulnerability; exploitation methods; preventive and remediation measures; and, finally, a step-by-step list of lab tasks to perform to secure the presented vulnerable code.
Smart Grid Security and Resilience
Security and Verification in Computing
Advancements in Semiconductor Devices and Circuit Design
Zihan Zhao, Sidi Mohamed Beillahi, Ryan Song, Yuxi Cai · 6 authors
This paper presents SigVM, the first blockchain virtual machine that extends EVM to support an event-driven execution model, enabling developers to build truly decentralized smart contracts. Contracts in SigVM can emit signal events, on which other contracts can listen. Once an event is triggered, corresponding handler functions are automatically executed as signal transactions. We build an end-to-end blockchain platform SigChain and a contract language compiler SigSolid to realize the potential of SigVM. Experimental results show that our benchmark applications can be reimplemented with SigVM in a truly decentralized way, eliminating the dependency on centralized and unreliable mechanisms like off-chain relay servers. The development effort of reimplementing these contracts with SigVM is small, i.e., we modified on average 3.17% of the contract code. The runtime and the gas overhead of SigVM on these contracts is negligible.
Stefanos Chaliasos, Arthur Gervais, Benjamin Livshits
The Solidity programming language is the most widely used language for smart contract development. Improving smart contracts’ correctness, security, and performance has been the driving force for research in vulnerability detection, program analysis, and compiler techniques for Solidity. Similar to system-level languages such as C, Solidity enables the embedding of low-level code in programs, in the form of inline assembly code. Developers use inline assembly for low-level optimizations, extending the Solidity language through libraries, and using blockchain-specific opcodes only available through inline assembly. Nevertheless, inline assembly fragments are not well understood by an average developer and can introduce security threats as well as affect the optimizations that can be applied to programs by the compiler; it also significantly limits the effectiveness of source code static analyzers that operate on the Solidity level. A better understanding of how inline assembly is used in practice could in turn increase the performance, security, and support for inline assembly in Solidity. This paper presents a large-scale quantitative study of the use of inline assembly in 6.8M smart contracts deployed on the Ethereum blockchain. We find that 23% of the analyzed smart contracts contain inline assembly code, and that the use of inline assembly has become more widespread over time. We further performed a manual qualitative analysis for identifying usage patterns of inline assembly in Solidity smart contracts. Our findings are intended to help practitioners understand when they should use inline assembly and guide developers of Solidity tools in prioritizing which parts of inline assembly to implement first. Finally, the insights of this study could be used to enhance the Solidity language, improve the Solidity compiler, and to open up new research directions by driving future researchers to build appropriate methods and techniques for replacing inline assembly in Solidity programs when there is no real necessity to use it.
Javier Godoy, Juan Pablo Galeotti, Diego Garbervetsky, Sebastián Uchitel
Smart contracts are immutable programs deployed on the blockchain that can manage significant assets. Because of this, verification and validation of smart contracts is of vital importance. Indeed, it is industrial practice to hire independent specialized companies to audit smart contracts before deployment. Auditors typically rely on a combination of tools and experience but still fail to identify problems in smart contracts before deployment, causing significant losses. In this paper, we propose using predicate abstraction to construct models which can be used by auditors to explore and validate smart contact behaviour at the function call level by proposing predicates that expose different aspects of the contract. We propose predicates based on requires clauses and enum-type state variables as a starting point for contract validation and report on an evaluation on two different benchmarks.
Eric Keilty, Keerthi Nelaturu, Bowen Wu, Andreas Veneris
As the popularity of distributed ledger technology and smart contracts continues to grow, so does the number of decentralized applications and their potential exposure to expensive exploits. The need for strong vulnerability detection tools is critical. Move is a recently developed smart contract language with safety and security at the core of its design containing formal verification tools embedded into the language. Currently, these tools can only verify local properties within a single Move function. They cannot verify global properties that result from multiple function executions. In this paper, we introduce VeriMove, an extension of the VeriSolid correct-by-design model checking framework that supports the Move language. We show that model checking is a feasible method to formally verify global properties in Move smart contracts.
As a powerful tool for building framework and autonomous system across various domains, smart contracts are used to maintain security analysis in a better way. However, owing to the decentralised structure of the blockchain on which they are built, a number of concerns have surfaced about weaknesses in their programming, that according to their unique characteristics, might have (and have already had) a very large economic effect. This essay surveys the whole scope of smart contract security issues and the cutting edge of freely accessible security software.
Tommaso Frassetto, Patrick Jauernig, David Koisser, David Kretzler · 7 authors
Smart contracts enable users to execute payments depending on complex program logic. Ethereum is the most notable example of a blockchain that supports smart contracts leveraged for countless applications including games, auctions and financial products. Unfortunately, the traditional method of running contract code on-chain is very expensive, for instance, on the Ethereum platform, fees have dramatically increased, rendering the system unsuitable for complex applications. A prominent solution to address this problem is to execute code off-chain and only use the blockchain as a trust anchor. While there has been significant progress in developing off-chain systems over the last years, current off-chain solutions suffer from various drawbacks including costly blockchain interactions, lack of data privacy, huge capital costs from locked collateral, or supporting only a restricted set of applications. \n \nIn this paper, we present POSE—a practical off-chain protocol for smart contracts that addresses the aforementioned shortcomings of existing solutions. POSE leverages a pool of Trusted Execution Environments (TEEs) to execute the computation efficiently and to swiftly recover from accidental or malicious failures. We show that POSE provides strong security guarantees even if a large subset of parties is corrupted. We evaluate our proof-of-concept implementation with respect to its efficiency and effectiveness.
Smart contracts are self-governed computer programs that run on blockchain to facilitate asset transfer between users within a trustless environment. The absence of contract specifications hinders routine tasks, such as program understanding, debugging, testing, and verification of smart contracts. In this work, we propose a unified specification mining framework to infer specification models from past transaction histories. These include access control models describing high-level authorization rules, program invariants capturing low-level program semantics, and behavior models characterizing interaction patterns allowed by contract implementations. The extracted specification models can be used to perform conformance checking on smart contracts, with the goal of eliminating unforeseen contract quality issues.
The growth in the popularity of smart contracts has been accompanied by a rise in security attacks targeting smart contracts, which have led to financial losses of millions of dollars and erosion of trust. To enable developers discover vulnerabilities in smart contracts, several static analysis tools have been proposed. However, despite the numerous bug-finding tools, security vulnerabilities abound in smart contracts, and developers rely on finding vulnerabilities manually. Our goal in this dissertation study is to expand the space of security vulnerabilities detection by proposing effective static analysis approaches for smart contracts. We study the effectiveness of the existing static analysis tools and propose solutions for security vulnerabilities detection relying on analyzing the dependency of the contract code on user inputs that lead to security vulnerabilities. Our results of evaluating static analysis tools show that existing static tools for smart contracts have significant false-negatives and false-positives. Further, the results show that our first vulnerability detection approach achieves a significant improvement in the effectiveness of detecting vulnerabilities compared to the prior work.
Smart contracts are gaining popularity as a means to support transparent, traceable, and self-executing decentralized applications, which enable the exchange of value in a trustless environment. Developers of smart contracts rely on various libraries, such as OpenZeppelin for Solidity contracts, to improve application quality and reduce development costs. The API documentations of these libraries are important sources of information for developers who are unfamiliar with the APIs. Yet, maintaining high-quality documentations is non-trivial, and errors in documentations may place barriers for developers to learn the correct usages of APIs. In this paper, we propose a technique, DocCon, to detect inconsistencies between documentations and the corresponding code for Solidity smart contract libraries. Our fact-based approach allows inconsistencies of different severity levels to be queried, from a database containing precomputed facts about the API code and documentations. DocCon successfully detected high-priority API documentation errors in popular smart contract libraries, including mismatching parameters, missing requirements, outdated descriptions, etc. Our experiment result shows that DocCon achieves good precision and is applicable to different libraries: 29 and 22 out of our reported 40 errors have been confirmed and fixed by library developers so far.
Smart contracts are self-executing computer programs deployed on blockchain to enable trustworthy exchange of value without the need of a central authority. With the absence of documentation and specifications, routine tasks such as program understanding, maintenance, verification, and validation, remain challenging for smart contracts. In this paper, we propose a dynamic invariant detection tool, InvCon, for Ethereum smart contracts to mitigate this issue. The detected invariants can be used to not only support the reverse engineering of contract specifications, but also enable standard-compliance checking for contract implementations. InvCon provides a Web-based interface and a demonstration video of it is available at: https://youtu.be/Y1QBHjDSMYk.
Ignacio Amores-Sesar, Christian Cachin, Tedeschi, Enrico
Avalanche is a blockchain consensus protocol with exceptionally low latency and high throughput. This has swiftly established the corresponding token as a top-tier cryptocurrency. Avalanche achieves such remarkable metrics by substituting proof of work with a random sampling mechanism. The protocol also differs from Bitcoin, Ethereum, and many others by forming a directed acyclic graph (DAG) instead of a chain. It does not totally order all transactions, establishes a partial order among them, and accepts transactions in the DAG that satisfy specific properties. Such parallelism is widely regarded as a technique that increases the efficiency of consensus. Despite its success, Avalanche consensus lacks a complete abstract specification and a matching formal analysis. To address this drawback, this work provides first a detailed formulation of Avalanche through pseudocode. This includes features that are omitted from the original whitepaper or are only vaguely explained in the documentation. Second, the paper gives an analysis of the formal properties fulfilled by Avalanche in the sense of a generic broadcast protocol that only orders related transactions. Last but not least, the analysis reveals a vulnerability that affects the liveness of the protocol. A possible solution that addresses the problem is also proposed.
Blockchains have seen growing traction with cryptocurrencies reaching a market cap of over 1 trillion dollars, major institution investors taking interests, and global impacts on governments, businesses, and individuals. Also growing significantly is the heterogeneity of the ecosystem where a variety of blockchains co-exist. Cross-chain bridge is a necessary building block in this multi-chain ecosystem. Existing solutions, however, either suffer from performance issues or rely on trust assumptions of committees that significantly lower the security. Recurring attacks against bridges have cost users more than 1.5 billion USD. In this paper, we introduce zkBridge, an efficient cross-chain bridge that guarantees strong security without external trust assumptions. With succinct proofs, zkBridge not only guarantees correctness, but also significantly reduces on-chain verification cost. We propose novel succinct proof protocols that are orders-of-magnitude faster than existing solutions for workload in zkBridge. With a modular design, zkBridge enables a broad spectrum of use cases and capabilities, including message passing, token transferring, and other computational logic operating on state changes from different chains. To demonstrate the practicality of zkBridge, we implemented a prototype bridge from Cosmos to Ethereum, a particularly challenging direction that involves large proof circuits that existing systems cannot efficiently handle. Our evaluation shows that zkBridge achieves practical performance: proof generation takes less than 20 seconds, while verifying proofs on-chain costs less than 230K gas. For completeness, we also implemented and evaluated the direction from Ethereum to other EVM-compatible chains (such as BSC) which involves smaller circuits and incurs much less overhead.