Disjunctive Information Flow for Communicating Processes

Ximeng Li, Flemming Nielson, Hanne Riis Nielson, Xinyu Feng

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

Abstract

The security validation of practical computer systems calls for the ability to specify and verify information flow policies that are dependent on data content. Such policies play an important role in concurrent, communicating systems: consider a scenario where messages are sent to different processes according to their tagging. We devise a security type system that enforces content-dependent information flow policies in the presence of communication and concurrency. The type system soundly guarantees a compositional noninterference property. All theoretical results have been formally proved in the Coq proof assistant [9].
Original languageEnglish
Title of host publicationRevised Selected Papers of the 10th International Symposium on Trustworthy Global Computing (TGC 2015)
EditorsPierre Ganty, Michele Loreti
PublisherSpringer
Publication date2016
Pages95-111
ISBN (Print)978-3-319-28765-2
ISBN (Electronic)978-3-319-28766-9
DOIs
Publication statusPublished - 2016
Event10th International Symposium on Trustworthy Global Computing (TGC 2015) - Madrid, Spain
Duration: 31 Aug 20151 Sep 2015
Conference number: 10
http://tgc2015.disia.unifi.it/

Conference

Conference10th International Symposium on Trustworthy Global Computing (TGC 2015)
Number10
CountrySpain
CityMadrid
Period31/08/201501/09/2015
Internet address
SeriesLecture Notes in Computer Science
Volume9533
ISSN0302-9743

Fingerprint Dive into the research topics of 'Disjunctive Information Flow for Communicating Processes'. Together they form a unique fingerprint.

Cite this