SKLEE: A Dynamic Symbolic Analysis Tool for Ethereum Smart Contracts (Tool Paper)

Namrata Jain, Kosuke Kaneko, Subodh Sharma

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We present SKLEE, a dynamic symbolic framework to analyse Solidity smart contracts for various safety vulnerabilities. While there are many analysis tools for Solidity contracts, in this work we demonstrate that existing analysis infrastructures for other sequential programming languages, such as C, can be leveraged to construct a competitive analysis framework for Solidity contracts. Notably, SKLEE is bootstrapped on top of KLEE – a dynamic symbolic test-case generation tool for C programs – with modelling for Solidity primitives such as send, call, transfer, and others. Our experiments indicate that SKLEE is indeed competitive with other state-of-the-art tools in terms of (i) the number of bug classes it can identify, and (ii) the number of benchmarks it can analyse in a given time bound.

Original languageEnglish
Title of host publicationSoftware Engineering and Formal Methods - 20th International Conference, SEFM 2022, Proceedings
EditorsBernd-Holger Schlingloff, Ming Chai
PublisherSpringer Science and Business Media Deutschland GmbH
Pages244-250
Number of pages7
ISBN (Print)9783031171079
DOIs
Publication statusPublished - 2022
Event20th International Conference on Software Engineering and Formal Methods, SEFM 2022 - Berlin, Germany
Duration: Sep 26 2022Sep 30 2022

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume13550 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference20th International Conference on Software Engineering and Formal Methods, SEFM 2022
Country/TerritoryGermany
CityBerlin
Period9/26/229/30/22

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint

Dive into the research topics of 'SKLEE: A Dynamic Symbolic Analysis Tool for Ethereum Smart Contracts (Tool Paper)'. Together they form a unique fingerprint.

Cite this