Abstract Read Permission Support for the Nagini Verifier

General Background.

Deductive program verification aims to show that a program adheres to a given specification, which is typically expressed in the form of pre- and postconditions as well as loop invariants. Verification becomes much more complex for programming languages which allow manipulating objects on a heap. When calling a method, it is for example not obvious which parts of the heap may be read or modified by said method, and which facts about the heap that were known before the call may therefore still be assumed to hold afterwards. In a concurrent setting, this problem becomes much more pronounced, because other threads might in principle modify any part of the heap at any time.

One way to address both of these problems is to treat each memory location as a resource which can be accessed by a thread only if
it has a needed permission. For example, a thread would be allowed to write to a memory location only if it has a full permission (denoted by rational number 1) to that location, and the thread would be allowed to read a memory location it has some positive permission amount to that location. A naïve way to specify permission amounts would be to use rational numbers like 1/2 explicitly. However, when using explicit rational numbers one cannot verify examples where a recursive call leaves some permission to the caller. This problem can be solved by using abstract read permissions [VMCAI2013] that allow to model an abstract read permission amount.

Project Background.

The Viper verification infrastructure [VMCAI2016] is a framework for automatically verifying programs using permission-based specifications. It consists of an intermediate language in which both programs and specifications can be expressed, as well as two backend-verifiers which can automatically reason about programs written in said language using SMT solvers. The Viper language contains constructs for describing concrete amounts of permissions (like 1/2), but lacks native support for abstract read permissions.

The Viper infrastructure serves as the basis for the Nagini verifier for statically-typed Python programs, which is currently being developed at the Chair of Programming Methodology and is and intended to be used for verifying the Python implementation of the external pageSCION internet architecture. Doing so requires annotating the SCION source code with specifications, including permissions, which would greatly benefit from the ability to use abstract read permissions.

Goals.

The goal of this project is to add support for abstract read permissions to the Nagini verifier for Python. In particular, the project aims to:

Design an extended Viper language that has a native support for abstract read permissions.
Implement a translator from the extended Viper language to the original Viper language.
Implement support for abstract read permissions in Nagini by translating into the extended Viper language.
Add support for quantified abstract read permissions, i.e., read permissions for a statically unknown number of memory locations, to the extended Viper language in a way which is well-suited for SMT solvers.
Update Nagini to utilize the extended Viper language with quantified abstract read permissions.
Evaluate the implementation by encoding typical examples from the SCION implementation and Chalice test suite.

Useful Prerequisites.

The following skills would be helpful, but can also be learned during the project:

Familiarity with deductive verification techniques (e.g., Hoare logic).
Programming experience with Scala and Python.

Opportunities.

The project offers the following opportunities:

Contribute to the verification of real, security-critical code.
Learn about state-of-the-art verification techniques and logic, in the context of the Viper project.
Understand low-level details of SMT solver encoding.
Work with and contribute to state-of-the-art, open source verification tools.

Contacts.

References.

[VMCAI2013] S. Heule and K. R. M. Leino and P. Müller and A. J. Summers: Abstract Read Permissions: Fractional Permissions without the Fractions. Verification, Model Checking, and Abstract Interpretation (VMCAI), 2013.

[VMCAI2016] P. Müller and M. Schwerhoff and A. J. Summers: Viper: A Verification Infrastructure for Permission-Based Reasoning. Verification, Model Checking, and Abstract Interpretation (VMCAI), 2016.