CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Flow locks: Towards a core calculus for dynamic flow policies

N. Broberg ; David Sands (Institutionen för data- och informationsteknik, Datavetenskap (Chalmers))
Lecture Notes in Computer Science Vol. 3924 (2006), p. 180-196.
[Konferensbidrag, refereegranskat]

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.

Denna post skapades 2009-12-01.
CPL Pubid: 102557


Läs direkt!

Länk till annan sajt (kan kräva inloggning)

Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Datavetenskap (Chalmers)


Information Technology

Chalmers infrastruktur