Meng Xu, "Fast and Reliable Formal Verification of Smart Contracts with the Move Prover"

CERIAS Weekly Security Seminar - Purdue University

English - November 30, 2022 21:30 - 212 MB Video - ★★★★ - 6 ratings
Technology Education Courses infosec security video seminar cerias purdue information sfs research education Homepage Download Apple Podcasts Google Podcasts Overcast Castro Pocket Casts RSS feed

Previous Episode: Brian Barnier & Prachee Kale, "Making Cybersecurity Reliable and Cybersecurity Careers Rewarding"

Next Episode: Julie Haney, "Users Are Not Stupid: Six Cybersecurity Pitfalls Overturned"

The Move Prover (MVP) is a formal verifier for smart contracts
written In the Move programming language. MVP has an expressive
specification language, and is fast and reliable enough that it can
be run routinely by developers and in integration testing. Besides
the simplicity of smart contracts and the Move language, three
implementation approaches are responsible for the practicality of
MVP: (1) an alias-free memory model, (2)fine-grained invariant
checking, and (3) monomorphization. The entirety of the Move code
for the Diem blockchain has been extensively specified and can be
completely verified by MVP in a few minutes. Changes in the Diem
framework must be successfully verified before being integrated
into the open source repository on GitHub.