⚠️ Projekt ist archiviert ⚠️

Dieses Projekt wird nicht mehr intern entwickelt und gewartet.

Manticore

Manticore ist ein Werkzeug zur symbolischen Ausführung für die Analyse von Smart Contracts und Binärdateien.

Funktionen

• Programmerkundung: Manticore kann ein Programm mit symbolischen Eingaben ausführen und alle möglichen Zustände erkunden, die es erreichen kann
• Eingabegenerierung: Manticore kann automatisch konkrete Eingaben erzeugen, die zu einem bestimmten Programmzustand führen
• Fehlererkennung: Manticore kann Abstürze und andere Fehlerfälle in Binärdateien und Smart Contracts erkennen
• Instrumentierung: Manticore ermöglicht eine feingranulare Steuerung der Zustandserkundung durch Ereignisrückrufe und Instruktions-Hooks
• Programmierschnittstelle: Manticore bietet programmatischen Zugriff auf seine Analyse-Engine über eine Python-API

Manticore kann folgende Programmtypen analysieren:

• Ethereum-Smart-Contracts (EVM-Bytecode)
• Linux-ELF-Binärdateien (x86, x86_64, aarch64 und ARMv7)
• WASM-Module

Installation

Hinweis: Wir empfehlen, Manticore in einer virtuellen Umgebung zu installieren, um Konflikte mit anderen Projekten oder Paketen zu vermeiden.

Option 1: Installation von PyPI:

pip install manticore

Option 2: Installation von PyPI mit zusätzlichen Abhängigkeiten zur Ausführung nativer Binärdateien:

pip install "manticore[native]"

Option 3: Installation eines nächtlichen Entwicklungsbuilds:

pip install --pre "manticore[native]"

Option 4: Installation aus dem master-Branch:

git clone https://github.com/trailofbits/manticore.git
cd manticore
pip install -e ".[native]"

Option 5: Installation über Docker:

docker pull trailofbits/manticore

Nach der Installation stehen das CLI-Tool manticore und die Python-API zur Verfügung.

Für eine Entwicklungsinstallation siehe unser Wiki.

Verwendung

CLI

Manticore verfügt über eine Befehlszeilenschnittstelle, die eine grundlegende symbolische Analyse einer Binärdatei oder eines Smart Contracts durchführen kann. Die Analyseergebnisse werden in einem Arbeitsbereichsverzeichnis abgelegt, das mit mcore_ beginnt. Informationen zum Arbeitsbereich finden Sie im Wiki.

EVM

Die Manticore CLI erkennt automatisch, dass Sie einen Vertrag testen möchten, wenn (z. B.) der Vertrag die Erweiterung .sol oder .vy hat. Siehe eine Demo.

$ manticore examples/evm/umd_example.sol 
 [9921] m.main:INFO: Registered plugins: DetectUninitializedMemory, DetectReentrancySimple, DetectExternalCallAndLeak, ...
 [9921] m.e.manticore:INFO: Starting symbolic create contract
 [9921] m.e.manticore:INFO: Starting symbolic transaction: 0
 [9921] m.e.manticore:INFO: 4 alive states, 6 terminated states
 [9921] m.e.manticore:INFO: Starting symbolic transaction: 1
 [9921] m.e.manticore:INFO: 16 alive states, 22 terminated states
[13761] m.c.manticore:INFO: Generated testcase No. 0 - STOP(3 txs)
[13754] m.c.manticore:INFO: Generated testcase No. 1 - STOP(3 txs)
...
[13743] m.c.manticore:INFO: Generated testcase No. 36 - THROW(3 txs)
[13740] m.c.manticore:INFO: Generated testcase No. 37 - THROW(3 txs)
[9921] m.c.manticore:INFO: Results in ~/manticore/mcore_gsncmlgx

Manticore-verifier

Ein alternatives CLI-Werkzeug wird bereitgestellt, das das Testen von Verträgen vereinfacht und das Schreiben von Eigenschaftsmethoden in derselben Hochsprache wie der Vertrag ermöglicht. Schauen Sie sich die Dokumentation zu manticore-verifier an. Siehe eine Demo

Native

$ manticore examples/linux/basic
[9507] m.n.manticore:INFO: Loading program examples/linux/basic
[9507] m.c.manticore:INFO: Generated testcase No. 0 - Program finished with exit status: 0
[9507] m.c.manticore:INFO: Generated testcase No. 1 - Program finished with exit status: 0
[9507] m.c.manticore:INFO: Results in ~/manticore/mcore_7u7hgfay
[9507] m.n.manticore:INFO: Total time: 2.8029580116271973

API

Manticore bietet eine Python-Programmierschnittstelle, mit der leistungsstarke benutzerdefinierte Analysen implementiert werden können.

EVM

Für Ethereum-Smart-Contracts kann die API für die detaillierte Verifikation beliebiger Vertragseigenschaften verwendet werden. Benutzer können die Startbedingungen festlegen, symbolische Transaktionen ausführen und dann entdeckte Zustände überprüfen, um Invarianten für einen Vertrag sicherzustellen.

from manticore.ethereum import ManticoreEVM
contract_src="""
contract Adder {
    function incremented(uint value) public returns (uint){
        if (value == 1)
            revert();
        return value + 1;
    }
}
"""
m = ManticoreEVM()

user_account = m.create_account(balance=10000000)
contract_account = m.solidity_create_contract(contract_src,
                                              owner=user_account,
                                              balance=0)
value = m.make_symbolic_value()

contract_account.incremented(value)

for state in m.ready_states:
    print("can value be 1? {}".format(state.can_be_true(value == 1)))
    print("can value be 200? {}".format(state.can_be_true(value == 200)))

Native

Es ist auch möglich, die API zu verwenden, um benutzerdefinierte Analysetools für Linux-Binärdateien zu erstellen. Die Anpassung des Anfangszustands hilft, Probleme mit der Zustandsexplosion zu vermeiden, die bei Verwendung der CLI häufig auftreten.

# example Manticore script
from manticore.native import Manticore

m = Manticore.linux('./example')

@m.hook(0x400ca0)
def hook(state):
  cpu = state.cpu
  print('eax', cpu.EAX)
  print(cpu.read_int(cpu.ESP))

  m.kill()  # tell Manticore to stop

m.run()

WASM

Manticore kann auch WebAssembly-Funktionen mit symbolischen Eingaben für die Eigenschaftsvalidierung oder allgemeine Analyse auswerten.

from manticore.wasm import ManticoreWASM

m = ManticoreWASM("collatz.wasm")