Software Verification

Supervisor: Marieke Huisman and Alexander Stekelenburg

Recently, a new format for describing verifications task (i.e. a program with some specifications), called SV-LIB has been released. This format is intended to be more general and allow verifiers to focus on the verification task instead of the idiosyncrasies of C, which is the current de-facto standard format of competitions like SV-COMP. The new SV-LIB format will hopefully facilitate more collaboration and competition between verification tools.

Here at the Formal Methods and Tools group of the University of Twente we develop a deductive verifier called VerCors. VerCors can prove the correctness and memory-safety of sequential and concurrent programs written in Java, C, CUDA, OpenCL, and more. We would like to extend the tool with support for SV-LIB. By adding support for SV-LIB it becomes possible to collaborate on a verification task with another verifiers such as CPAChecker. CPAChecker can generate loop invariants which VerCors can then use.

In this project you will add support for SV-Lib to VerCors and determine how effective collaborating on a verification task with another verifier can be.

The suggested steps for this research project are:
- Compare SV-LIB to VerCors' internal verification language PVL to determine if all SV-LIB features have an equivalent feature in PVL
- Implement an SV-LIB frontend for VerCors (there's an ANTLR parser already available)
- Translate some examples from PVL to SV-LIB to compare performance
- Attempt to verify some examples by combining VerCors and CPAChecker



Additional information

Information on SV-LIB can be found in the paper, in this presentation, and in the Gitlab repository.

Information on VerCors can be found in the tutorial on the website. Additionally, there is also a paper about combining VerCors and CPAChecker for verification.

Supervisors: Marieke Huisman, Robert Mensing
Traditionally, program verification focuses on proving functional properties of a program: if a program is executed, it will compute a certain value, or reach a certain state. Recently, several people have developed techniques for relational verification, which establishes a relationship between the execution of two different programs (or even of the program with itself) [1, 2, 3, 4].

Relational verification has been used for example for information flow properties [1, 7], slicing [2] and regression verification [6]. The VerCors verifier that we are developing in the Formal Methods and Tools group at the University of Twente currently does not support relational verification, while Viper (the verifier underlying VerCors) does support this [7, 8]. In this assignment, we ask you to study the different approaches to relational verification, and to see how we can extend the VerCors verifier to support relational verification.

Typical steps in the project would be:

• understand existing approaches to relational verification in the literature
• identify which approach would fit well with VerCors
• propose a design to extend VerCors with relational verification support
• implement the support

Some relevant literature
[1] Gilles Barthe, Pedro R. D'Argenio, Tamara Rezk: Secure Information Flow by Self-Composition. CSFW 2004: 100-114
[2] Gilles Barthe, Juan Manuel Crespo, César Kunz: Relational Verification Using Product Programs. FM 2011: 200-214
[3] Ádám Darvas, Reiner Hähnle, David Sands: A Theorem Proving Approach to Analysis of Secure Information Flow. SPC 2005: 193-209
[4] Moritz Kiefer, Vladimir Klebanov, Mattias Ulbrich: Relational Program Reasoning Using Compiler IR. VSTTE 2016: 149-165
[5] Bernhard Beckert, Thorsten Bormer, Stephan Gocht, Mihai Herda, Daniel Lentzsch, Mattias Ulbrich: SemSlice: Exploiting Relational Verification for Automatic Program Slicing. IFM 2017: 312-319
[6] Bernhard Beckert, Mattias Ulbrich, Birgit Vogel-Heuser, Alexander Weigl: Regression Verification for Programmable Logic Controller Software. ICFEM 2015: 234-251
[7] Marco Eilers, Peter Müller, Samuel Hitz: Modular Product Programs. ESOP 2018: 502-529
[8] Marco Eilers, Severin Meier, Peter Müller: Product Programs in the Wild: Retrofitting Program Verifiers to Check Information Flow Security. CAV (1) 2021: 718-741

Supervisor: Marieke Huisman and Alexander Stekelenburg

The C and C++ languages (and others) use a preprocessor to split up a codebase into multiple files and enable the use of macros to make the language more ergonomic. Many C libraries use macros and these libraries would be cumbersome to use without these macros.

For software verification we write the specifications in comments, but these comments are ignored by the preprocessor. This means that macros will not be expanded inside specifications which makes writing specifications cumbersome compared to writing code. Additionally, preprocessors only include line information in their output which makes it impossible to find the correct column to point to if an error occurs in a macro expansion.

We would like to investigate if and to what degree improving macro support would allow us to support verifying C code that uses libraries. Additionally, since macros can be used to generate repetitive code they may also be useful for generating repetitive specifications.

The goal of this project is to determine how macros can aid verification, and to design and implement a C/C++ preprocessor to allow us to use macros in more cases. The preprocessor should be able to expand macros inside and outside of comments, and should preserve line and column information such that errors can be precisely located in error messages.

There are multiple approaches we can take, which of these is optimal depends on how macros are used in real C/C++ projects and how we would like to use them in annotations. Both the Frama-C and VeriFast verifiers use a custom preprocessor for this purpose, but the implementation is too closely entangled with these verifiers to be re-used by other tools.

We would like to use such a preprocessor for the C and C++ frontend of the VerCors deductive verifier that we develop here at the FMT group in Twente. You can find out more about VerCors here: https://vercors.ewi.utwente.nl.

Supervisor: Marieke Huisman, Alexander Stekelenburg
Deductive verifiers can be used to prove correctness of a program. To determine whether a program is correct, the user needs to give a program and its specification to the verifier. These specifications are typically written in a specification language, often inspired by predicate logic. However, while very similar, specification languages for different verifiers often have slightly different semantics, due to which it is difficult to reuse specifications from other verifiers.

We have developed the Specification Translator, a tool to translate specifications between several deductive verifiers for Java programs. It currently supports Krakatoa, OpenJML and VerCors specifications. As a result, we are now able to reuse specifications between these three verifiers.

In this project, we ask you to add support for another deductive verifier to the Specification Translator. An interesting candidate for this is KeY. You will have to study the differences in semantics of the specification languages, and see how support for KeY's specification language can be added to the Specification Translator.

You will be expected to take the following steps:

• Understand KeY's specification language
• Identify differences between the semantics of KeY's specification language and the languages currently supported
• Implement support for KeY's specification language in the Specification Translator

Supervisors: Peter Lammich
Interactive Theorem Provers (ITPs) provide a way to develop computer checked (mathematical) proofs. In particular, they can be used to prove programs correct. In this project, you will learn to use an ITP, and apply it to prove correct a functional program or data structure of your choice (agreed on with the supervisor).