manticore
Manticore 0.3.7
Dieses Projekt wird nicht mehr intern entwickelt und gepflegt. Wir prüfen und akzeptieren jedoch gerne kleine, gut geschriebene Pull-Requests der Community. Wir berücksichtigen nur Fehlerbehebungen und kleinere Verbesserungen.
Alle neuen oder derzeit offenen Fragen und Diskussionen werden von der Community beantwortet und unterstützt.
Manticore ist ein symbolisches Ausführungstool für die Analyse von Smart Contracts und Binärdateien.
Manticore kann die folgenden Arten von Programmen 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 manticoreOption 2: Installation von PyPI, mit zusätzlichen Abhängigkeiten, die zum Ausführen nativer Binärdateien erforderlich sind:
pip install " manticore[native] "Option 3: Installieren eines nächtlichen Entwicklungs-Builds:
pip install --pre " manticore[native] " Option 4: Installation vom master -Zweig:
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 manticore CLI-Tool und die Python-API zur Verfügung.
Eine Entwicklungsinstallation finden Sie in unserem Wiki.
Manticore verfügt über eine Befehlszeilenschnittstelle, die eine grundlegende symbolische Analyse eines Binär- oder Smart-Vertrags durchführen kann. Die Analyseergebnisse werden in einem Arbeitsbereichsverzeichnis abgelegt, das mit mcore_ beginnt. Informationen zum Arbeitsbereich finden Sie im Wiki.
Manticore CLI erkennt automatisch, dass Sie versuchen, einen Vertrag zu testen, wenn der Vertrag beispielsweise die Erweiterung .sol oder .vy hat. Sehen Sie sich eine Demo an.
$ 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_gsncmlgxEs wird ein alternatives CLI-Tool bereitgestellt, das das Testen von Verträgen vereinfacht und das Schreiben von Eigenschaftsmethoden in derselben Hochsprache ermöglicht, die der Vertrag verwendet. Schauen Sie sich die Manticore-Verifier-Dokumentation an. Sehen Sie sich eine Demo an
$ 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.8029580116271973Manticore stellt eine Python-Programmierschnittstelle zur Verfügung, mit der leistungsstarke individuelle Analysen implementiert werden können.
Für Ethereum-Smart-Verträge kann die API zur detaillierten Überprüfung beliebiger Vertragseigenschaften verwendet werden. Benutzer können die Startbedingungen festlegen, symbolische Transaktionen ausführen und dann die erkannten Zustände überprüfen, um Invarianten für eine Vertragssperre 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. Durch die Anpassung des Anfangszustands können Probleme bei der Zustandsexplosion vermieden werden, die bei der 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 über symbolische Eingaben zur Eigenschaftsvalidierung oder allgemeinen 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 Übergeben von --ulimit stack=100000000:100000000 an docker run erfolgensolc -Programm in Ihrem $PATH erforderlich.crytic-compile direkt für Ihren Code auszuführen, um die Identifizierung etwaiger Probleme zu erleichtern. Manticore verlässt sich auf einen externen Solver, 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. Wenn nicht, wird auf Z3 oder CVC4 zurückgegriffen. Wenn Sie manuell auswählen möchten, welcher Solver verwendet werden soll, können Sie dies wie folgt tun: manticore --smt.solver Z3
Weitere Informationen finden Sie unter https://cvc4.github.io/. Andernfalls holen Sie sich einfach die Binärdatei 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 hier https://yices.csl.sri.com/
sudo add-apt-repository ppa:sri-csl/formal-methods
sudo apt-get update
sudo apt-get install yices2
Schauen Sie gerne in unserem Slack-Kanal #manticore in Empire Hacking vorbei, um Hilfe bei der Verwendung oder Erweiterung von Manticore zu erhalten.
Die Dokumentation ist an mehreren Stellen verfügbar:
Das Wiki enthält Informationen zum Einstieg in Manticore und zum Mitwirken
Die API-Referenz enthält eine ausführlichere und ausführlichere Dokumentation unserer API
Das Beispielverzeichnis enthält einige kleine Beispiele, die API-Funktionen veranschaulichen
Das manticore-examples-Repository enthält einige kompliziertere Beispiele, darunter einige echte CTF-Probleme
Wenn Sie einen Fehlerbericht oder eine Funktionsanfrage einreichen möchten, nutzen Sie bitte unsere Problemseite.
Für Fragen und Erläuterungen besuchen Sie bitte die Diskussionsseite.
Manticore wird unter der AGPLv3-Lizenz lizenziert und vertrieben. Kontaktieren Sie uns, wenn Sie eine Ausnahme von den Bedingungen wünschen.
Wenn Sie Manticore in der akademischen Arbeit verwenden, sollten Sie sich für den Crytic-Forschungspreis in Höhe von 10.000 US-Dollar bewerben.
