Automatic Inference of Information Flow Properties
Background
A program has secure information flow if it does not leak any information about secret values like passwords or encryption keys in its output values. Non-interference is a program property which is closely related: Put simply, if all input and output variables of a given program are classified as either high (secret) or low (public), non-interference means that the values of the low outputs are not influenced by the high inputs, i.e., if the program is run multiple times with the same low inputs (but possibly different high inputs), the low outputs will always stay the same.
As part of an effort to verify the Python implementation of the SCION internet architecture, our group is currently developing a technique for automatically verifying non-interference for Python programs. As is generally the case with deductive verification, this requires that specifications have to be added to the program in the form of pre- and postconditions as well as loop invariants, stating for example that certain inputs can be assumed to be low or high. Adding these specifications can mean a significant overhead for the programmer, and it would therefore be convenient if they could be automatically inferred. Static analysis provides mathematical guarantees about the behavior of programs and therefore is a suitable instrument to infer the desired specifications.
Goals
The project consists of the following milestones:
- Develop a static analysis that infers information flow properties. This analysis will combine existing approaches with novel ideas to handle concurrent, heap-manipulating programs.
- Implement the inference in Sample, a generic static analyzer developed within our group that is based on abstract interpretation, a general theory for approximating the behavior of programs.
- Test the implementation by inferring and verifying contracts for relevant parts of the SCION code.
Useful prerequisites
The following skills would be helpful, but can also be learned during the project:
- Background in static analysis and abstract interpretation.
- Familiarity with deductive verification techniques (e.g., Hoare logic).
- Experience with the Scala programming language.
Opportunities
The project offers the following opportunities:
- Contribute to the verification of real, security-critical code.
- Learn about state-of-the-art verification techniques for advanced program properties.
- Apply static analysis and abstract interpretation concepts in practice.
- Work with and contribute to state-of-the-art, open source verification tools.