Evidence-Based Audit

8 years 8 months ago
Evidence-Based Audit
Authorization logics provide a principled and flexible approach to specifying access control policies. One of their compelling benefits is that a proof in the logic is evidence that an access-control decision has been made in accordance with policy. Using such proofs for auditing reduces the trusted computing base and enables the ability to detect flaws in complex authorization policies. Moreover, the proof structure is itself useful, because proof normalization can yield information about the relevance of policy statements. Untrusted, but well-typed, applications that access resources through an appropriate interface must obey the access control policy and create proofs useful for audit. This paper presents AURA0, an authorization logic based on a dependently-typed variant of DCC and proves the metatheoretic properties of subject-reduction and normalization. It shows the utility of proof-based auditing in a number of examples and discusses several pragmatic issues that must be add...
Jeffrey A. Vaughan, Limin Jia, Karl Mazurak, Steve
Added 29 May 2010
Updated 29 May 2010
Type Conference
Year 2008
Where CSFW
Authors Jeffrey A. Vaughan, Limin Jia, Karl Mazurak, Steve Zdancewic
Comments (0)