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
Journal articles

Secure Information Flow for a Concurrent Language with Scheduling

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 specified an information flow type system for a concurrent language featuring primitives for scheduling, and shown that typable programs are non-interfering for a possibilistic notion of non-interference. The development, which constitutes to our best knowledge the first machine-checked account of non-interference for a concurrent language, takes advantage of the proof assistant facilities to structure the proofs about different views of the programming language and to identify the relationships among them and the type system. Our language and type system generalize previous work of Boudol and Castellani, Theoretical Computer Science 281 (2002), 109–130, in particular by including arrays and lifting several convenient but unnecessary conditions in the syntax and type system of the work of Boudol and Castellani. We illustrate the generality of our language and the usefulness of our type system with a medium size example.
Document type :
Journal articles
Complete list of metadata

Cited literature [52 references]  Display  Hide  Download

Contributor : Leonor Prensa Nieto Connect in order to contact the contributor
Submitted on : Tuesday, October 10, 2006 - 5:08:39 PM
Last modification on : Friday, February 4, 2022 - 3:30:27 AM
Long-term archiving on: : Tuesday, April 6, 2010 - 1:06:33 AM


  • HAL Id : inria-00097395, version 1



Gilles Barthe, Leonor Prensa Nieto. Secure Information Flow for a Concurrent Language with Scheduling. Journal of Computer Security, IOS Press, 2007, Formal Methods in Security Engineering Workshop (FMSE 04), 16 (6), pp.647 - 689. ⟨inria-00097395⟩



Record views


Files downloads