SolSEE: A Source-Level Symbolic Execution Engine for Solidity

Shang-Wei Lin, Palina Tolmach, Ye Liu, and Yi Li

In Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (FSE), 2022

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 at: https://sites.google.com/view/solsee/.

Cite:

@inproceedings{Lin2022SAS,
  author = {Lin, Shang-Wei and Tolmach, Palina and Liu, Ye and Li, Yi},
  booktitle = {Proceedings of the 30th ACM Joint European Software Engineering Conference and Symposium on the Foundations of Software Engineering (FSE)},
  month = nov,
  pages = {1687--1691},
  publisher = {ACM},
  title = {{SolSEE}: A Source-Level Symbolic Execution Engine for {Solidity}},
  year = {2022}
}