Several recent security-typed programming languages, such as Aura,
PCML5, and Fine, allow programmers to express and enforce access control
and information flow policies. In this paper, we show that
security-typed programming can be embedded as a library within a
general-purpose dependently typed programming language, Agda. Our
library, Aglet, accounts for the major features of existing
security-typed programming languages, such as decentralized access
control, typed proof-carrying authorization, ephemeral and dynamic
policies, authentication, spatial distribution, and information flow.
The implementation of Aglet consists of the following ingredients:
First, we represent the syntax and proofs of an authorization logic,
Garg and Pfenning's BL$_0$, using dependent types. Second, we implement
a proof search procedure, based on a focused sequent calculus, to ease
the burden of constructing proofs. Third, we represent computations
using a monad indexed by pre- and post-conditions drawn from the
authorization logic, which permits ephemeral policies that change during
execution. We describe the implementation of our library and illustrate
its use on benchmark examples considered in the literature.