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
Liste complète des métadonnées

Cited literature [31 references]  Display  Hide  Download

https://hal.inria.fr/inria-00000632
Contributor : Leonor Prensa Nieto <>
Submitted on : Thursday, November 10, 2005 - 12:41:46 PM
Last modification on : Saturday, January 27, 2018 - 1:31:28 AM
Document(s) archivé(s) le : Friday, April 2, 2010 - 6:55:13 PM

Identifiers

Collections

Citation

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⟩

Share

Metrics

Record views

278

Files downloads

189