solidity static analysis
Alpha
Analyse statique pour la vérification des contrats intelligents de Solidity, basé sur https://github.com/shaunazzopardi/solidity-cfg-builder et https://github.com/gordonpace/contractlarva.
Cet outil tente de prouver pleinement les propriétés des contrats intelligents de Solidity et, sur un succès partiel, renvoie une propriété résiduelle qui reste à prouver le contrat Smart Smart.
Nous utilisons une représentation de graphe de flux de contrôle d'un contrat intelligent Solidity dans le but de prouver les propriétés des contrats intelligents statiquement en surproduisant le flux de contrôle d'un contrat intelligent Solidity (basé sur Solidity-CFG-Builder, et son état variable.
Ceci est en partie basé sur les travaux présentés dans les actes de Prepost 2017, dans la série EPCTS, et disponible sur ArXIV.
Chaque fonction de contrat intelligent est représentée comme un automate à flux de contrôle (CFA) avec des transitions marquées avec un triple contenant: (i) une condition sur l'état variable du programme; (ii) une déclaration qui transforme l'état variable du programme; et (iii) un événement de propriété activé lors de l'exécution de la déclaration.
Chacun de ces automates est augmenté de transitions abstraites (taguées uniquement par un événement de propriété) qui permet à tout événement de se produire lorsqu'il est initial, d'appel ou d'état final du programme. Ceci est utilisé comme base de l'analyse intraprocédurale. Chacun de ces automates déploie toutes les exécutions du contrat intelligent qui appellent la fonction correspondante. Cet automate est appelé automate de contrôle de contrôle abstrait (ACFA).
Un algorithme de propagation de l'affirmation simple propage des affirmations sur l'état variable du programme (impliqué par les conditions et les déclarations) via les états explicites d'un CFA jusqu'à ce que les déclarations qui peuvent affecter l'affirmation soient rencontrées. C'est le son.
Une propriété est représentée comme un événement dynamique Automaton (DEA) qui utilise des transitions marquées avec un triple de: (i) un événement; (ii) un garde à l'état variable de la propriété; et (iii) une action sur l'état variable de la propriété.
Un ACFA avec une abstraction variable est composé de DEA, produisant un système surveillé abstrait (AMS) avec des transitions marquées avec des paires de transitions CFA et DEA, ou avec l'une des positions contenant le symbole #. Lorsque # est utilisé à la place d'une transition CFA, il signale la correspondance d'une transition abstraite, tandis qu'au lieu d'une transition DEA, il ne signale pas de correspondance de transition DEA.
Ensuite, un AMS est créé pour chaque fonction du programme contre la DEA donnée.
Un solveur SMT, Z3, est appelé à la volée lors de la construction de l'AMS pour déterminer s'il est possible pour la transition donnée s d'activer à ce moment-là dans une véritable course. Compte tenu d'une paire de transition CFA-DEA, nous vérifions que la garde DEA peut tenir vrai sur l'abstraction variable de l'état source mise à jour avec la condition et la déclaration de la transition CFA. Alors que la paire CFA- # #, nous vérifions que l'abstraction variable de l'état source mise à jour avec la condition et l'énoncé de la transition CFA n'est pas incompatible avec la négation de la disjonction des gardes de la transition DEA éventuellement activés à ce point (notez que les transitions DEA ouvrirent à partir du même état DEA sont assurées pour avoir des gardiens musicaux).
Chaque AMS est analysée pour identifier les paires de transition CFA-DEA, en extraction des transitions DEA utilisées de cette manière, ignorant les correspondances de transitions DEA avec l'espace-chargement #. L'union de ces transitions DEA produit un résidu de la DEA originale. Cela peut parfois être encore réduit par l'analyse syntatique de la DEA résiduelle.
De plus, à partir de l'AMSS, nous pouvons identifier lorsque le garde d'une transition DEA peut être supprimé (c'est-à-dire changé en vrai ), c'est-à-dire chaque fois qu'il peut être utilisé dans l'AMS, il est toujours utilisé.
Si le résidu produit n'a pas de transitions, la propriété a été prouvée.
Exigences: Cabal v2.4. * (Par exemple, installer la plate-forme Haskell complète)
Compilation: suivez les instructions ici
Pour les résultats corrects, assurez-vous toujours que le code de solidité se compile avec un compilateur de solidité.
Pour utiliser l'outil, passez l'emplacement du fichier Smart Contrat Solidity, le fichier de propriété DEA et l'emplacement préféré de la sortie à l'exécutable, par exemple: exécuter:
./Main "./examples/courierservice.sol" "./examples/courierservicespe.dea" "cfa.txt" "acfa.txt" "ams.txt" "résiduel.dea"
Ce projet est concédé sous licence de la licence Apache 2.0.
