Concurrent programming in C is complicated by optimisations that can be made to the code before or during execution. Both the compiler and the underlying hardware can optimise the behaviour of an individual thread without considering the rest of the program with which the thread interacts. In particular, these optimisations can reorder instructions from the perspective of other threads causing unexpected whole-program behaviour.
It is well known that such optimisations may violate security guarantees apparent at the level of source code, even when these optimisations have been proven to preserve functional correctness. For this reason, much security analysis is done on assembly code or binaries, rather than directly on source code. However, an analysis at the level of source code provides two advantages. Firstly, if it shows that the software is secure then that software is secure when compiled with any compiler to any hardware platform. Secondly, it provides feedback on the analysis at the source-code level (at which the programmer is working). Mapping analysis results on assembly code or binaries to the source-code level is a non-trivial problem.
This project will develop an information flow logic for C programs building on an existing formal semantics of the allowable compiler optimisations defined in the C11 standard. An information flow logic comprises a set of rules, typically one for each kind of program instruction, which are used to determine whether an instruction can leak (confidential) information. The logic will be encoded and proved sound in a theorem prover, and its use supported by adapting an existing program verification tool.
An information flow logic for C programs
A mechanization of the soundness of the logic in a theorem prover
An adaptation of a program verification tool to support the logic
Information for applicants
Programming, discrete mathematics.
Formal methods, theorem proving.
Expected qualifications (Course/Degrees etc.)
Bachelor or masters degree in computing or mathematics.