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

Cite this

@article{e942b36f72af4213a3aa1b7a4173256e,
title = "Enforcing globally dependent flow policies in message-passing systems",
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.",
keywords = "Dependent flow policies, Information flow security, Security type system, Static analysis",
author = "Ximeng Li and Flemming Nielson and Nielson, {Hanne Riis}",
year = "2019",
month = "10",
day = "1",
doi = "10.1016/j.cola.2019.100904",
language = "English",
volume = "54",
journal = "Journal of Computer Languages",
issn = "2665-9182",

}

Enforcing globally dependent flow policies in message-passing systems. / Li, Ximeng; Nielson, Flemming; Nielson, Hanne Riis.

In: Journal of Computer Languages, Vol. 54, 100904, 01.10.2019.

Research output: Contribution to journalJournal articleResearchpeer-review

TY - JOUR

T1 - Enforcing globally dependent flow policies in message-passing systems

AU - Li, Ximeng

AU - Nielson, Flemming

AU - Nielson, Hanne Riis

PY - 2019/10/1

Y1 - 2019/10/1

N2 - 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.

AB - 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.

KW - Dependent flow policies

KW - Information flow security

KW - Security type system

KW - Static analysis

U2 - 10.1016/j.cola.2019.100904

DO - 10.1016/j.cola.2019.100904

M3 - Journal article

VL - 54

JO - Journal of Computer Languages

JF - Journal of Computer Languages

SN - 2665-9182

M1 - 100904

ER -