Discretionary Information Flow Control for Interaction-Oriented Specifications

Research output: Chapter in Book/Report/Conference proceedingBook chapterResearchpeer-review

221 Downloads (Pure)


This paper presents an approach to specify and check discretionary information flow properties of concurrent systems. The approach is inspired by the success of the interaction-oriented paradigm to concurrent systems (cf. choreographies, behavioural types, protocols,...) in providing behavioural guarantees of global properties such as deadlock-absence. We show how some information flow properties are easier to formalise and check on a global interaction-oriented description of a concurrent system rather than on a local process-oriented description of the components of the system. We use a simple choreography description language adapted from the literature of choreographies and session types. We provide a generic method to instrument the semantics with information flow annotations. Policies are used to specify the admissible flows of information. The main contribution of the paper is a sound type system for statically checking if a system specification ensures an information flow policy. The approach is illustrated with two archetypal examples of distributed and parallel computing systems: a protocol for an identity-secured data providing service and a parallel MapReduce computation.
Original languageEnglish
Title of host publicationLogic, Rewriting, and Concurrency : Essays Dedicated to José Meseguer on the Occasion of His 65th Birthday
Publication date2015
ISBN (Print)978-3-319-23164-8
ISBN (Electronic)978-3-319-23165-5
Publication statusPublished - 2015
SeriesLecture Notes in Computer Science


  • Information flow control
  • Discretionary access control
  • Choreographies
  • Communication protocols
  • Interaction-oriented computing
  • Parallel computing
  • Service-oriented computing
  • Highperformance computing

Cite this

Lluch Lafuente, A., Nielson, F., & Nielson, H. R. (2015). Discretionary Information Flow Control for Interaction-Oriented Specifications. In Logic, Rewriting, and Concurrency: Essays Dedicated to José Meseguer on the Occasion of His 65th Birthday (pp. 427-450). Springer. Lecture Notes in Computer Science, Vol.. 9200 https://doi.org/10.1007/978-3-319-23165-5_20