Verification of closures for Go programs
Go (often called external page Golang) is a modern programming language with a focus on simple and scalable concurrency. It is used in large-scale web-based software projects, such as Netflix, Ethereum, and Scion. As experienced in numerous cases (including the famous external page Heartbleed), bugs in such systems can have severe consequences, compromising user data and costing large sums of money. Hence it is crucial to formally verify the absence of bugs in critical implementations.
In our group we are developing Gobra, a code verifier for the Go programming language. Gobra takes Go programs as input, annotated with logical specifications that describes the intended behavior of that program, and checks mechanically whether every execution of the input program follows that description without crashing. Internally, Gobra translates annotated Go programs to Viper, an intermediate verification language developed by our group.
One of the current limitations of Gobra is the absence of support for closures. Verifying closures is challenging for a number of reasons. First and foremost, closures are frequently used in conjunction with higher-order functions, like the sorting function from Go's standard library. However, higher-order functions cannot be specified directly in the first-order logic supported by automatic theorem provers. Another challenge is that closures in imperative languages like Go can capture local state, and modify it when called. As such calls can happen in unrelated parts of the code, this leads to additional difficulties for tracking side effects. Fabian Wolff in his Download master thesis (PDF, 821 KB) proposed a solution for verification of closures in Rust that could be used as a starting point, but cannot be exploited directly due to Go's type system not providing the strict separation guarantees from Rust's type system.
Furthermore, there is an additional wrinkle with respect to closures that is specific to Go. One common use case of closures is to write deferred clean-up code, through the keyword defer. Such deferred calls are stacked and called in reverse order at the end of the execution of the surrounding function. While it is possible to handle verification of deferred calls by treating them within a general closure framework, such a naive solution may be exceedingly verbose in practice. On the other hand, as deferred calls can occur within the body of a loop, eliminating deferred calls by rewriting the program is not possible in general.
Goals
The objective of this project is to extend Gobra with support for closures. The core milestones are:
- Developing a methodology to specify and verify Go code with closures, building on Fabian Wolff's work for Prusti.
- Extending the methodology so that it can support reasonably concise specification and verification of deferred function calls.
- Implementing the developed techniques in Gobra.
- Evaluating the methodology by demonstrating it on verification examples.
Opportunities
- Contribute to a state-of-the-art verifier that is at the center of a large ongoing research project.
- Gain experience in working with modern specification languages and code verification techniques.
Prerequisites
Candidates should have some experience writing programs with closures. Prior experience using Scala is recommended, given that major parts of Gobra are implemented in Scala. Previous exposure to Go may also be beneficial.