SolSEE

A Source-Level Symbolic Execution Engine for Solidity

Abstract

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 below and at: https://www.youtube.com/watch?v=jxShWuTwSzI.

Overview

Figure 1 demonstrates an overview of the tool architecture. SolSEE takes one or more smart contracts and a harness function as input, which should be provided using a Web UI. In its backend, SolSEE uses a Solidity compiler solc to generate the AST for the given contracts. Then, SolSEE symbolically executes each statement by traversing the AST based on the Solidity operational semantics. The (storage/memory) configuration of the smart contract is encoded symbolically as Z3 types. Also, the SMT solver is used to discharge the feasibility queries of symbolic paths and validity queries of assertions. The latter helps prove or disprove the user-defined properties encoded as assertions in the harness function.

Demonstration Video

Page updated

Google Sites

Report abuse