Avertissement
Cet article n'est pas une évaluation de l'efficacité des analyseurs automatiques. Je les applique à mes propres contrats, synthétisant intentionnellement des erreurs et étudie les réactions. Une telle étude ne peut pas être la base pour déterminer «mieux-pire», pour cela il est logique de mener une étude en aveugle sur un large échantillon de contrats, ce qui, étant donné la nature capricieuse de ce type de logiciel, est extrêmement difficile à mener. Il est tout à fait possible qu'une petite erreur dans le contrat puisse désactiver une grande partie de la logique de l'analyseur, et un simple signe heuristique peut ajouter une énorme quantité de points à l'analyseur en trouvant un bogue répandu que les concurrents n'ont tout simplement pas réussi à ajouter. Des erreurs dans la préparation et la compilation des contrats peuvent également jouer un rôle. Tous les logiciels en question sont assez jeunes et sont constamment développés, donc ne prenez pas les commentaires critiques comme des problèmes irréparables.
Le but de l'article est de donner au lecteur une compréhension du fonctionnement des méthodes d'analyse de code dans différents analyseurs et la capacité de les utiliser correctement, plutôt que de «faire un choix». Un choix raisonnable consiste à utiliser plusieurs outils à la fois, en se concentrant sur le plus approprié pour le contrat analysé.
Configuration et préparation pour le lancement
Mythril utilise plusieurs types d'analyses à la fois, voici quelques bons articles à ce sujet: le plus important , ceci ou cela . Avant de continuer, il est logique de les lire.
Tout d'abord, construisons notre propre image Docker de Mythril (peu importe ce que nous voulons y changer?):
git clone https://github.com/ConsenSys/mythril-classic.git cd mythril-classic docker build -t myth .
Essayez maintenant de l'exécuter sur nos contracts/flattened.sol (j'utilise le même contrat qui a été discuté dans l' introduction ), dans lequel il y a deux contrats principaux, Ownable de Zeppelin et notre Booking . Nous avons toujours un problème avec la version du compilateur, je l'ai corrigé de la même manière que dans l'article précédent, en ajoutant des lignes au Dockerfile qui remplaceront la version du compilateur:
COPY --from=ethereum/solc:0.4.20 /usr/bin/solc /usr/bin
Après avoir reconstruit l'image, vous pouvez essayer d'exécuter l'analyse de contrat. -v4 immédiatement les -v4 et --verbose-report pour voir tous les avertissements. C'est parti:
docker run -v $(pwd):/tmp \ -w /tmp myth:latest \ -v4 \ --verbose-report \ -x contracts/flattened.sol
Ici, nous travaillons avec un contrat aplati sans dépendances. Pour analyser un contrat Booking.sol distinct et pour que Mythril récupère toutes les dépendances, vous pouvez utiliser quelque chose comme ceci:
docker run -v $(pwd):/tmp \ -w /tmp myth:latest \ --solc-args="--allow-paths /tmp/node_modules/zeppelin-solidity/ zeppelin-solidity=/tmp/node_modules/zeppelin-solidity" \ -v4 \ --verbose-report \ -x contracts/Booking.sol
Je préfère travailler avec l'option aplatie, car nous allons beaucoup modifier le code. Mais Mythril a également un mode extrêmement pratique - --truffle , qui --truffle simplement tout ce que la truffle , vérifiant l'ensemble du projet pour les vulnérabilités. Une autre caractéristique importante est la possibilité de spécifier le nom du contrat à analyser via deux points, sinon Mythril analysera tous les contrats qu'il rencontre. Nous pensons que l' Ownable de OpenZeppelin est un contrat sécurisé, et nous allons seulement analyser la Booking , donc la dernière ligne à exécuter est:
docker run -v $(pwd):/tmp -w /tmp myth:latest -x contracts/flattened.sol:Booking -v4 --verbose-report
Démarrer et déployer le contrat
Nous démarrons l'analyseur avec la ligne ci-dessus, regardons la sortie, et nous obtenons, entre autres, cette ligne:
mythril.laser.ethereum.svm [WARNING]: No contract was created during the execution of contract creation Increase the resources for creation execution (--max-depth or --create-timeout) The analysis was completed successfully. No issues were detected.
Il s'avère que notre contrat n'a pas été créé et "corrigé" dans l'émulateur. C'est pourquoi je recommande d'utiliser l'indicateur -v4 pour tous les types d'analyse pour voir tous les messages et ne pas en rater un seul important. Voyons ce qui ne va pas. La solution à ce problème pratique est très importante pour comprendre comment utiliser correctement Mythril.
Nous lisons donc à propos de Mythril: It uses concolic analysis, taint analysis and control flow checking to detect a variety of security vulnerabilities . Si vous n'êtes pas très familier avec ces termes, je recommande le wiki sur les tests concoliques ici , mais voici une bonne présentation sur la vérification des taches pour x86. En bref: Mythril émule l'exécution d'un contrat, fixe les branches le long desquelles l'exécution peut aller et essaie d'atteindre un état «cassé» du contrat, triant diverses combinaisons de paramètres et essayant de contourner tous les chemins possibles. Voici un exemple de diagramme d'action de l'article ci-dessus:
1. . symbolic-, . 2. , , trace . , , . 3. . 4. trace-. 5. symbolic execution trace, symbolic , , , . 6. , . , . 7. : , , input-, , . input- , .6 . 8. .4
Si vous le simplifiez grandement, Mythril, après avoir rencontré une branche dans le code, peut comprendre sous quels ensembles de variables il est possible d'entrer dans l'une et l'autre branche. Dans chaque branche, Mythril sait si cela conduit à assert , transfer , selfdestruct et autres opcodes liés à la sécurité. Par conséquent, Mythril analyse quels ensembles de paramètres et de transactions peuvent entraîner une violation de la sécurité. Et la façon dont Mythril coupe les branches qui ne sont jamais contrôlées et analyse le flux de contrôle est sa principale astuce. Plus de détails sur l'intestin de Mythril et la marche des branches sont écrits ici .
En raison de la nature déterministe de l'exécution intelligente des contrats, la même séquence d'instructions entraîne toujours strictement un seul ensemble de changements d'état, quelle que soit la plate-forme, l'architecture ou l'environnement. De plus, les fonctions dans les contrats intelligents sont plutôt courtes et les ressources sont extrêmement limitées, donc les analyseurs comme Mythril, combinant exécution symbolique et native, peuvent fonctionner extrêmement efficacement pour les contrats intelligents.
Dans le processus, Mythril utilise le concept "d'état" - c'est le code du contrat, son environnement, un pointeur vers la commande actuelle, le stockage du contrat et l'état de la pile. Voici la documentation:
The machine state μ is defined as the tuple (g, pc, m, i, s) which are the gas available, the program counter pc ∈ P256, the memory contents, the active number of words in memory (counting continuously from position 0), and the stack contents. The memory contents μm are a series of zeroes of size 256.
Le graphe de transition entre les états est le principal objet d'étude. En cas de lancement réussi de l'analyse, des informations sur ce graphique sont affichées dans le journal d'analyse. De plus, Mythril peut construire ce graphique sous une forme lisible par l'homme en utilisant l'option --graph .
Maintenant, en comprenant plus ou moins ce que Mythril fera, nous continuerons de comprendre pourquoi le contrat n'est pas analysé et d'où il vient. [WARNING]: No contract was created during the execution of contract creation . Pour commencer, j'ai tordu les --max-depth --create-timeout et --max-depth (comme recommandé) et, n'obtenant pas le résultat, je pensais que le constructeur était à blâmer - quelque chose ne fonctionnait pas. Voici son code:
function Booking( string _description, string _fileUrl, bytes32 _fileHash, uint256 _price, uint256 _cancellationFee, uint256 _rentDateStart, uint256 _rentDateEnd, uint256 _noCancelPeriod, uint256 _acceptObjectPeriod ) public payable { require(_price > 0); require(_price > _cancellationFee); require(_rentDateStart > getCurrentTime()); require(_rentDateEnd > _rentDateStart); require(_rentDateStart+_acceptObjectPeriod < _rentDateEnd); require(_rentDateStart > _noCancelPeriod); m_description = _description; m_fileUrl = _fileUrl; m_fileHash = _fileHash; m_price = _price; m_cancellationFee = _cancellationFee; m_rentDateStart = _rentDateStart; m_rentDateEnd = _rentDateEnd; m_noCancelPeriod = _noCancelPeriod; m_acceptObjectPeriod = _acceptObjectPeriod; }
Rappelez-vous l'algorithme d'action de Mythril. Pour exécuter la trace, vous devez appeler le constructeur du contrat, car toute exécution ultérieure dépendra des paramètres avec lesquels le constructeur a été appelé. Par exemple, si vous appelez le constructeur avec _price == 0 , le constructeur require(_price > 0) une exception sur require(_price > 0) . Même si Mythril parcourt les nombreuses valeurs de _price , le constructeur _price toujours si, par exemple, _price <= _cancellationFee . Dans ce contrat, il y a une douzaine de paramètres associés à des restrictions strictes, et Mythril, bien sûr, ne peut pas deviner les combinaisons valides de paramètres. Il essaie d'aller à la prochaine branche d'exécution, triant les paramètres du constructeur, mais il n'a pratiquement aucune chance de deviner - il y a trop de combinaisons de paramètres. Par conséquent, le calcul du contrat ne fonctionne pas - toutes les façons reposent sur une sorte d' require(...) , et nous obtenons le problème ci-dessus.
Maintenant, nous avons deux façons: la première consiste à désactiver tous les éléments require dans le constructeur en les commentant. Mythril pourra alors appeler le constructeur avec n'importe quel ensemble de paramètres et tout fonctionnera. Mais cela signifie qu'en examinant un contrat avec de tels paramètres, Mythril trouvera des erreurs possibles avec des valeurs incorrectes transmises au constructeur. En termes simples, si Mythril trouve un bogue qui survient si le créateur du contrat spécifie _cancellationFee un milliard de fois le prix de location de _mprice , alors il n'y a aucune utilité dans un tel bogue - un tel contrat ne sera jamais bloqué et les ressources pour trouver des erreurs seront dépensées. Nous supposons que le contrat est toujours bloqué avec des paramètres plus ou moins cohérents, donc pour une analyse plus approfondie, il est logique de spécifier des paramètres de constructeur plus réalistes afin que Mythril ne recherche pas les erreurs qui ne se produiront jamais si le contrat est correctement clôturé.
J'ai passé de nombreuses heures à essayer de comprendre exactement où le déploiement s'arrête, y compris et à désactiver diverses parties du constructeur. En plus de mes problèmes, le constructeur utilise getCurrentTime() , qui retourne l'heure actuelle, et on ne sait pas comment cet appel gère Mythril. Je ne décrirai pas ces aventures ici, car très probablement avec une utilisation régulière, ces subtilités seront connues de l'auditeur. Par conséquent, j'ai choisi la deuxième façon: pour limiter les données d'entrée, et simplement supprimé tous les paramètres du constructeur, même getCurrentTime() , simplement codé en dur les paramètres nécessaires directement dans le constructeur (idéalement, ces paramètres devraient être obtenus auprès du client):
function Booking( ) public payable { m_description = "My very long booking text about hotel and beautiful sea view!"; m_fileUrl = "https://ether-airbnb.bam/some-url/"; m_fileHash = 0x1628f3170cc16d40aad2e8fa1ab084f542fcb12e75ce1add62891dd75ba1ffd7; m_price = 1000000000000000000; // 1 ETH m_cancellationFee = 100000000000000000; // 0.1 ETH m_rentDateStart = 1550664800 + 3600 * 24; // current time + 1 day m_rentDateEnd = 1550664800 + 3600 * 24 * 4; // current time + 4 days m_acceptObjectPeriod = 3600 * 8; // 8 hours m_noCancelPeriod = 3600 * 24; // 1 day require(m_price > 0); require(m_price > m_cancellationFee); require(m_rentDateStart > 1550664800); require(m_rentDateEnd > m_rentDateStart); require((m_rentDateStart + m_acceptObjectPeriod) < m_rentDateEnd); require(m_rentDateStart > m_noCancelPeriod); }
De plus, pour que tout commence, vous devez également définir le paramètre max-depth . Cela a fonctionné pour moi avec ce constructeur avec --max-depth=34 sur l'instance AWS t2.medium. Dans le même temps, sur mon ordinateur portable, qui est plus puissant, tout commence sans max-depth . A en juger par l'utilisation de ce paramètre , il est nécessaire de construire des branches pour l'analyse, et sa valeur par défaut est l'infini ( code ). Par conséquent, tournez-tournez ce paramètre, mais assurez-vous que le contrat souhaité est analysé. Vous pouvez comprendre cela par des messages comme:
mythril.laser.ethereum.svm [INFO]: 248 nodes, 247 edges, 2510 total states mythril.laser.ethereum.svm [INFO]: Achieved 59.86% coverage for code: .............
La première ligne décrit simplement le graphique qui sera analysé, lisez vous-même le reste des lignes. De sérieuses ressources informatiques sont nécessaires pour analyser les différentes branches qui peuvent être exécutées, donc lors de l'analyse de gros contrats, vous devrez attendre même sur un ordinateur rapide.
Rechercher des erreurs
Nous allons maintenant rechercher les erreurs et ajouter les nôtres. Mythril recherche les branches dans lesquelles se déroulent la diffusion, l'autodestruction, l'affirmation et d'autres actions importantes du point de vue de la sécurité. Si l'une des instructions ci-dessus apparaît quelque part dans le code du contrat, Mythril examine les façons dont il est possible de se rendre dans cette agence et, de plus, affiche la séquence des transactions menant à cette agence!
Tout d'abord, voyons ce que Mythril a émis pour le contrat de Booking longue durée. Premier avertissement:
==== Dependence on predictable environment variable ==== SWC ID: 116 Severity: Low Contract: Booking Function name: fallback PC address: 566 Estimated Gas Usage: 17908 - 61696 Sending of Ether depends on a predictable variable. The contract sends Ether depending on the values of the following variables: - block.timestamp Note that the values of variables like coinbase, gaslimit, block number and timestamp are predictable and/or can be manipulated by a malicious miner. Don't use them for random number generation or to make critical decisions. -------------------- In file: contracts/flattened.sol:142 msg.sender.transfer(msg.value-m_price)
et cela se produit parce que
require(m_rentDateStart > getCurrentTime());
dans la fonction de secours.
Notez que Mythril a réalisé que getCurrentTime() cache dans getCurrentTime() . Malgré le fait que le sens du contrat n'est pas une erreur, le fait que Mythril associe block.timestamp à la diffusion est excellent! Dans ce cas, le programmeur doit comprendre que la décision est prise sur la base de la valeur que le mineur peut contrôler. Et, si à l'avenir une enchère ou une autre enchère pour un service survient à ce lieu du contrat, il faut tenir compte de la possibilité d'attaques en cours.
Voyons si Mythril voit une dépendance à block.timestamp si nous cachons la variable dans un appel imbriqué comme ceci:
function getCurrentTime() public view returns (uint256) { - return now; + return getCurrentTimeInner(); } + function getCurrentTimeInner() internal returns (uint256) { + return now; + }
Et oui! Mythril continue de voir la connexion entre block.timestamp et le transfert de diffusion, c'est extrêmement important pour l'auditeur. Le lien entre la variable contrôlée par l'attaquant et la décision prise après plusieurs changements dans l'état du contrat peut être très masqué par la logique, et Mythril vous permet de la suivre. Bien qu'il ne soit pas utile de compter sur le fait que toutes les connexions possibles entre toutes les variables possibles seront getCurrentTime() pour vous: si vous continuez à vous moquer de la fonction getCurrentTime() et à effectuer une triple profondeur d'imbrication, l'avertissement disparaît. Chaque appel de fonction pour Mythril nécessite la création de nouvelles branches d'état, donc l'analyse de niveaux très profonds d'imbrication nécessitera d'énormes ressources.
Il y a, bien sûr, une chance assez sérieuse que j'utilise simplement de manière incorrecte les paramètres d'analyse ou que la coupure se produise quelque part dans les profondeurs de l'analyseur. Comme je l'ai dit, le produit est en développement actif, juste au moment de la rédaction, je vois des commits dans le référentiel avec la mention de max-depth , alors ne prenez pas les problèmes actuels au sérieux, nous avons déjà trouvé suffisamment de preuves que Mythril peut très efficacement rechercher des connexions implicites entre variables.
Tout d'abord, ajoutez au contrat une fonction qui donne la diffusion à n'importe qui, mais seulement après que le client a envoyé la diffusion au contrat. Nous avons permis à quiconque de ramasser 1/5 de l'éther, mais uniquement lorsque le contrat est en State.PAID (c'est-à-dire uniquement après que le client a payé le numéro loué avec de l'éther). Voici la fonction:
function collectTaxes() external onlyState(State.PAID) { msg.sender.transfer(address(this).balance / 5); }
Mythril a trouvé le problème:
==== Unprotected Ether Withdrawal ==== SWC ID: 105 Severity: High Contract: Booking Function name: collectTaxes() PC address: 2492 Estimated Gas Usage: 2135 - 2746 Anyone can withdraw ETH from the contract account. Arbitrary senders other than the contract creator can withdraw ETH from the contract account without previously having sent a equivalent amount of ETH to it. This is likely to be a vulnerability. -------------------- In file: contracts/flattened.sol:149 msg.sender.transfer(address(this).balance / 5) -------------------- -------------------- Transaction Sequence: { "2": { "calldata": "0x", "call_value": "0xde0b6b3a7640000", "caller": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" }, "3": { "calldata": "0x01b613a5", "call_value": "0x0", "caller": "0xdeadbeefdeadbeefdeadbeefdeadbeefdeadbeef" } }
Génial, c'est-à-dire Mythril a même fait ressortir deux transactions, ce qui conduit au fait que vous pouvez retirer de l'éther du contrat. Maintenant, changez l'exigence State.RENT en State.RENT , comme ceci:
- function collectTaxes() external onlyState(State.PAID){ + function collectTaxes() external onlyState(State.RENT) {
Maintenant collectTaxes() ne peut être appelé que lorsque le contrat est dans l'état State.RENT , et pour le moment il n'y a rien sur la balance, car le contrat a déjà envoyé la totalité de l'émission au propriétaire. Et l'important ici est que cette fois, Mythril NE génère PAS l'erreur ==== Unprotected Ether Withdrawal ==== ! Sous la condition onlyState(State.RENT) , l'analyseur n'est pas arrivé à la branche de code qui envoie de l'éther du contrat avec un solde non nul. Mythril est passé par différentes options pour les paramètres, mais vous ne pouvez entrer dans State.RENT qu'en envoyant toute la diffusion au bailleur. Par conséquent, il est impossible d'accéder à cette branche du code avec un solde non nul, et Mythril ne dérange absolument pas l'auditeur!
De la même manière, Mythril trouvera l' selfdestruct et assert , montrant à l'auditeur quelles actions peuvent conduire à la destruction du contrat ou à la rupture d'une fonction importante. Je ne donnerai pas ces exemples, essayez simplement de créer une fonction similaire à celle ci-dessus, en appelant uniquement selfdestruct et en déformant sa logique.
N'oubliez pas non plus que l'une des parties de Mythril est l'exécution symbolique, et cette approche, en elle-même, sans émuler l'exécution, peut déterminer de nombreuses vulnérabilités. Par exemple, toute utilisation de "+", "-" et d'autres opérateurs arithmétiques peut être considérée comme une vulnérabilité de "dépassement d'entier" si l'un des opérandes est en quelque sorte contrôlé par l'attaquant. Mais je répète encore une fois, la caractéristique la plus puissante de Mythril est la combinaison de l'exécution symbolique et native et la détermination des valeurs des paramètres conduisant à une ramification logique.
Conclusion
Bien sûr, pour montrer toute la gamme des problèmes potentiels que Mythril est capable de détecter, il faudra non pas un, mais plusieurs articles. Pour tout le reste, il sait tout faire dans une vraie blockchain, trouvant les contrats et les vulnérabilités nécessaires par des signatures, construisant de beaux graphes d'appels, formatant des rapports. Mythril vous permet également d'écrire vos propres scripts de test, fournissant une interface basée sur python au contrat et vous permettant de tester des fonctions individuelles, de fixer des valeurs de paramètres ou même de mettre en œuvre votre propre stratégie pour travailler avec du code désassemblé avec un degré de flexibilité arbitraire.
Mythril est encore un logiciel assez jeune, ce n'est pas IDA Pro, et il y a très peu de documentation sauf quelques articles. La valeur de nombreux paramètres ne peut être lue que dans le code Mythril, en commençant par cli.py. J'espère qu'une description complète et approfondie du fonctionnement de chaque paramètre apparaîtra dans la documentation.
De plus, lorsque le contrat est plus ou moins volumineux, la sortie d'un tas d'erreurs prend beaucoup de place, mais j'aimerais pouvoir recevoir des informations compressées sur l'erreur trouvée, car lorsque vous travaillez avec Mythril, vous devez absolument regarder le chemin d'analyse, voir quels contrats ont été testés au mieux de vos capacités et être en mesure de désactiver de force des erreurs spécifiques que l'auditeur considère comme faussement positives.
Mais en général, Mythril est un excellent et extrêmement puissant outil d'analyse des contrats intelligents et devrait à l'heure actuelle être dans l'arsenal de tout auditeur. Il vous permet au moins de prêter attention aux parties critiques du code et de détecter les relations cachées entre les variables.
Pour résumer, les recommandations d'utilisation de Mythril sont les suivantes:
- Limitez autant que possible les conditions de départ du contrat à l'étude. Si lors de l'analyse Mythril dépensera beaucoup de ressources sur des branches qui ne seront jamais implémentées en pratique, il perdra la capacité de trouver des bugs vraiment importants, vous devriez donc toujours essayer de restreindre la zone des branches potentielles.
- Assurez-vous que l'analyse des contrats a commencé, ne manquez pas les messages comme
mythril.laser.ethereum.svm [WARNING]: No contract was created during the execution of contract creation Increase the resources for creation execution (--max-depth or --create-timeout) , sinon vous pourriez penser à tort qu'il n'y a pas de bugs. - Vous pouvez désactiver arbitrairement les branches dans le code du contrat, ce qui donne moins de variation à Mythril dans le choix des branches et l'économie de ressources. Essayez de le faire sans restrictions sur la
max-depth , afin de ne pas "couper" l'analyse, mais attention à ne pas masquer l'erreur. - Faites attention à chaque avertissement, même les commentaires légers valent parfois la peine d'ajouter au moins un commentaire au code du contrat, ce qui facilite la tâche des autres développeurs.
Dans le prochain article, nous traiterons de l'analyseur Manticore, mais voici la table des matières des articles prêts ou prévus pour l'écriture:
Partie 1. Introduction. Compilation, aplatissement, versions de Solidity
Partie 2. Slither
Partie 3. Mythril (cet article)
Partie 4. Manticore (pendant l'écriture)
Partie 5. Echidna (pendant l'écriture)