Secure Guarded Commands

Flemming Nielson*, Hanne Riis Nielson

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingBook chapterResearchpeer-review


We develop a lightweight approach to information flow control that interacts with the use of cryptographic schemes. The language is a version of Dijkstra’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.

Original languageEnglish
Title of host publicationFrom Lambda Calculus to Cybersecurity Through Program Analysis
EditorsA, Di Pierro, P. Malacaria , R. Nagarajan
Publication date1 Jan 2020
ISBN (Print)978-3-030-41102-2
Publication statusPublished - 1 Jan 2020
SeriesLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume12065 LNCS


Dive into the research topics of 'Secure Guarded Commands'. Together they form a unique fingerprint.

Cite this