HAL will be down for maintenance from Friday, June 10 at 4pm through Monday, June 13 at 9am. More information
Skip to Main content Skip to Navigation
Conference papers

Formally Verifying Information Flow Type Systems for Concurrent and Thread Systems

Gilles Barthe 1 Leonor Prensa Nieto 2
1 EVEREST - Environments for Verification and Security of Software
CRISAM - Inria Sophia Antipolis - Méditerranée
2 MOSEL - Proof-oriented development of computer-based systems
INRIA Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
Abstract : 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~\cite{BC02:tcs}, 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [31 references]  Display  Hide  Download

Contributor : Leonor Prensa Nieto Connect in order to contact the contributor
Submitted on : Thursday, November 10, 2005 - 12:41:46 PM
Last modification on : Friday, February 4, 2022 - 3:30:57 AM
Long-term archiving on: : Friday, April 2, 2010 - 6:55:13 PM




Gilles Barthe, Leonor Prensa Nieto. Formally Verifying Information Flow Type Systems for Concurrent and Thread Systems. 2nd ACM Workshop on Formal Methods in Security Engineering - FMSE'2004, Michael Backes, David Basin, and Michael Waidner, Oct 2004, Washington D.C./USA, pp.13-22, ⟨10.1145/1029133.1029136⟩. ⟨inria-00000632⟩



Record views


Files downloads