Formally verifying information flow type systems for concurrent and thread systems
Gilles Barthe, Leonor Prensa Nieto · 2004
Information flow type systems provide an elegant means to enforce confidentiality of programs. Using the proof assis-tant Isabelle/HOL, we have machine-checked a recent work of Boudol and Castellani [4], which defines an information flow type system for a concurrent language with scheduling, and shows that typable programs are non-interferent. As a benefit of using a proof assistant, we are able to deal with a more general language than the one studied by Boudol and Castellani. The development constitutes to our best knowl-edge the first machine-checked account of non-interference for a concurrent language.