Verification Support for Collections in Python
Background
In the past two decades, there has been a lot of progress in static verification of object oriented programs, to the point where automatic verifiers can now verify both safety and functional correctness of realistic programs.
One aspect which is not supported by current verifiers are collections, i.e. heap structures like lists, sets and maps, which differ from arrays in the sense that properties like containment are typically defined modulo object equality.
Consider for example the expression "o in os" in Python, where "o" is some object and "os" is a set. This expression evaluates to true if there is an object in the set "os" whose "__hash__" method returns the same value as that of "o", and whose "__eq__" method returns true when called with the argument "o".
This presents several challenges for verification; first of all, both "__hash__" and "__eq__" can be overridden in subclasses, and the exact types of "o" and of the elements of "os" are generally not known statically. In particular, this means that both the definitions of these methods and their footprints (i.e., the set of heap locations they depend on), which are important to know when verifying heap dependent programs, are not known statically.
Secondly, the most natural way of formalizing the behavior of set containment involves existential quantification, which is typically not handled well by the SMT solvers used by automated verifiers.
Our group is developing Nagini, a Python frontend for the Viper verification infrastructure, whose purpose is to verify the Python implementation of the SCION internet architecture. Like most typical Python code, the SCION implementation makes extensive use of the built-in Python lists, sets and dictionaries. Moreover, the code uses classes with custom equality relations in combination with these collections.
In order to be able to verify code which uses collections, we will have to specify the interface methods of Python's collections in the Viper language in a way which can be efficiently reasoned about using SMT solvers.
Goals
The goal of this project is to add support for equality-aware collections to the Nagini verifier for Python. In particular, the project aims to:
- Design a way to support dynamically-bound pure function calls in specifications
- Implement this, and additional features needed specifically for equality relations, in the Nagini verifier
- Express contracts of collection methods in a way which is well-suited for SMT solvers
- Encode and fine-tune collection axiomatizations in the Viper language
- Evaluate the implementation by verifying typical code examples from the SCION implementation
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 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
Contact