trailofbits/manticoreStrumento di esecuzione simbolica
Questo progetto non è più sviluppato e mantenuto internamente.
Manticore è uno strumento di esecuzione simbolica per l'analisi di smart contract e binari.
Manticore può analizzare i seguenti tipi di programmi:
Nota: Si consiglia di installare Manticore in un ambiente virtuale per evitare conflitti con altri progetti o pacchetti
Opzione 1: Installazione da PyPI:
pip install manticore
Opzione 2: Installazione da PyPI, con dipendenze aggiuntive necessarie per eseguire binari nativi:
pip install "manticore[native]"
Opzione 3: Installazione di una build di sviluppo notturna:
pip install --pre "manticore[native]"
Opzione 4: Installazione dal ramo master:
git clone https://github.com/trailofbits/manticore.git
cd manticore
pip install -e ".[native]"
Opzione 5: Installazione tramite Docker:
docker pull trailofbits/manticore
Una volta installato, lo strumento CLI manticore e l'API Python saranno disponibili.
Per un'installazione di sviluppo, consulta il nostro wiki.
Manticore ha un'interfaccia a riga di comando che può eseguire un'analisi simbolica di base di un binario o di uno smart contract. I risultati dell'analisi verranno inseriti in una directory workspace che inizia con mcore_. Per informazioni sul workspace, consulta il wiki.
La CLI di Manticore rileva automaticamente che stai cercando di testare un contratto se (ad es.) il contratto ha estensione .sol o .vy. Vedi una 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
Viene fornito uno strumento CLI alternativo che semplifica il testing dei contratti e permette di scrivere metodi di proprietà nello stesso linguaggio ad alto livello utilizzato dal contratto. Dai un'occhiata alla documentazione di manticore-verifier. Vedi una 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 fornisce un'interfaccia di programmazione Python che può essere utilizzata per implementare potenti analisi personalizzate.
Per gli smart contract Ethereum, l'API può essere utilizzata per la verifica dettagliata di proprietà arbitrarie del contratto. Gli utenti possono impostare le condizioni iniziali, eseguire transazioni simboliche e poi rivedere gli stati scoperti per garantire che gli invarianti di un contratto siano soddisfatti.
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)))
È anche possibile utilizzare l'API per creare strumenti di analisi personalizzati per binari Linux. Personalizzare lo stato iniziale aiuta a evitare problemi di esplosione degli stati che si verificano comunemente quando si utilizza la CLI.
# 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 può anche valutare funzioni WebAssembly su input simbolici per la validazione di proprietà o analisi generale.
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 o passando --ulimit stack=100000000:100000000 a docker runsolc nel tuo $PATH.crytic-compile direttamente sul tuo codice per facilitare l'identificazione di eventuali problemi.Manticore si basa su un solver esterno che supporta smtlib2. Attualmente sono supportati Z3, Yices e CVC4 e possono essere selezionati tramite riga di comando o impostazioni di configurazione. Se Yices è disponibile, Manticore lo utilizzerà per impostazione predefinita. In caso contrario, ricadrà su Z3 o CVC4. Se vuoi scegliere manualmente quale solver utilizzare, puoi farlo in questo modo:
manticore --smt.solver Z3
Per maggiori dettagli vai su https://cvc4.github.io/. Altrimenti, scarica il binario e usalo.
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 è incredibilmente veloce. Maggiori dettagli qui https://yices.csl.sri.com/
sudo add-apt-repository ppa:sri-csl/formal-methods
sudo apt-get update
sudo apt-get install yices2
Sentiti libero di passare dal nostro canale slack #manticore su Empire Hacking per aiuto nell'uso o nell'estensione di Manticore.
La documentazione è disponibile in diversi luoghi:
Il wiki contiene informazioni su come iniziare con Manticore e contribuire
Il riferimento API contiene documentazione più approfondita e dettagliata sulla nostra API
La directory examples contiene alcuni piccoli esempi che mostrano le caratteristiche dell'API
Il repository manticore-examples contiene alcuni esempi più complessi, inclusi alcuni veri problemi CTF
Se desideri segnalare un bug o richiedere una funzionalità, utilizza la nostra pagina issues.
Per domande e chiarimenti, visita la pagina discussion.
Manticore è concesso in licenza e distribuito sotto la licenza AGPLv3. Contattaci se stai cercando un'eccezione ai termini.
Se stai utilizzando Manticore in lavori accademici, considera di candidarti al Crytic $10k Research Prize.
