Une première pour un géant de l’informatique

Microsoft a récemment annoncé le développement d’un système de vérification des smarts contracts programmés sous le langage de programmation Solidity. Ce projet à été développée grâce à l’équipe de Microsoft Azure Blockchain.

L’outil aura le nom de VeriSol-Verifier for Solidity. L’outil permettra aux développeurs d’écrire des termes pour leurs contrats en utilisant un langage intermédiaire qui pourra ensuite être testé avec de puissantes machines destinées à la résolution de d’équations mathématiques.

“The Microsoft blog states that “the VeriSol team used the verifier to formalize and check specifications of the smart contracts that govern consortium members in Ethereum on Azure and Azure Blockchain Service.”

Le blog de Microsoft indique que “l’équipe VeriSol a utilisé le vérificateur pour formaliser et vérifier les spécifications des contrats intelligents qui régissent les membres du consortium dans Ethereum on Azure et Azure Blockchain Service”.

Une prochaine mise en service annoncée

Actuellement testé en tant que prototype et constatant les atouts de la technologie basée sur Ethereum en termes de sécurité, l’équipe a l’objectif de compléter la plupart des applications d’entreprise des contrats intelligents. Ce projet est le fruit d’un partenariat entre les équipes Azure Blockchain et Research de Microsoft.

Assumant le fait que la sécurité est le nerf sensible des contrats intelligents comme en témoigne l’uniformité du vol de cryptogrammes et des piratages de change, la vérification formelle permet aux développeurs de vérifier la sécurité des composants critiques des contrats intelligents.

Les contrats intelligents ont certaines propriétés qui facilitent leur vérification formelle. Comme l’explique Shuvendu Lahiri, chercheur principal chez Microsoft:

“The modest code size and the sequential execution semantics of smart contractsmake them amenable to scalable verification, and the open operating environment substantially reduces the need to manually model the environment in which a smart contract operates”

“La taille modeste du code et la sémantique d’exécution séquentielle des contrats intelligents permettent une vérification évolutive, et l’environnement d’exploitation ouvert réduit considérablement la nécessité de modéliser manuellement l’environnement dans lequel un contrat intelligent fonctionne.

VeriSol complétera Azure Blockchain Development Kit and Workbench de Microsoft.  Celui ci offre des modèles de développement et des intégrations pour les services Azure comme la gestion des clés et l’identité. Des outils de vérification formels comme VeriSol permettent aux développeurs de vérifier plus facilement leur travail et de détecter les failles de sécurité.

Les développeurs disposent ainsi d’un cheminement plus efficace vers la production. Solidity est le langage le plus populaire pour la programmation de contrats intelligents sur Ethereum. Un outil de vérification formelle automatisé devrait donc permettre aux développeurs d’améliorer plus facilement la sécurité de leurs dApps.

Share This