La sécurité du code des contrats intelligents est d'une importance capitale pour l'industrie de la blockchain. Les contrats intelligents contiennent les implémentations des DAO, des tokens, des NFT, des services DeFi et d'autres applications et actifs blockchain, et sont à la fois régulièrement ciblés par des attaquants pour des exploits délibérés et sources de conséquences potentiellement désastreuses en raison d'erreurs de programmation involontaires.
Depuis au moins 50 ans, le domaine de la vérification formelle offre aux programmeurs la vision alléchante de trouver automatiquement des bogues et des vulnérabilités dans les applications en utilisant la logique formelle et les mathématiques.
La vérification formelle des contrats intelligents a suscité un intérêt considérable en tant que moyen d'augmenter la sécurité du code des contrats intelligents sur des plateformes blockchain comme Ethereum et dans des langages comme Solidity. Contrairement au code à usage général, le code des contrats intelligents est particulièrement adapté aux méthodes d'analyse statique et de vérification formelle.
Cette présentation portera sur la vérification formelle des contrats intelligents C# sur la plateforme blockchain Stratis en utilisant l'outil d'analyse statique et de vérification formelle Silver. Stratis est une plateforme blockchain modulaire open-source implémentée en C# qui fournit un registre distribué et un environnement pour exécuter des contrats intelligents écrits en C# en utilisant le CLR .NET comme VM de contrat intelligent.
Silver analyse les contrats intelligents Stratis à la fois au niveau du code source et du bytecode et utilise le cadre de programmation Spec# créé par Microsoft Research pour vérifier formellement le code des contrats intelligents C#.
Les sujets que je vais aborder sont :
* Vue d'ensemble des concepts de base de la blockchain et des contrats intelligents
* Vue d'ensemble de la plateforme blockchain Stratis et de l'environnement des contrats intelligents C#
* Brève vue d'ensemble de l'écosystème du compilateur C# Roslyn
* Vue d'ensemble de l'outil en ligne de commande Silver et du plugin Visual Studio Roslyn
* Analyse statique du code CIL .NET
* Brève vue d'ensemble de la vérification formelle
* Vue d'ensemble du système de programmation Spec#
* Réutilisation de Spec# pour le C# moderne en utilisant les réécrivains de code source Roslyn
* Cas d'utilisation de la vérification formelle - analyse des différentes vulnérabilités des contrats intelligents et comment la vérification formelle peut y remédier
Découvrez plus de nos intervenants et conférences à