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

Cite this

Li, X., Nielson, F., Nielson, H. R., & Feng, X. (2016). Disjunctive Information Flow for Communicating Processes. In P. Ganty, & M. Loreti (Eds.), Revised Selected Papers of the 10th International Symposium on Trustworthy Global Computing (TGC 2015) (pp. 95-111). Springer. Lecture Notes in Computer Science, Vol.. 9533 https://doi.org/10.1007/978-3-319-28766-9_7
Li, Ximeng ; Nielson, Flemming ; Nielson, Hanne Riis ; Feng, Xinyu. / Disjunctive Information Flow for Communicating Processes. Revised Selected Papers of the 10th International Symposium on Trustworthy Global Computing (TGC 2015). editor / Pierre Ganty ; Michele Loreti. Springer, 2016. pp. 95-111 (Lecture Notes in Computer Science, Vol. 9533).
@inproceedings{5c9effd3c28e4af89f2aa062cdc61766,
title = "Disjunctive Information Flow for Communicating Processes",
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].",
author = "Ximeng Li and Flemming Nielson and Nielson, {Hanne Riis} and Xinyu Feng",
year = "2016",
doi = "10.1007/978-3-319-28766-9_7",
language = "English",
isbn = "978-3-319-28765-2",
pages = "95--111",
editor = "Ganty, {Pierre } and Loreti, {Michele }",
booktitle = "Revised Selected Papers of the 10th International Symposium on Trustworthy Global Computing (TGC 2015)",
publisher = "Springer",

}

Li, X, Nielson, F, Nielson, HR & Feng, X 2016, Disjunctive Information Flow for Communicating Processes. in P Ganty & M Loreti (eds), Revised Selected Papers of the 10th International Symposium on Trustworthy Global Computing (TGC 2015). Springer, Lecture Notes in Computer Science, vol. 9533, pp. 95-111, 10th International Symposium on Trustworthy Global Computing (TGC 2015), Madrid, Spain, 31/08/2015. https://doi.org/10.1007/978-3-319-28766-9_7

Disjunctive Information Flow for Communicating Processes. / Li, Ximeng; Nielson, Flemming; Nielson, Hanne Riis; Feng, Xinyu.

Revised Selected Papers of the 10th International Symposium on Trustworthy Global Computing (TGC 2015). ed. / Pierre Ganty; Michele Loreti. Springer, 2016. p. 95-111 (Lecture Notes in Computer Science, Vol. 9533).

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

TY - GEN

T1 - Disjunctive Information Flow for Communicating Processes

AU - Li, Ximeng

AU - Nielson, Flemming

AU - Nielson, Hanne Riis

AU - Feng, Xinyu

PY - 2016

Y1 - 2016

N2 - 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].

AB - 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].

U2 - 10.1007/978-3-319-28766-9_7

DO - 10.1007/978-3-319-28766-9_7

M3 - Article in proceedings

SN - 978-3-319-28765-2

SP - 95

EP - 111

BT - Revised Selected Papers of the 10th International Symposium on Trustworthy Global Computing (TGC 2015)

A2 - Ganty, Pierre

A2 - Loreti, Michele

PB - Springer

ER -

Li X, Nielson F, Nielson HR, Feng X. Disjunctive Information Flow for Communicating Processes. In Ganty P, Loreti M, editors, Revised Selected Papers of the 10th International Symposium on Trustworthy Global Computing (TGC 2015). Springer. 2016. p. 95-111. (Lecture Notes in Computer Science, Vol. 9533). https://doi.org/10.1007/978-3-319-28766-9_7