Book chapter
Lightweight information flow
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.
Language: | English |
---|---|
Publisher: | Springer |
Year: | 2019 |
Pages: | 455-470 |
Series: | Lecture Notes in Computer Science (including Subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
Journal subtitle: | Essays Dedicated To Rocco De Nicola on the Occasion of His 65th Birthday |
ISBN: | 3030214842 , 3030214850 , 9783030214845 and 9783030214852 |
ISSN: | 03029743 |
Types: | Book chapter |
DOI: | 10.1007/978-3-030-21485-2_25 |
ORCIDs: | 0000-0002-1972-7491 , 0000-0003-3061-863X , 0000-0002-1419-1405 , Nielson, Flemming and Nielson, Hanne Riis |