Formally verifying information flow type systems for concurrent and thread systems

Information flow type systems provide an elegant means to enforce confidentiality of programs. Using the proof assistant 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 knowledge the first machine-checked account of non-interference for a concurrent language. Categories and Subject Descriptors F.3.3 [Studies of Program Constructs]: Type structure; D.2.8 [Software Engineering]: Software/Program Verification; D.3.2 [Language Classifications]: Concurrent, distributed, and parallel languages General Terms Security, languages, verification Keywords Non-interference, concurrency, machine-checked proofs

• Type: Conference
• Year: 2004
• Where: CCS
• Authors: Gilles Barthe, Leonor Prensa Nieto
• Keywords: CCS 2004, Concurrent Language, Information flow Type, Proof Assistant, Security Privacy