@inbook{5fa21f345eeb407d9dd780a523ff91cf,
title = "Discretionary Information Flow Control for Interaction-Oriented Specifications",
abstract = "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.",
keywords = "Information flow control, Discretionary access control, Choreographies, Communication protocols, Interaction-oriented computing, Parallel computing, Service-oriented computing, Highperformance computing",
author = "{Lluch Lafuente}, Alberto and Flemming Nielson and Nielson, {Hanne Riis}",
year = "2015",
doi = "10.1007/978-3-319-23165-5_20",
language = "English",
isbn = "978-3-319-23164-8",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "427--450",
booktitle = "Logic, Rewriting, and Concurrency",
}