Dynamic DCC Related Reading
Types and Access Control
- Access Control in a Core Calculus of
- A Core Calculus of Dependency
(Abadi, Banerjee, Heintze, Riecke)
These papers describe two versions of DCC, the immediate inspiration
for the Dynamic DCC language we would like to implement. The single
author was published later, but I think is an easier read and a better
place to start. The four author paper is more general and explains
how DCC can be used to model a variety of analyses.
- A Type Discipline for Authorization
Polices (Fournet, Gordon, and Maffeis)
This paper gives a pi-calculus with the special type constructor OK.
The type OK(S) has the intended semantics that policy S holds, where
S is a datalog term. Their terms give only a single inhabitant of
OK(S) for any S; this means that they do not actually pass proofs at
runtime. There is a later paper which expresses policies in dcc,
but it's not publicly available yet.
The Curry-Howard Isomorphism
- Proofs are Programs: 19th Century Logic and
21st Century Computing (Wadler)
In Dynamic DCC, we plan to use digital signatures as verifiable
assertion which can be used as part of a proof. The remainder of
a proof will be constructed with lambda calculus like terms. This
paper gives a succinct overview of Curry-Howard isomorphism, which
says that "programs are proofs."
(David Aspinall and Martin Hofmann—Chapter 2 in
Advanced Types and Programming Languages edited B.C. Pierce)
Dependent types allow types to mention terms. Dependent types are
essential for fully exploiting the Curry-Howard isomorphism.
- The Haskell Programmer's Guide to the IO
The "P says" type constructor in DCC is (almost) a monad. This paper
discusses monads in Haskell with some lightweight category theory.
I've only skimmed this, but it looks cool and there's good buzz on
Lambda the Ultimate.
- The Marriage of Effects and Monads
(Wadler and Thiemann)
A little dense, but looks like a good starting point for learning about
the monads and effects-types.
- An Idealized MetaML Simpler, and More
Expressivei (Moggi, Taha, Benaissa, and Sheard)
- A Modal Analysis of Staged Computation
(Davies and Pfenning)
- Implementing Multi-stage Languages Using ASTs,
Gensym, and Reflection (Calcagno, Taha, Huang, and Leory)
I haven't read these yet. The first two appear to address
staged computation along the lines of Context Modal Type Theory (below).
The latter takes a different tact.
- Run-time principals in information flow type
systems (Tse and Zdancewic)
An information flow language the ability the run dynamic queries on
principals and branch to code in which the query has been statically
assumed to be true (or false). This similar to the dynamic typecheck
we want for dynamic dcc.
- Language-Based Information-Flow Security
(Sabelfeld and Myers)
A thorough survey of information flow security papers.
Compiling Functional Programs
- A Standard ML Compiler
(Appel and MacQueen)
A light description of the first SML compiler implemented in Standard
ML. This highlights pattern compilation and the use of simple
lambda calculus as an intermediate representation language.
- Implementing Functional Languages: A
Tutorial (Peyton Jones and Lester)
This book is much for in depth than the above paper and gives a Miranda
implementation or a compiler for a core functional language. Peyton
Jones has an earlier book, "The Implementation of Functional
Programming Languages," but, he says, it is less practically
- Trust Management: Features and Foundations
(Chapin, Skalka, and Wang)
A survey of trust managment systems.
- Contextual Modal Type Theory
(Nanevski, Pfenning, and Pientka)
Includes a short discussion of quoting/unquoting terms that
are closed except for a few variables.
- Cryptographic Sealing for Information Secrecy
and Authentication (Gifford)
Discusses how to realize compound security policies in terms of
digital signing and encryption.
- The Confused Deputy
(Norm Hardy; OS Review 1988)
- Protection in Operating Systems
(Harrison, Ruzzo, and Ullman; CACM 1976)
- Paradigm regained: Abstraction Mechanisms
for Access Control (Miller and Shapiro; ASIAN 2003)
- The Structure of Authority: Why Security is not
a separable concern (Miller, Tulloh, and Shapiro; LNCS 3389)
A practical formal model for safety analysis in capability-based
systems (Spiessens and Van Roy; Trustworthy Global