manticore
Manticore 0.3.7
Ce projet n'est plus développé et maintenu en interne. Cependant, nous sommes heureux d'examiner et d'accepter de petites demandes d'extraction bien écrites de la part de la communauté. Nous ne considérerons que les corrections de bugs et les améliorations mineures.
Tous les problèmes et discussions nouveaux ou actuellement ouverts doivent recevoir une réponse et être soutenus par la communauté.
Manticore est un outil d'exécution symbolique pour l'analyse des contrats intelligents et des binaires.
Manticore peut analyser les types de programmes suivants :
Remarque : Nous vous recommandons d'installer Manticore dans un environnement virtuel pour éviter les conflits avec d'autres projets ou packages.
Option 1 : Installation à partir de PyPI :
pip install manticoreOption 2 : Installation à partir de PyPI, avec des dépendances supplémentaires nécessaires pour exécuter les binaires natifs :
pip install " manticore[native] "Option 3 : Installation d'une version de développement nocturne :
pip install --pre " manticore[native] " Option 4 : Installation à partir de la branche master :
git clone https://github.com/trailofbits/manticore.git
cd manticore
pip install -e " .[native] "Option 5 : Installer via Docker :
docker pull trailofbits/manticore Une fois installés, l'outil CLI manticore et l'API Python seront disponibles.
Pour une installation de développement, consultez notre wiki.
Manticore dispose d'une interface de ligne de commande qui peut effectuer une analyse symbolique de base d'un contrat binaire ou intelligent. Les résultats de l'analyse seront placés dans un répertoire d'espace de travail commençant par mcore_ . Pour plus d'informations sur l'espace de travail, consultez le wiki.
Manticore CLI détecte automatiquement que vous essayez de tester un contrat si (par exemple) 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_gsncmlgxUn outil CLI alternatif est fourni pour simplifier les tests de contrat et permettre 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 du vérificateur manticore. 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.8029580116271973Manticore fournit une interface de programmation Python qui peut être utilisée pour implémenter de puissantes analyses personnalisées.
Pour les contrats intelligents Ethereum, l’API peut être utilisée pour une vérification détaillée des propriétés arbitraires du contrat. Les utilisateurs peuvent définir les conditions de départ, exécuter des transactions symboliques, puis examiner les états découverts pour garantir les invariants pour le maintien d'un contrat.
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. La personnalisation de l’état initial permet d’éviter les problèmes d’explosion d’état qui surviennent fréquemment 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 les fonctions WebAssembly sur des entrées symboliques pour la validation des propriétés ou l'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 s'appuie sur un solveur externe supportant smtlib2. Actuellement, Z3, Yices et CVC4 sont pris en charge 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 reviendra à 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, rendez-vous sur 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 à vous arrêter sur notre chaîne 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 sur la façon de démarrer avec Manticore et de contribuer
La référence API contient une documentation plus complète et plus approfondie sur notre API
Le répertoire d'exemples contient quelques petits exemples qui présentent les fonctionnalités de l'API
Le dépôt manticore-examples contient des exemples plus complexes, y compris de vrais problèmes CTF.
Si vous souhaitez déposer un rapport de bug ou une demande de fonctionnalité, veuillez utiliser notre page de problèmes.
Pour des questions et des précisions, 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 le cadre de travaux universitaires, envisagez de postuler au prix de recherche Crytic de 10 000 $.
