Alexander Kittelmann

Context: In the context of information flow, variables are mapped to a security level. Not all flows are desirable (i.e., we want to prohibit leakage of private information to public sinks). That means that no f lows from higher security levels to lower ones should exist. We proposed and formalized a concept to ensure a correct information f low by construction. Instead of a subsequent analysis, we know which information is confidential and develop our programs accordingly.

Goal: The current formalization exists only on paper. We want to use an interactive proof assistant to mechnanize this formalization and to increase trust. The goal is to instantiate a constructed program in the theorem prover and to certify its correctness w.r.t. to the formalization of rules.

Prerequisites: Basic knowledge of formal verification, information flow and integrity properties, theorem proving.