Runtime checking of code contracts in Python

General background

When trying to assert properties of programs and program executions, one can generally choose between static checks and checks at runtime. While only static checks can soundly prove safety properties for all program executions, runtime checks are often easier to implement, don't suffer from incompleteness, and can be used in scenarios where some information needed for static checking is missing (e.g. source code of precompiled libraries). For verification of contracts of heap-dependent programs, using for example separation logic, runtime checking is a non-trivial task. While there is previous work on this topic, it does not take into acount concurrency or partially annotated programs where some functions don't have contracts, and it offers no support for fractional permissions.

Project background

Our group is developing a Python frontend for the Viper verification infrastructure, whose goal is to verify the Python implementation of the SCION internet architecture. A specification language for Python has been developed and will be used to write contracts for both the SCION code and any used libraries.
One of the project goals is to make the writing and maintenance of specifications as simple and accessible as possible. Runtime verfication can help with this by showing programmers the concrete program state whenever an assertion is violated, as opposed to a symbolic state or even just a generic verification failure. In addition, it can be used to evaluate the specifications for axiomatized methods, by making sure that their contracts are fulfilled in test runs.

Goals

Develop a technique for instrumenting Python code
Develop a runtime checking technique for concurrent programs partially annotated with contracts using fractional permissions
Implement instrumentation and checking for the specification language developed for the Viper Python frontend
Evaluate the implementation by writing and checking contracts for libraries used by the SCION implementation

Useful prerequisites

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

Programming experience with Python

Opportunities

The project offers the following opportunities:

Understand the advantages and challenges of checking program properties at runtime as opposed to checking them statically
Delve deep into advanced Python features like AST rewriting
Work with and contribute to state-of-the-art, open source verification tools