@inbook{0d48625e59dd48258030127152c088e4,
title = "Secure Guarded Commands",
abstract = "We develop a lightweight approach to information flow control that interacts with the use of cryptographic schemes. The language is a version of Dijkstra{\textquoteright}s Guarded Commands language extended with parallelism, communication and symmetric cryptography. Information flow is modelled using security labels that are sets of hashed symmetric keys expressing the capabilities needed for access to data. In essence, encryption is used to encapsulate the protection offered by the information flow policy. We develop a type system aimed at tracking explicit, implicit, bypassing and correlation flows arising due to the parallel processes and the internal non-determinism inherent in Guarded Commands. The development is facilitated by the parallel processes having disjoint memories and is illustrated on a multiplexer scenario previously addressed using content-dependent information flow policies.",
author = "Flemming Nielson and Nielson, {Hanne Riis}",
year = "2020",
month = jan,
day = "1",
doi = "10.1007/978-3-030-41103-9_7",
language = "English",
isbn = "978-3-030-41102-2",
series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",
publisher = "Springer",
pages = "201--215",
editor = "{Di Pierro}, A, and {Malacaria }, P. and {Nagarajan }, R.",
booktitle = "From Lambda Calculus to Cybersecurity Through Program Analysis",
}