Move: Language, Bytecode Verifier, Prover

Speaker: Shaz Qadeer

Shaz Qadeer works at Facebook. In addition to the work described in the abstract of this talk, he also works on Civl, a reifier for concurrent programs.. His research interests span all aspects of development of robust and secure software.

Abstract

Move is a language originally designed for programming Diem, a peer-to-peer network for replicated computation (also known as a blockchain in some circles).

The Move programming framework provides:

1. a compiler that lowers the code to bytecode,
2. a verifier that guarantees type and memory safety even in the presence of untrusted code, and
3. a prover capable of verifying functional correctness of compiled bytecode against deep safety specifications.

This talk will provide an overview of the language, the bytecode verifier, and the prover. If time permits, I will speculate on new applications for Move.