Contracts, Simulations, and Sessions: Formal Verification of Compilers, Smart Contracts, and Protocols

Abstract

Smart contracts are self-enforcing, self-executing protocols governing interactions between several (potentially distrusting) parties. Smart contracts automate the execution of an agreement between participants, typically using the blockchain. The potential for, and the magnitude of, financial losses motivate the application of the most rigorous correctness guarantees to smart contracts, i.e., formal verification. This dissertation applies concurrent process theory and formal verification across the full smart contract development pipeline, from semantics and compilation to transformation correctness and protocol specification. At the level of language semantics, this dissertation provides a small-step operational semantics for the Marlowe smart contract programming language. This clean semantic foundation is then used to verify the correctness of the Faustus smart contract programming language compiler. Faustus is a smart contract programming language that extends Marlowe with parameterized contract abstractions and an expression language for guarded commands with operators based on CCS. The compiler is verified in stages: first the normalization of the guard expressions is verified, and then the compilation to Marlowe is verified. Faustus contracts are then formalized as a labeled transition system that distinguishes observable and unobservable behavior. This formalization allows a smart contract transformation to be verified using weak bisimulation. The observable behaviors of the original contract are preserved in the transformed contract. Finally, this dissertation presents STILL, a standalone interactive tactic-based theorem prover for dependent session types. Unlike similar provers for linear type theories, STILL allows for delayed linear context partitioning at the tactic level rather than modifying the underlying proof rules. Protocols for the axiom of choice, natural numbers, and a long-running bit counter are verified to demonstrate the properties of the STILL system and its underlying type theory. This dissertation uses simulation, bisimulation, theorem proving, and process extraction to connect implementations to formal specifications. Together, these results show how formal methods based on concurrency and type theory can provide correctness guarantees at each step of protocol specification and smart contract development.