Aglet
Security-typed programming within dependently typed programming. 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 a number of the benchmark examples considered in the literature.
This software is also peer reviewed by journal TOMS.
This software is also peer reviewed by journal TOMS.
Keywords for this software
References in zbMATH (referenced in 4 articles , 1 standard article )
Showing results 1 to 4 of 4.
Sorted by year (- Stefan, Deian; Mazières, David; Mitchell, John C.; Russo, Alejandro: Flexible dynamic information flow control in the presence of exceptions (2017)
- Broberg, Niklas; van Delft, Bart; Sands, David: Paragon for practical programming with information-flow control (2013) ioport
- Stefan, Deian; Russo, Alejandro; Buiras, Pablo; Levy, Amit; Mitchell, John C.; Maziéres, David: Addressing covert termination and timing channels in concurrent information flow systems (2012)
- Morgenstern, Jamie; Licata, Daniel R.: Security-typed programming within dependently typed programming (2010)