Security Analysis Tool: Manticore

SmartState.tech
3 min readSep 25, 2022

--

What is: security analysis tool Manticore
Security Analysis Tool: Manticore

Manticore is a Python-based symbolic execution tool for Ethereum smart contracts and binary audit. In addition to EVM based smart contracts (EVM bytecode), Manticore can also analyze Linux ELF binaries (x86, x86_64, aarch64, and ARMv7) and WASM Modules.

One of its unique features is the ability to explore a lot of execution ways by means of replacing the original program inputs with symbolic parameters and studying their conditions thoroughly, testing each element of the program carefully. Despite these apparent complications, it actually has very few dependencies. Manticore models various attack scenarios to check the code security. It is very helpful while searching for crash scenarios, execution tracing, input checks and the like.

Manticore analysis capabilities
Manticore analysis capabilities

Manticore features

Manticore has its unique features, which make it so attractive, such as:

  • Program exploration. The tool uses symbolic input parameters to study every possible state of a program and trigger various code paths
  • Input generation. It automatically produces relevant inputs which result in a program state in question
  • Error discovery. Manticore detects failures and errors in smart contracts and binaries and traces the inputs leading to the investigated crash
  • Instrumentation. It takes over the control of the exploration through callbacks and records the execution trace
  • Programmatic interface. It exposes the analysis engine via Python

Manticore detectors

To hit the target, Manticore uses a pack of specific detectors:

- DetectEnvInstruction (it detects the instruction used for the environmental or block data to avoid the manipulation of this data by the third parties)

- DetectSuicidal (checks for self-destruct instructions)

- DetectExternalCallAndLeak (checks external calls or leaks of the addresses)

- DetectInvalid (finds invalid instructions)

- DetectReentrancySimple and Advanced (both are used to look for reentrancy bugs)

- DetectIntegerOverflow (used to detect overflow and underflow conditions)

- DetectUnusedRetVal (helps to spot unused return values from internal transactions)

- DetectDelegatecall (It helps to discover, if the destination address or/and first four bytes are taken over by the caller)

- DetectUninitializedMemory and DetectUninitializedStorage (check the use of uninitialized memory or storage)

- DetectRaceCondition (it helps to discover transaction order dependencies)

- DetectManipulableBalance (checks the execution of manipulable balance)

How is Manticore used?

Manticore is used mostly for binary and malware analysis and reverse engineering. Some specialists see it as too slow, but only for the fact that it thoroughly checks various parts of code with a number of attack scenarios.

Before installing the tool, Solidity compiler solc and theorem prover z3 must be installed, too. For smart contract testing Manticore uses a symbolic EVM (Ethereum Virtual Machine). It easily integrates with Ethersplay and a Command line tool, as well, which helps to create program test cases with symbolic execution to perform as many tests as needed to discover the possible bugs and failures.

For binary analysis of Execute and linkable format files (ELF files) either command line interface (CLI) or Python API can be used. The user just has to run Manticore with the binary path and add optional parameters, if necessary.

SmartState: Web3 security easier than ever
SmartState: Web3 security easier than ever

About SmartState

Launched in 2019 and located in Dubai, SmartState provides enterprise level of Web3 security and is retaining the place of one of the leading DeFi security auditing companies. We carry out tests of security of the code core, smart contracts and blockchain for all types of errors or vulnerabilities.

We specialize in manual testing, so the SmartState’s tech team of white-hat security professionals carefully measures up a project’s git and supports clients with guidelines and recommendations for the further advancement.

Our security audit reports review the threats and vulnerabilities with which codebases may be exploited in the future, because the network achieves scalability and expands to accommodate more use cases and functionality.

Keep up to date with all the SmartState news & events, follow us on social media:

--

--

SmartState.tech
SmartState.tech

Written by SmartState.tech

🇦🇪 Dubai-based enterprise level Web3 security company. Top-notch smart contract audits & blockchain security solutions 🚀🔒

No responses yet