⚠️ Progetto archiviato ⚠️

Questo progetto non è più sviluppato e mantenuto internamente.

Manticore

Manticore è uno strumento di esecuzione simbolica per l'analisi di smart contract e binari.

Caratteristiche

• Esplorazione dei programmi: Manticore può eseguire un programma con input simbolici ed esplorare tutti gli stati possibili che può raggiungere
• Generazione di input: Manticore può produrre automaticamente input concreti che portano a un dato stato del programma
• Scoperta di errori: Manticore può rilevare crash e altri casi di fallimento in binari e smart contract
• Strumentazione: Manticore fornisce un controllo granulare dell'esplorazione degli stati tramite callback di eventi e hook di istruzioni
• Interfaccia programmatica: Manticore espone accesso programmatico al suo motore di analisi tramite un'API Python

Manticore può analizzare i seguenti tipi di programmi:

• Smart contract Ethereum (bytecode EVM)
• Binari Linux ELF (x86, x86_64, aarch64 e ARMv7)
• Moduli WASM

Installazione

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.

Utilizzo

CLI

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.

EVM

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

Manticore-verifier

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

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 fornisce un'interfaccia di programmazione Python che può essere utilizzata per implementare potenti analisi personalizzate.

EVM

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)))

Native

È 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()

WASM

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")