trailofbits/manticoreSymbolic execution tool
Ce projet n'est plus développé ni maintenu en interne.
Manticore est un outil d'exécution symbolique pour l'analyse de contrats intelligents et de binaires.
Manticore peut analyser les types de programmes suivants :
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.
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.
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
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
$ 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 fournit une interface de programmation Python qui peut être utilisée pour implémenter des analyses personnalisées puissantes.
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)))
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()
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
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 ou en passant --ulimit stack=100000000:100000000 à docker runsolc dans votre $PATH.crytic-compile directement sur votre code pour faciliter l'identification des problèmes.Manticore repose sur un solveur externe supportant smtlib2. Actuellement, Z3, Yices et CVC4 sont supportés et peuvent être sélectionnés via la ligne de commande ou les paramètres de configuration. Si Yices est disponible, Manticore l'utilisera par défaut. Sinon, il utilisera Z3 ou CVC4. Si vous souhaitez choisir manuellement le solveur à utiliser, vous pouvez le faire comme ceci :
manticore --smt.solver Z3
Pour plus de détails, consultez https://cvc4.github.io/. Sinon, récupérez simplement le binaire et utilisez-le.
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 est incroyablement rapide. Plus de détails ici https://yices.csl.sri.com/
sudo add-apt-repository ppa:sri-csl/formal-methods
sudo apt-get update
sudo apt-get install yices2
N'hésitez pas à passer par notre canal Slack #manticore dans Empire Hacking pour obtenir de l'aide sur l'utilisation ou l'extension de Manticore.
La documentation est disponible à plusieurs endroits :
Le wiki contient des informations pour commencer avec Manticore et contribuer
La référence de l'API contient une documentation plus complète et approfondie sur notre API
Le répertoire examples contient quelques petits exemples qui montrent les fonctionnalités de l'API
Le dépôt manticore-examples contient des exemples plus complexes, y compris de vrais problèmes de CTF
Si vous souhaitez soumettre un rapport de bogue ou une demande de fonctionnalité, veuillez utiliser notre page issues.
Pour les questions et clarifications, veuillez visiter la page de discussion.
Manticore est sous licence et distribué sous la licence AGPLv3. Contactez-nous si vous recherchez une exception aux conditions.
Si vous utilisez Manticore dans un cadre académique, envisagez de postuler au Crytic $10k Research Prize.
