Retrospective security has become increasingly important to the theory and practice of cyber security, with auditing a crucial component of it. However, in systems where auditing is used, programs are typically instrumented to generate audit logs using manual, ad-hoc techniques. We propose a foundational semantics for auditing, intended to support provable correctness of program rewriting algorithms that instrument formal logging specifications. Correctness guarantees that the execution of an instrumented program produces sound and complete audit logs, properties defined by an information containment relation between logs and the program's logging semantics.

 

We study two applications of our theory that support a defense in depth approach to security, in particular the combination of retrospective audit logging with prospective access control mechanisms in a single uniform policy specification. As a first application, we consider break-the-glass policies, which are common in healthcare informatics when the need to access information in emergency situations overrides "normal" security concerns. As a second application, we consider an in depth approach to a dynamic taint analysis defense against injection attacks, in the presence of partially trusted sanitization. A program rewriting implementation of these mechanisms for the OpenMRS medical records software system is current work in progress.