[TYPES] Paper: Dynamic security labels and noninterference

[Lantian Zheng]

Those working on language-based information flow may be interested in
our forthcoming paper (in the Workshop on Formal Aspects of Security
and Trust), abstract below. The paper is available at URL:
http://www.cs.cornell.edu/zlt/papers/dynlabel.pdf or
http://www.cs.cornell.edu/andru/pubs.html.

Comments and suggestions are most welcome.

-- Lantian

                  Dynamic Security Labels and Noninterference
                          Lantian Zheng, Andrew Myers
                               Cornell University


    This paper gives a language in which information flow is securely
    controlled by a dependent type system, yet the security classes of
    data can vary dynamically.  Information flow policies provide the
    means to express strong security requirements for data
    confidentiality and integrity.  Recent work on security-typed
    programming languages has shown that information flow can be
    analyzed statically, ensuring that programs will respect the
    restrictions placed on data.  However, real computing systems have
    security policies that vary dynamically and that cannot be
    determined at the time of program analysis. For example, a file has
    associated access permissions that cannot be known with certainty
    until it is opened.  Although one security-typed programming
    language has included support for dynamic security labels, there has
    been no demonstration that a general mechanism for dynamic labels
    can securely control information flow.  In this paper, we present an
    expressive language-based mechanism for reasoning about dynamic
    security labels.  The mechanism is formally presented in a core
    language based on the typed lambda calculus; any well-typed program
    in this language is provably secure because it satisfies
    noninterference.