Smart Contracts are computer programs that enable decentralized applications on the blockchain. They are usually written in Turing-complete programming languages like Solidity, which is similar to JavaScript. In Solidity, a contract is a first-class object that can extend its capabilities by inheriting other contracts or delegating tasks to them. However, the complexity of this composability also makes smart contracts vulnerable to many security threats.

Figure 1 illustrates the basic workflows involved in the development and deployment of smart contracts. Typically, developers write the smart contract code in files with the “.sol” suffix and use the Solidity compiler to translate the source code into bytecode. The bytecode is then deployed to blockchain platforms like Ethereum. Since the infamous DAO attack in 2016, security experts and attackers alike have been focusing on finding vulnerabilities in smart contracts. Several approaches have been proposed to detect contract vulnerabilities, with many achieving significant success. However, after investigating the existing approaches, we found a lack of powerful formal verification engines for Solidity smart contracts. Existing approaches to smart contract security can be classified based on their input, either bytecode or source code. Most approaches target bytecode-level analysis using techniques such as fuzzing and symbolic execution. Others focus on source code-level analysis using formal verification and AST-based static analysis. However, these approaches are often either inaccurate or inefficient. Bytecode-level analysis typically produces more accurate results, while source code-level analysis can find more vulnerabilities.

Figure 1. The basic workflow of smart contracts.

Formal verification involves using mathematical formal methods to analyze a program and determine whether it is correct or incorrect. A robust smart contract formal verification engine must be accompanied by a source-level symbolic execution engine to ensure both accuracy and scalability. In this post, we present SolSEE, which is the first source-level symbolic execution engine for Solidity smart contracts. SolSEE is capable of executing smart contracts written in multiple Solidity versions, customizable harness support, identifying common contract vulnerabilities, and performing bounded formal verification.

Introduction to SolSEE

Figure 2. The architecture of SolSEE.

SolSEE’s symbolic execution module supports most Solidity language features, such as intra- and inter-contract function calls, multiple inheritances, library support through the “using … for” construct, low-level function calls like “.call.value()()” and the associated fallback mechanism, modifiers, and others. Similar to the Solidity compiler, SolSEE automatically generates getter functions for public smart contract variables of elementary types. However, SolSEE does not support inline assembly, like other source-level analyzers for smart contracts. Additionally, SolSEE introduces a supplementary “assume()” statement that allows developers to specify assumption conditions during verification, as shown in Listing 2 on line 5.

SolSEE differentiates the semantics of the “require()” and “assert()” functions, which can both lead to transaction rollbacks if their conditions fail. In Solidity, “require()” is used to check a condition that is expected to fail occasionally, such as a guard condition on function input arguments. Therefore, if the expression enclosed in “require()” evaluates to false, SolSEE rolls back all transaction effects on the smart contract state. Each statement in the harness function is considered a separate transaction. On the other hand, “assert()” in Solidity is used to check conditions that should never evaluate to false. If an asserted condition is violated, SolSEE halts execution and reports a violation.

SolSEE not only performs bounded formal verification on Solidity smart contracts but also detects any vulnerabilities that it may find during symbolic execution. One of the most common issues in Solidity smart contracts is integer under- and overflows, particularly since unsigned integers are heavily utilized to store essential information like token balances. SolSEE employs a modular arithmetic approach to handle unsigned integers of different sizes, ranging from uint8 to uint256. It models these integers using Z3 integers and constrains them with range assertions to ensure that they follow the semantics of unsigned integer arithmetic operations in Solidity. While bit vectors are another popular approach to model unsigned integers, they have been found to have scalability issues.

To model one- and multi-dimensional arrays and mappings, SolSEE relies on the array theory.

SolSEE supports both randomly generated interaction sequences and user-provided harness functions to guide the symbolic execution process. However, using a harness function can lead to more meaningful interactions and make the analysis more configurable. During path exploration and assertion checking, SolSEE uses the Z3 SMT-solver to resolve constraints. The harness function can also be used to encode assertions about the execution trace or smart contract invariants. To optimize performance, SolSEE assumes that smart contract variables in the harness or analyzed smart contracts have concrete (default) values unless they are declared as symbolic. Additionally, the Ethereum balance of the main harness smart contract (MAIN) is assumed to be symbolic. This level of configurability and optimization is crucial for analyzing complex smart contract code effectively and efficiently in a realistic setting, as demonstrated in our evaluation.

Demonstration by Harness Example

To demonstrate the capabilities of SolSEE, we provide an example using a token smart contract implementation shown in Listing 1. In this implementation, users interact with the contract by invoking its public or external functions via transactions. The deposit() function (lines 18–20) accepts ETH and records the deposited amount in a balances mapping entry associated with the transaction sender. The recover() function (lines 21–23) sends all the ETH balance of the token to its owner, as determined by the Ownable smart contract that Token inherits from (lines 1–10). The signature of recover() contains an invocation of the only owner modifier to ensure that only the owner can call it (lines 7–8). During symbolic execution, SolSEE represents the storage and memory configuration of the contract and executes each statement based on the operational semantics of Solidity, which supports key features such as inheritance, modifiers, and ETH transfer. To explore interesting smart contract behaviors efficiently, SolSEE supports a user-defined harness function that specifies the sequence of function calls to be analyzed symbolically. The harness follows the syntax and semantics of Solidity and is intuitive and easy to use for developers. SolSEE also relies on the Z3 SMT-solver to determine the satisfiability of the generated path constraints.

Listing 2 provides an example of how to define a harness in SolSEE. The MAIN contract acts as the entry point, and the harness is defined as its constructor. The harness includes the declaration of a symbolic variable, which should be prefixed with “$” (line 4), and the creation of the Token smart contract, which involves transferring a symbolic amount of ETH to this contract (line 6). Additionally, the harness invokes the recover() function of the Token smart contract, which succeeds because it is called by the MAIN contract, satisfying the only owner modifier. Lines 10–12 define a fallback function, which is a feature unique to Solidity and also supported by SolSEE. The fallback function is called when ETH is transferred to a smart contract, such as during the execution of the “.call.value()()” in Listing 1, line 22. As recover() is executed successfully, the assertion in Listing 2, line 8, should always be satisfied. The assertion in a harness function can also declare a property, constructed using Solidity operators and variables available in the MAIN contract. Additionally, SolSEE allows assumptions to be specified in terms of smart contract variables using the assume() statement. For example, line 5 in Listing 2 indicates that the analysis will only consider paths where the ETH balance of the MAIN contract is not less than the amount of ETH being sent to the Token during its creation.

Comparison with the SOTAs

We showcase the powerful capabilities of SolSEE by comparing it with other source-level tools designed for analyzing Solidity smart contracts. The tools we compare with include sold-verify, VeriSol v0.1.5, VeriSol-SP (a modified version of VeriSol v0.1.5 used in SmartPulse), VeriSmart, and SMTChecker (included in sold v0.5.11). All of these tools claim to be able to detect assertion failures, which is the feature we focus on evaluating. To assess the performance of SolSEE and these tools, we ran them on our sample contract (Listing 1) and a dataset containing nine different Solidity features. Table 1 summarizes how each tool supports these nine features, with each feature having a corresponding smart contract listed in the first two columns of the table.

Our results show that SolSEE is the only tool that supports all nine Solidity features used in our experiments. On the other hand, the other tools lack support for some of these features. For example, VeriSol does not support modifiers with multiple “_;” statements, VeriSmart cannot handle fallback functions or correctly analyze arithmetic operations on variables of unsigned integer (uint) types, sold-verify and VeriSol require a non-default modular arithmetic mode to follow the semantics of arithmetic operations for uint, SMTChecker does not support variables of type struct, and sold-verify fails to process a bytes32 array.

Additionally, our evaluation reveals that the analyzed tools often report false positives. This is partly due to the lack of harness function support and missing or incorrect handling of Solidity language features and their semantics. None of the tools, except SolSEE and SmartPulse, correctly implement C3 Linearization, which is used by Solidity to decide the order in which methods are inherited in the presence of multiple inheritances. Furthermore, VeriSmart and SMTChecker can only process smart contracts correctly if all the functionality is stored in a single contract, i.e., no external function calls are allowed.

Regarding the speed of analysis, SolSEE is as efficient as the other tools used for comparison.

Related work

Most of the symbolic execution tools available for smart contracts operate on the bytecode level, which provides limited information about the contract’s semantics and complicates reasoning about high-level properties. These tools usually focus on detecting well-known vulnerabilities based on patterns in the bytecode, but they do not offer comprehensive support for Solidity features. For instance, Oyente, Mythril, and Maian are tools that operate on bytecode and focus on detecting vulnerabilities. Manticore is a symbolic execution engine that operates on the bytecode level and supports property-based symbolic execution. However, it offers little support for high-level Solidity semantics and presents low-level bytecode instructions that are difficult for developers to match with their original Solidity code. In contrast, existing source-level tools for Solidity smart contracts offer better support for Solidity features but lack customization of the function call sequence and the environment to be analyzed. For example, VeriSmart and SmarTest are smart contract verifiers that perform symbolic execution but do not precisely handle the execution of fallback functions and inter-contract function calls, which are critical components of smart contracts. SMTChecker, a built-in verifier within the Solidity compiler, also fails to analyze inter-contract function calls. Two other source-level tools, sold-verify and VeriSol, translate Solidity code into Boogie intermediate language, which may introduce discrepancies between the analyzed code translation and original Solidity semantics. These tools also lack support for certain Solidity features and do not allow customization of the harness function and analyzed environment, leading to false positives.

Certora is a formal verification tool for smart contracts that focuses on bounded formal verification. To use Certora, developers must learn their proposed specification language, CVL, to write the specification and the harness function. However, this new domain-specific language may have a steep learning curve for general smart contract developers.

In contrast, SolSEE is a source-level symbolic execution tool for Solidity smart contracts that supports the analysis of various Solidity features and allows developers to write the properties and harness functions in Solidity language, which is more user-friendly to developers.

SolSEE was previously published as research work in a top-tier software engineering conference in 2022 and is currently in its beta phase developed by MetaTrust, a Singaporean start-up business specializing in Web3 security. SolSEE will be integrated into MetaTrust’s product lines as a proprietary tool to assist smart contract developers and auditors.

Company Introduction

Metatrust is a leading security solutions provider focused on helping developers enhance security protections throughout various stages of the software development lifecycle to safeguard their digital assets and privacy. Metatrust’s solutions cover multiple areas, including security risk assessments, security auditing, and smart contract security protection.

Reference work

[1] Shang-Wei Lin, Palina Tolmach, Ye Liu, and Yi Li. “SolSEE: a source-level symbolic execution engine for solidity.” In Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pp. 1687–1691. 2022.

Try our product for FREE to scan the smart contracts you care about.

• Sign-up：https://app.metatrust.io/sign-up
• Sign-in：https://app.metatrust.io/sign-in

Twitter: https://twitter.com/MetatrustLabs

Website: https://metatrust.io/