Stephen Tse and Steve Zdancewic, University of Pennsylvania

Apollo project

Publications

Bibliography: stse.bib
  1. Run-time principals in information-flow type systems
    Stephen Tse and Steve Zdancewic
    IEEE Symposium on Security and Privacy (SP), 2004
    Full paper: pdf, ps, tex,
    Tech report: pdf, ps, tex, dir
    Talk: pdf, ps, tin
    Abstract Information-flow type systems are a promising approach for enforcing strong end-to-end confidentiality and integrity policies. Such policies, however, are usually specified in term of static information - data is labeled high or low security at compile time. In practice, the confidentiality of data may depend on information available only while the system is running.

    This paper studies language support for run-time principals, a mechanism for specifying information-flow security policies that depend on which principals interact with the system. We establish the basic property of noninterference for programs written in such language, and use run-time principals for specifying run-time authority in downgrading mechanisms such as declassification.

    In addition to allowing more expressive security policies, run-time principals enable the integration of language-based security mechanisms with other existing approaches such as Java stack inspection and public key infrastructures. We sketch an implementation of run-time principals via public keys such that principal delegation is verified by certificate chains.
  2. Translating dependency into parametricity
    Stephen Tse and Steve Zdancewic
    ACM International Conference on Functional Programming (ICFP), 2004
    Full paper: pdf, ps, tin, src
    Tech report: pdf, ps, tin, dir
    Reference: dcc, free
    Abstract Abadi et al. introduced the dependency core calculus (DCC) as a unifying framework to study many important program analyses such as binding time, information flow, slicing, and function call tracking. DCC uses a lattice of monads and a nonstandard typing rule for their associated bind operations to describe the dependency of computations in a program. Abadi et al. proved a noninterference theorem that establishes the correctness of DCC's type system and thus the correctness of the type systems for the analyses above.

    In this paper, we study the relationship between DCC and the Girard-Reynolds polymorphic lambda calculus (System F). We encode the recursion-free fragment of DCC into F via a type-directed translation. Our main theoretical result is that, following from the correctness of the translation, the parametricity theorem for F implies the noninterference theorem for DCC. In addition, the translation provides insights into DCC's type system and implementation strategies of dependency calculi in polymorphic languages.
  3. Designing a security-typed language with certificate-based declassification
    Stephen Tse and Steve Zdancewic
    European Symposium on Programming (ESOP), 2005
    Full paper: pdf, ps, tin, dir
    Tech report: pdf, ps, elf
    Abstract This paper presents the design of a programming language that supports information-flow security policies and certificate-based declassification.

    The language uses monadic information-flow annotations in the style of Abadi et al.'s dependency core calculus, and has an effects system and fixpoints. The type system conflates security concepts such as labels, principals, and privileges with abstract types, allowing a uniform treatment of lattice structures throughout the language. Myers' and Liskov's decentralized label model is encoded using type constructors that describe confidentiality and integrity policies, and label refinements and principal groups follow naturally from intersection and union types. Singleton types, combined with bounded universal and existential quantifications connect the type system with public-key infrastructures whose digital certificates provide authorization for privileged operations such as declassification. These features allow specification of security policies in term of dynamic entities such as run-time user identities and file access permissions.

    Besides showing that the language is sound, we present a security theorem that generalizes standard noninterference to account for information flows introduced by declassification. Although this result gives only a coarse approximation to the information potentially leaked, it captures our intuitions about certificate-based declassification.
  4. Dynamic updating of information-flow policies
    Michael Hicks, Stephen Tse, Boniface Hicks and Steve Zdancewic
    Foundations of Computer Security, 2005.
    Full paper: pdf
    Tech report: pdf, elf, tin
    Abstract Applications that manipulate sensitive information should satisfy two requirements. Namely, they should exhibit end-to-end security by governing information flow and sound execution by never performing an action inconsistent with the current policy, even as that policy changes over time. Language-based information flow analysis promises to be a critical component in making these guarantees. In previous research, security-typed language analyses have been developed to model many parts of real programs, including runtime principals. No current language-based analyses, however, allow for dynamically changing security policies. We have developed a type system for a simple, security-typed language which builds on techniques for dynamic software updating and allows for dynamic security policy updates. We have proven the main results of noninterference and soundness for this language. This is an important advance in language-based techniques which will provide a foundation for the future work of extending this language for use in building secure distributed applications.

Software

  1. Apollo: an interpreter for System F with subtyping and information flow. It is written in OCaml and uses Sugar generator (see below). (example, README, test, tgz)
  2. LF2TeX: visualize logic constraints (Twelf code) as natural deductions (proof trees in TeX). (link)
  3. Sugar: a concrete syntax grammar for generating scanners, parsers, printers and abstract-syntax definitions. (link)

Resources