Skip to content

Flow locks: Towards a core calculus for dynamic flow policies

34Citations
Citations of this article
10Readers
Mendeley users who have this article in their library.

This artice is free to access.

Abstract

Security is rarely a static notion. What is considered to be confidential or untrusted data varies over time according to changing events and states. The static verification of secure information flow has been a popular theme in recent programming language research, but information flow policies considered are based on multilevel security which presents a static view of security levels. In this paper we introduce a very simple mechanism for specifying dynamic information flow policies, flow locks, which specify conditions under which data may be read by a certain actor. The interface between the policy and the code is via instructions which open and close flow locks. We present a type and effect system for an ML-like language with references which permits the completely static verification of flow lock policies, and prove that the system satisfies a semantic security property generalising noninterference. We show that this simple mechanism can represent a number of recently proposed information flow paradigms for declassification. © Springer-Verlag Berlin Heidelberg 2006.

Cite

CITATION STYLE

APA

Broberg, N., & Sands, D. (2006). Flow locks: Towards a core calculus for dynamic flow policies. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3924 LNCS, pp. 180–196). https://doi.org/10.1007/11693024_13

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free