Sciweavers

Share
CCS
2004
ACM

Formally verifying information flow type systems for concurrent and thread systems

12 years 1 days ago
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
Gilles Barthe, Leonor Prensa Nieto
Added 01 Jul 2010
Updated 01 Jul 2010
Type Conference
Year 2004
Where CCS
Authors Gilles Barthe, Leonor Prensa Nieto
Comments (0)
books