Proposal
This project focuses on a particularly active area of language-based security, namely type systems for information flow control. In order to guarantee that such type systems do actually enforce the intended confidentiality properties, a mathematical soundness proof with respect to the language semantics is required. In order to obtain the highest level of assurance, we propose to conduct these proofs with the help of theorem provers. This proposal aims to make the formalization and verification of information flow type systems an almost routine matter by dedicated support of the required proofs through a combination of interactive and automatic theorem provers. We plan to verify a wide range of qualitative and quatitaive information flow type systems. The proofs will be conducted with the help of the interactive theorem prover Isabelle and the automatic theorem prover SPASS. Special emphasis will be put on an effective combination of the two provers, exploiting in particular SPASS’s newly built-in linear arithmetic.