Advanced Proof Support for Go
external page Go 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 cases such as external page Heartbleed, bugs in such systems can have severe consequences, compromising confidential user data and costing large sums of money. Testing and similar runtime verification techniques can increase confidence in the correctness of code. However, they do not provide strong guarantees about the absence of bugs.
Gobra is a verification tool for Go programs, developed in our group. It allows developers to write contracts in the source code, which are then used to automatically check the functional correctness of the program. Internally, Gobra translates Go programs to the Viper intermediate verification language.
For more complex programs, additional proof annotations are required to aid Gobra in checking correctness. Currently, the only proof annotations supported by Gobra are basic assertions. Improving Gobra’s support for proof annotations, will be beneficial for writing concise, easier to understand Gobra programs and will increase the set of verifiable properties. Good examples of other proof annotations already exist: Dafny, another deductive verifier, supports annotations for well-known reasoning steps such as induction, and introduction and elimination of logical quantifiers. For instance, the statement `var x :| 0 < x && x < 42` defines a variable `x` such that it has some value strictly between 0 and 42, corresponding to existential-elimination.
Goals
The aim of the project is to extend Gobra with support for more advanced proof annotations as for example seen in Dafny. The core milestones of this project are:
- Design a proof annotation language for Gobra. The annotation language can be inspired by existing work, but should also aim to improve the current state of the art of proof annotations in deductive verifiers.
- Derive and implement an encoding of the proof annotation language from Gobra to Viper.
- Verify several programs illustrating the expressiveness of your annotation language.
Opportunities
- Obtain an in-depth understanding of modern verification techniques and how they are used in practice.
- Contribute to a state-of-the-art verifier that is at the center of a large ongoing research project.
- Gain experience with the development of a program verification tool.
Prerequisites
Major parts of Gobra are implemented in Scala. Therefore, prior experience programming in Scala would be beneficial, but is not required.