Formal verification of C# smart contracts

The security of smart contract code is of utmost importance to the blockchain industry. Smart contracts contain the implementations of DAOs, tokens, NFTs, DeFi services, and other blockchain applications and assets, and are both routinely targeted for deliberate exploits by attackers as well as sources of potentially disastrous consequences due to inadvertent programming errors.

For at least 50 years the field of formal verification has offered to programmers the tantalizing vision of automagically finding bugs and vulnerabilities in applications using formal logic and mathematics.

Formal verification of smart contracts has attracted considerable interest as a way to increase the security of smart contract code on blockchain platforms like Ethereum and in languages like Solidity. In contrast to general-purpose code, smart contract code is uniquely suited to the methods of static analysis and formal verification.

This presentation will look at formal verification of C# smart contracts on the Stratis blockchain platform using the Silver static analysis and formal verification tool. Stratis is an open-source modular blockchain platform implemented in C# that provides a distributed ledger and environment for executing smart contracts written in C# using the .NET CLR as the smart contract VM.

Silver analyzes Stratis smart contracts at both the source code and bytecode level and uses the Spec# programming framework created by Microsoft Research to formally verify C# smart contract code.

The topics that I'll cover are:
* Overview of basic blockchain and smart contract concepts
* Overview of the Stratis blockchain platform and C# smart contract environment
* Short overview of the C# Roslyn compiler ecosystem
* Overview of the Silver command-line tool and Visual Studio Roslyn plugin
* Statically analyzing .NET CIL code
* Short overview of formal verification
* Overview of the Spec# programming system
* Repurposing Spec# for modern C# using Roslyn source-code rewriters
* Formal verification use cases - analyzing different smart contract vulnerabilities and how formal verification can address them