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.
Type de document :
Communication dans un congrès
2nd ACM Workshop on Formal Methods in Security Engineering - FMSE'2004, Oct 2004, Washington D.C./USA, ACM Press, pp.13-22, 2004, Proceedings of the 2004 ACM workshop on Formal methods in security engineering. 〈10.1145/1029133.1029136〉
Liste complète des métadonnées

Littérature citée [31 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00000632
Contributeur : Leonor Prensa Nieto <>
Soumis le : jeudi 10 novembre 2005 - 12:41:46
Dernière modification le : samedi 27 janvier 2018 - 01:31:28
Document(s) archivé(s) le : vendredi 2 avril 2010 - 18:55:13

Identifiants

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, Oct 2004, Washington D.C./USA, ACM Press, pp.13-22, 2004, Proceedings of the 2004 ACM workshop on Formal methods in security engineering. 〈10.1145/1029133.1029136〉. 〈inria-00000632〉

Partager

Métriques

Consultations de la notice

274

Téléchargements de fichiers

180