Visitez le
https://archive.devcon.org/ pour accéder à l'ensemble de la bibliothèque des conférences Devcon avec la facilité de filtrage, des playlists, des suggestions personnalisées, un accès décentralisé sur IPFS et plus encore.
Dans cet atelier pratique, nous passerons en revue le processus de vérification formelle des contrats intelligents. Les participants apprendront (1) comment spécifier formellement les exigences fonctionnelles pertinentes des contrats Ethereum, telles que "la somme des dépôts ne dépasse jamais le solde du contrat", et (2) comment les vérifier en utilisant des outils d'analyse existants pour Ethereum.
Tout d'abord, nous montrerons comment spécifier formellement le comportement attendu des contrats intelligents. Nous examinerons de plus près les propriétés temporelles de sécurité, une classe expressive de propriétés pour capturer quelles séquences d'états de contrat sont considérées comme correctes. Nous présenterons des idiomes de exigences courants, y compris le contrôle d'accès, les propriétés basées sur l'état, les invariants multi-contrats, et d'autres.
Ensuite, nous fournirons un aperçu des outils de test existants, tels que les outils basés sur l'exécution symbolique et les fuzzers. L'objectif est de comprendre comment ils peuvent être utilisés pour identifier les violations des propriétés formalisées ainsi que leurs limitations à fournir des garanties formelles illimitées.
Enfin, nous apprendrons comment les vérificateurs formels vont au-delà des tests et peuvent fournir des garanties formelles illimitées (pour toute séquence de transactions). Nous examinerons de plus près le langage de spécification utilisé par VerX et sa méthode de vérification automatisée, qui est facile à utiliser et ne nécessite pas de connaissances approfondies en vérification formelle.
Intervenants : Dimitar Dimitrov, Anton Permenev, Hubert Ritzdorf, Petar Tsankov
Niveau de compétence : intermédiaire
Parcours : Sécurité
Mots-clés : technique
Devcon est la conférence Ethereum pour les développeurs, chercheurs, penseurs et créateurs.
Devcon 5 a eu lieu à Osaka, Japon, du 8 au 11 octobre 2019.
Devcon est organisé et présenté par la Fondation Ethereum, avec le soutien de nos sponsors. Pour en savoir plus, veuillez visiter
https://ethereum.foundation/