Manticore: A user-friendly symbolic execution framework for binaries and smart contracts

Mark Mossberg, Felipe Manzano, Eric Hennenfent, Alex Groce, Gustavo Grieco, Josselin Feist, Trent Brunson, Artem Dinaburg

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

254 Scopus citations

Abstract

An effective way to maximize code coverage in software tests is through dynamic symbolic execution-a technique that uses constraint solving to systematically explore a program's state space. We introduce an open-source dynamic symbolic execution framework called Manticore for analyzing binaries and Ethereum smart contracts. Manticore's flexible architecture allows it to support both traditional and exotic execution environments, and its API allows users to customize their analysis. Here, we discuss Manticore's architecture and demonstrate the capabilities we have used to find bugs and verify the correctness of code for our commercial clients.

Original languageEnglish (US)
Title of host publicationProceedings - 2019 34th IEEE/ACM International Conference on Automated Software Engineering, ASE 2019
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages1186-1189
Number of pages4
ISBN (Electronic)9781728125084
DOIs
StatePublished - Nov 2019
Externally publishedYes
Event34th IEEE/ACM International Conference on Automated Software Engineering, ASE 2019 - San Diego, United States
Duration: Nov 10 2019Nov 15 2019

Publication series

NameProceedings - 2019 34th IEEE/ACM International Conference on Automated Software Engineering, ASE 2019

Conference

Conference34th IEEE/ACM International Conference on Automated Software Engineering, ASE 2019
Country/TerritoryUnited States
CitySan Diego
Period11/10/1911/15/19

Keywords

  • Ethereum
  • Manticore
  • Mcore
  • Smart contract
  • Symbolic execution

ASJC Scopus subject areas

  • Computer Networks and Communications
  • Software
  • Control and Optimization

Fingerprint

Dive into the research topics of 'Manticore: A user-friendly symbolic execution framework for binaries and smart contracts'. Together they form a unique fingerprint.

Cite this