Discretionary Information Flow Control for Interaction-Oriented Specifications

Alberto Lluch Lafuente, Flemming Nielson, Hanne Riis Nielson

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

663 Downloads (Orbit)

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.
Original languageEnglish
Title of host publicationLogic, Rewriting, and Concurrency : Essays Dedicated to José Meseguer on the Occasion of His 65th Birthday
PublisherSpringer
Publication date2015
Pages427-450
ISBN (Print)978-3-319-23164-8
ISBN (Electronic)978-3-319-23165-5
DOIs
Publication statusPublished - 2015
SeriesLecture Notes in Computer Science
Volume9200
ISSN0302-9743

Keywords

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

Fingerprint

Dive into the research topics of 'Discretionary Information Flow Control for Interaction-Oriented Specifications'. Together they form a unique fingerprint.

Cite this