Code Verification

From Safe Systems Programming to Proven–Correct Software

Who is the material made for?

This module targets developers and designers interested in programming languages and tools for increasing their confidence in future projects.

It will enable them to judge better trade–offs between using formal verification tools that yield hard safety and security guarantees and the development effort required to use those tools.

The module assumes some programming background, though not necessarily insystemsprogramming languages (e.g.,C/C++ or Rust). A general computer science background is beneficial.

Introduction

Ensuring that a program safely and securely does what it is supposed to do is notoriously difficult. This module introduces a continuum of languages, tools, and techniques for increasing confidence into software.

7

We will discuss those techniques by developing programs with increasingly more rigid safety, correctness, and security guarantees. As such, successful course participants will be able to judge better the benefits – for example: ruling out certain bugs during development – and the costs – for example: additional development effort when working with a tool – of available systems programming languages and verification tools.

Since security is impossible without safety–ca. 70% of all security vulnerabilities can be traced back to memory safety issues – we will start by considering how memory safety issues arise, by looking at different classes of attacks in C and Java, exploiting manual memory management and serialization, respectively. We will then introduce the Rust programming language, a modern high–performance systems programming language. Programming in Rust requires more effort than programming inC/C++: programs that compile in C may be rejected by the Rust compiler unless the programmer carefully adds certain annotations.At the same time, the Rust compiler guarantees that common memory safety issues, for example use–after–free bugs, will never occur in a valid Rust program.

.Verification tools can give much stronger guarantees at the cost of requiring more program annotations from software developers. For example, for a banking application we may want to ensure that every transaction distributes money only among the intended accounts as specified. We will use the Rust verifier Prusti to specify and verify such contracts, thereby discussing tools for developing proven–correct software that work on top of Rust.

Overall, participants will then be able to make an educates choice about tool usage based on what kind of guarantees are needed for a project and how much effort (in terms of annotations required by verification tools and the compiler) one is willing to invest.