Encoding Information Flow in AURA, Technical Appendix

Two of the main ways to protect security-sensitive resources in computer systems are to enforce access-control policies and information-flow policies. In this paper, we show how to enforce information-flow policies in AURA, which is a programming language for access control. When augmented with this mechanism for enforcing information-flow polices, AURA can further improve the security of reference monitors that implement access control. We show how to encode security types and lattices of security labels using AURA’s existing constructs for authorization logic. We prove a noninterference theorem for this encoding. We also investigate how to use expressive access control policies specified in authorization logic as the policies for information declassification