⚠️ Projet archivé ⚠️

Ce projet n'est plus développé ni maintenu en interne.

Manticore

Manticore est un outil d'exécution symbolique pour l'analyse de contrats intelligents et de binaires.

Fonctionnalités

• Exploration de programmes : Manticore peut exécuter un programme avec des entrées symboliques et explorer tous les états possibles qu'il peut atteindre
• Génération d'entrées : Manticore peut produire automatiquement des entrées concrètes qui mènent à un état de programme donné
• Détection d'erreurs : Manticore peut détecter les crashs et autres cas d'échec dans les binaires et les contrats intelligents
• Instrumentation : Manticore offre un contrôle fin de l'exploration des états via des rappels d'événements et des hooks d'instructions
• Interface programmatique : Manticore expose un accès programmatique à son moteur d'analyse via une API Python

Manticore peut analyser les types de programmes suivants :

• Contrats intelligents Ethereum (bytecode EVM)
• Binaires Linux ELF (x86, x86_64, aarch64 et ARMv7)
• Modules WASM

Installation

Note : Nous recommandons d'installer Manticore dans un environnement virtuel pour éviter les conflits avec d'autres projets ou paquets

Option 1 : Installation depuis PyPI :

pip install manticore

Option 2 : Installation depuis PyPI, avec dépendances supplémentaires nécessaires pour exécuter des binaires natifs :

pip install "manticore[native]"

Option 3 : Installation d'une version de développement nightly :

pip install --pre "manticore[native]"

Option 4 : Installation depuis la branche master :

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

Option 5 : Installation via Docker :

docker pull trailofbits/manticore

Une fois installé, l'outil en ligne de commande manticore et l'API Python seront disponibles.

Pour une installation de développement, consultez notre wiki.

Utilisation

CLI

Manticore dispose d'une interface en ligne de commande qui peut effectuer une analyse symbolique de base d'un binaire ou d'un contrat intelligent. Les résultats de l'analyse seront placés dans un répertoire de travail commençant par mcore_. Pour plus d'informations sur l'espace de travail, consultez le wiki.

EVM

La CLI de Manticore détecte automatiquement que vous essayez de tester un contrat si (par ex.) le contrat a une extension .sol ou .vy. Voir une démo.

$ 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

Un outil CLI alternatif est fourni qui simplifie les tests de contrats et permet d'écrire des méthodes de propriétés dans le même langage de haut niveau que celui utilisé par le contrat. Consultez la documentation de manticore-verifier. Voir une démo

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 fournit une interface de programmation Python qui peut être utilisée pour implémenter des analyses personnalisées puissantes.

EVM

Pour les contrats intelligents Ethereum, l'API peut être utilisée pour une vérification détaillée des propriétés arbitraires des contrats. Les utilisateurs peuvent définir les conditions de départ, exécuter des transactions symboliques, puis examiner les états découverts pour s'assurer que les invariants d'un contrat sont respectés.

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

Il est également possible d'utiliser l'API pour créer des outils d'analyse personnalisés pour les binaires Linux. Adapter l'état initial permet d'éviter les problèmes d'explosion d'état qui surviennent couramment lors de l'utilisation de 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 peut également évaluer des fonctions WebAssembly sur des entrées symboliques pour la validation de propriétés ou une analyse générale.

from manticore.wasm import ManticoreWASM