Toward a Framework for Soundness Proofs of Type Systems in Language-based 
Information-flow Security


In language-based information-flow security, the usage of security type 
systems as static analysis method for determining the presence of unwanted 
information leakage is widely spread. A security type system is sound 
if all typable programs satisfy a desired semantic security property.
Conducting soundness proofs for security type systems typically requires 
a lot of work. In order to facilitate the development of new security type 
systems, it is desirable to have a reliable framework that helps checking 
quickly whether a security type system is sound.

In this thesis, we took two steps toward a framework for soundness proofs 
of security type systems: 
1) We investigated a proof assistant as basis for such a framework by 
developing machine-checked versions of three chosen soundness proofs 
in Isabelle/HOL.
2) We systematically compared and analyzed the chosen soundness proofs 
using Isabelle/HOL formalizations from the first step. From the differences 
we encountered between the three example formalizations in Isabelle/HOL, 
we identified parameters for soundness proofs. We used these parameters 
to describe experiments on each of our Isabelle/HOL soundness proofs out 
of which we conducted 5 and describes their results.

In the talk, we present results and highlights from step 1 and 2 and 
share some ideas on future work in the direction of a framework for 
soundness proofs of type systems in language-based information-flow
security.