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

Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts

Software Engineering 2019-11-19 v3 Cryptography and Security

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

View on arXiv ↗ PDF ↗

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.

Keywords

symbolic execution smart contract compiler optimization

Cite

@article{arxiv.1907.03890,
  title  = {Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts},
  author = {Mark Mossberg and Felipe Manzano and Eric Hennenfent and Alex Groce and Gustavo Grieco and Josselin Feist and Trent Brunson and Artem Dinaburg},
  journal= {arXiv preprint arXiv:1907.03890},
  year   = {2019}
}

Comments

Fix in bibliography

Manticore: A User-Friendly Symbolic Execution Framework for Binaries and Smart Contracts

Abstract

Keywords

Cite

Comments

Related papers