Disjunctive Information Flow for Communicating Processes

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

doi:10.1007/978-3-319-28766-9_7

Disjunctive Information Flow for Communicating Processes

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

Department of Applied Mathematics and Computer Science

University of Science and Technology of China

Research output: Chapter in Book/Report/Conference proceeding › Article in proceedings › Research › peer-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 language	English
Title of host publication	Revised Selected Papers of the 10th International Symposium on Trustworthy Global Computing (TGC 2015)
Editors	Pierre Ganty, Michele Loreti
Publisher	Springer
Publication date	2016
Pages	95-111
ISBN (Print)	978-3-319-28765-2
ISBN (Electronic)	978-3-319-28766-9
DOIs	https://doi.org/10.1007/978-3-319-28766-9_7
Publication status	Published - 2016
Event	10th International Symposium on Trustworthy Global Computing (TGC 2015) - Madrid, Spain Duration: 31 Aug 2015 → 1 Sept 2015 Conference number: 10 http://tgc2015.disia.unifi.it/

Conference

Conference	10th International Symposium on Trustworthy Global Computing (TGC 2015)
Number	10
Country/Territory	Spain
City	Madrid
Period	31/08/2015 → 01/09/2015
Internet address	http://tgc2015.disia.unifi.it/

Series	Lecture Notes in Computer Science
Volume	9533
ISSN	0302-9743

Access to Document

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

OpenUrl availability

Full text

Cite this

@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",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "95--111",

editor = "Ganty, {Pierre } and Loreti, {Michele }",

booktitle = "Revised Selected Papers of the 10th International Symposium on Trustworthy Global Computing (TGC 2015)",

note = "10th International Symposium on Trustworthy Global Computing (TGC 2015), TGC ; Conference date: 31-08-2015 Through 01-09-2015",

url = "http://tgc2015.disia.unifi.it/",

}

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 et al.
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 proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - Disjunctive Information Flow for Communicating Processes

AU - Li, Ximeng

AU - Nielson, Flemming

AU - Nielson, Hanne Riis

AU - Feng, Xinyu

N1 - Conference code: 10

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

T3 - Lecture Notes in Computer Science

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

T2 - 10th International Symposium on Trustworthy Global Computing (TGC 2015)

Y2 - 31 August 2015 through 1 September 2015

ER -

Disjunctive Information Flow for Communicating Processes

Abstract

Conference

Access to Document

OpenUrl availability

Fingerprint

Cite this