Evidence-Based Audit, Technical Appendix

摘要: Authorization logics provide a principled and flexible approach to specifying access control policies. One of their compelling benefits is that proof in the logic evidence an access-control decision has been made accordance with policy. Using such proofs for auditing reduces trusted computing base enables ability detect flaws complex authorization Moreover, structure itself useful, because normalization can yield information about relevance policy statements. Untrusted, but well-typed, applications resources through appropriate interface must obey create useful audit. This paper presents AURA0, based on dependently-typed variant DCC proves metatheoretic properties subject-reduction normalization. It shows utility proof-based number examples discusses several pragmatic issues be addressed this context.