Abstract
We develop a type system for identifying the information flow between variables in a program in the Guarded Commands language. First we characterise the types of information flow that may arise between variables in a non-deterministic program: explicit, implicit, bypassing, correlated or sanitised. Next we allow to specify security policies in a number of traditional ways based on mandatory access control: defining a security lattice, working with components or decentralised labels, both as pertains to confidentiality and integrity. Offending information flows are those identified by the type system and that violate the security policy; a program is sufficiently secure if it contains only acceptable information flows.
| Original language | English |
|---|---|
| Title of host publication | Models, Languages, and Tools for Concurrent and Distributed Programming |
| Publisher | Springer |
| Publication date | 1 Jan 2019 |
| Pages | 455-470 |
| ISBN (Print) | 978-3-030-21484-5 |
| DOIs | |
| Publication status | Published - 1 Jan 2019 |
| Series | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
|---|---|
| Volume | 11665 LNCS |
| ISSN | 0302-9743 |
Cite this
}
Lightweight information flow. / Nielson, Flemming; Nielson, Hanne Riis.
Models, Languages, and Tools for Concurrent and Distributed Programming. Springer, 2019. p. 455-470 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), Vol. 11665 LNCS).Research output: Chapter in Book/Report/Conference proceeding › Book chapter › Research › peer-review
TY - CHAP
T1 - Lightweight information flow
AU - Nielson, Flemming
AU - Nielson, Hanne Riis
PY - 2019/1/1
Y1 - 2019/1/1
N2 - We develop a type system for identifying the information flow between variables in a program in the Guarded Commands language. First we characterise the types of information flow that may arise between variables in a non-deterministic program: explicit, implicit, bypassing, correlated or sanitised. Next we allow to specify security policies in a number of traditional ways based on mandatory access control: defining a security lattice, working with components or decentralised labels, both as pertains to confidentiality and integrity. Offending information flows are those identified by the type system and that violate the security policy; a program is sufficiently secure if it contains only acceptable information flows.
AB - We develop a type system for identifying the information flow between variables in a program in the Guarded Commands language. First we characterise the types of information flow that may arise between variables in a non-deterministic program: explicit, implicit, bypassing, correlated or sanitised. Next we allow to specify security policies in a number of traditional ways based on mandatory access control: defining a security lattice, working with components or decentralised labels, both as pertains to confidentiality and integrity. Offending information flows are those identified by the type system and that violate the security policy; a program is sufficiently secure if it contains only acceptable information flows.
U2 - 10.1007/978-3-030-21485-2_25
DO - 10.1007/978-3-030-21485-2_25
M3 - Book chapter
AN - SCOPUS:85068818443
SN - 978-3-030-21484-5
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 455
EP - 470
BT - Models, Languages, and Tools for Concurrent and Distributed Programming
PB - Springer
ER -