Rasmus Rønneberg

Context: In information flow control by construction the idea is to develop programs and algorithms such that they are guaranteed to fulfill a specification stating how the information is allowed to flow. This is done by step-wise constructing the program through sound refinements. These refinements are currently proved sound by pen and paper analysis but not yet with automated tools.

Goal: Use an automated theorem prover, such as lean or coq, to prove that the refinements for information flow control are sound and does not lead to illegal flows of information.

Requirements: Basic knowledge of logic and discrete mathematics.