trailofbits/manticoreSymbolic execution tool
Dieses Projekt wird nicht mehr intern entwickelt und gewartet.
Manticore ist ein Werkzeug zur symbolischen Ausführung für die Analyse von Smart Contracts und Binärdateien.
Manticore kann folgende Programmtypen analysieren:
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.
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.
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
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
$ 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
Manticore bietet eine Python-Programmierschnittstelle, mit der leistungsstarke benutzerdefinierte Analysen implementiert werden können.
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)))
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()
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")
def arg_gen(state):
# Generate a symbolic argument to pass to the collatz function.
# Possible values: 4, 6, 8
arg = state.new_symbolic_value(32, "collatz_arg")
state.constrain(arg > 3)
state.constrain(arg < 9)
state.constrain(arg % 2 == 0)
return [arg]
# Run the collatz function with the given argument generator.
m.collatz(arg_gen)
# Manually collect return values
# Prints 2, 3, 8
for idx, val_list in enumerate(m.collect_returns()):
print("State", idx, "::", val_list[0])
ulimit -s 100000 oder durch Übergabe von --ulimit stack=100000000:100000000 an docker run erfolgensolc in Ihrem $PATH.crytic-compile direkt auf Ihren Code anzuwenden, um Probleme leichter zu identifizieren.Manticore verwendet einen externen Löser, der smtlib2 unterstützt. Derzeit werden Z3, Yices und CVC4 unterstützt und können über die Befehlszeile oder Konfigurationseinstellungen ausgewählt werden.
Wenn Yices verfügbar ist, wird Manticore es standardmäßig verwenden. Falls nicht, fällt es auf Z3 oder CVC4 zurück. Wenn Sie manuell auswählen möchten, welcher Löser verwendet werden soll, können Sie dies wie folgt tun:
manticore --smt.solver Z3
Weitere Details finden Sie unter https://cvc4.github.io/. Andernfalls laden Sie einfach die Binärdatei herunter und verwenden Sie sie.
sudo wget -O /usr/bin/cvc4 https://github.com/CVC4/CVC4/releases/download/1.7/cvc4-1.7-x86_64-linux-opt
sudo chmod +x /usr/bin/cvc4
Yices ist unglaublich schnell. Weitere Details finden Sie unter https://yices.csl.sri.com/
sudo add-apt-repository ppa:sri-csl/formal-methods
sudo apt-get update
sudo apt-get install yices2
Besuchen Sie gerne unseren #manticore-Slack-Kanal im Empire Hacking für Hilfe bei der Verwendung oder Erweiterung von Manticore.
Dokumentation ist an mehreren Stellen verfügbar:
Das Wiki enthält Informationen zum Einstieg in Manticore und zum Beitragen
Die API-Referenz enthält ausführlichere und tiefgehendere Dokumentation zu unserer API
Das Verzeichnis Beispiele enthält einige kleine Beispiele, die API-Funktionen vorstellen
Das Repository manticore-examples enthält einige komplexere Beispiele, darunter echte CTF-Probleme
Wenn Sie einen Fehlerbericht oder eine Funktionsanfrage einreichen möchten, nutzen Sie bitte unsere Issues-Seite.
Für Fragen und Klarstellungen besuchen Sie bitte die Diskussionsseite.
Manticore ist unter der AGPLv3-Lizenz lizenziert und verteilt. Kontaktieren Sie uns, wenn Sie nach einer Ausnahme zu den Bedingungen suchen.
Wenn Sie Manticore in akademischen Arbeiten verwenden, ziehen Sie eine Bewerbung für den Crytic $10k Research Prize in Betracht.
