Enforcing globally dependent flow policies in message-passing systems

Ximeng Li*, Flemming Nielson, Hanne Riis Nielson

*Corresponding author for this work

Research output: Contribution to journalJournal articleResearchpeer-review

Abstract

The flow of information in a computing system is a crucial indicator for the security of the system. In a system of multiple message-passing processes, the flow of information could depend on the states of different processes. We devise a type-based verification technique for flow policies with such multi-process (global) dependencies, to provide confidentiality guarantees. In this technique, the confidentiality requirements for the presence and content of messages are dealt with separately. We develop a pair of synergetic static analyses to over-approximate the potential sets of values of the variables depended upon by the flow policies – covering global value correspondence between the variables of different processes. We significantly improve the permissiveness of security typing by exploiting information about which variables are live, and by specializing the flow policies using the conditional expressions of branching and looping constructs. We prove the soundness of our verification technique, provide a proof-of-concept implementation of it, and illustrate its effectiveness at an example system where the flow of information depends on how the headers of the messages from different processes correlate.

Original languageEnglish
Article number100904
JournalJournal of Computer Languages
Volume54
Number of pages46
ISSN2665-9182
DOIs
Publication statusPublished - 1 Oct 2019

Keywords

  • Dependent flow policies
  • Information flow security
  • Security type system
  • Static analysis

Fingerprint Dive into the research topics of 'Enforcing globally dependent flow policies in message-passing systems'. Together they form a unique fingerprint.

Cite this