Automated counterexample-driven audits of authentic system records
Rafael Accorsi · FreiDok plus (Universitätsbibliothek Freiburg) · 2008
In modern computer topics, such as usage control, privacy protection and regulatory compliance, it is essential to enforce that computer systems adhere to the policies governing their operation, i.e. to prevent systems from violating the policies by transitioning into an illegal state. Reference monitors are employed to enforce policies during the execution. However, the increasing demand to demonstrate correct policy enforcement and the impossibility to fully enforce some of the policy elements at runtime raise the need for audits to decide whether systems in fact obey the policies. In computer systems, an audit is the a posteriori examination of system records conducted by an independent third-party to generate evidence about policy adherence. Despite the soaring need for audits, current state-of-the-art exhibits the following shortcomings: • logging mechanisms do not completely provide for authentic system records, so that a suitable basis for audits is not guaranteed. • audits are at best semi-automated, which has a negative impact on the time and cost involved in conducting audits, as well as on the correctness and credibility of generated evidence. This thesis tackles these shortcomings by introducing a novel model for automated audits and elaborates on the design, properties and implementation of two of its components, namely the BBox and ExaMINA. Like a flight recorder, the BBox is a digital black box for systems. It employs a trusted co-processor and a secure logging mechanism to protect system records, thereby providing for authentic and tamper-evident system records. The BBox also allows the extraction of portions of the system records filtered according to some simple search criteria, which reduce the size of the system records to be audited. Using an exemplary policy language for the expression of policies, ExaMINA automatically audits selected system records against the corresponding policy and generates evidence. To conduct audits, ExaMINA uses falsification: instead of showing that the system adheres to each rule, ExaMINA searches the system records for counterexamples for the adherence to the policy, thereby trying to refute the hypothesis that the system to which the records belong obeys the policy. Since finding a single counterexample suffices for refutation, counterexampledriven audits have the potential to provide for faster evidence generation in case of policy violations.