Enregistré : 21/07/2021 Séminaire de Sécurité CERIAS à l'Université de Purdue Un Vérificateur Formel pour le Langage Move de la Blockchain Diem David Dill, Facebook La blockchain Diem, qui a été initiée en 2018 par Facebook, comprend un nouveau langage de programmation appelé Move pour la mise en œuvre de contrats intelligents. La correction des programmes Move est particulièrement importante car la blockchain hébergera de grandes quantités d'actifs, ces actifs étant gérés par des contrats intelligents, et en raison d'un historique de pertes importantes sur d'autres blockchains à cause de bugs dans les contrats intelligents. Le langage Move est conçu pour être aussi sûr que possible, et il est accompagné d'une spécification formelle et d'un outil de vérification automatique, appelé le Move Prover. Un projet visant à spécifier et à vérifier formellement autant de propriétés importantes que possible de la bibliothèque standard Move est désormais bien avancé. Cette présentation portera sur les objectifs du projet et les idées les plus intéressantes que nous avons eues jusqu'à la date de la présentation. L'implémentation complète de la blockchain, y compris le langage Move, la machine virtuelle, le Move Prover et divers modules Move presque finalisés, est disponible sur
http://github.com/libra \(Visitez : www.cerias.purdue.edu\)