Direkt zum Inhalt | Direkt zur Navigation

Eingang zum Volltext

Lizenz

Bitte beziehen Sie sich beim Zitieren dieses Dokumentes immer auf folgende
URN: urn:nbn:de:bsz:25-opus-60483
URL: http://www.freidok.uni-freiburg.de/volltexte/6048/


Accorsi, Rafael

Automated counterexample-driven audits of authentic system records

Automatisierte auf Gegenbeispielen basierte Audits von authentischen Systemaufzeichnungen

Dokument1.pdf (4.387 KB) (md5sum: 7e3abfdd66123df8504ec4f182767671)

Kurzfassung in Englisch

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.


Kurzfassung in Deutsch

Die Durchsetzung von Richtlinien in Computersystemen ist von großer Bedeutung, um das Auftreten unzulässiger Zustände zu verhindern. Unter anderem im Zusammenhang mit der Nutzungskontrolle, dem Schutz der Privatsphäre und der Einhaltung gesetzlicher Auflagen (der sog. Compliance) ist dies unabdingbar.

Bislang werden Ausführungsmonitore eingesetzt, um Richtlinien zur Laufzeit durchzusetzen. Dies reicht jedoch wegen der zunehmenden Forderung nach nachweisbarer Durchsetzung und der Unmöglichkeit, manche Elemente der Richtlinien während der Ausführung erzwingen zu können, allein nicht aus. Somit müssen nachträgliche, von unabhängigen Dritten durchgeführte Analysen der Ereignisprotokolle eines Systems herangezogen werden, um Evidenzen, also Nachweise, über die Einhaltung der Richtlinien zu erzeugen bzw. die Quelle aufgetretener Verletzungen aufzuzeigen. Derartige Analysen nennt man Audits.

Trotz der Notwendigkeit von Audits weisen derzeitige Verfahren die folgenden Mängel auf:

• Mechanismen zur Aufzeichnung von Ereignisprotokollen gewährleisten nur bedingt die Authentizität der erfassten und gespeicherten Ereignisse, sodass eine angemessene Basis für Audits nicht garantiert werden kann.

• Audits sind bestenfalls halbautomatisiert. Dies wirkt sich nicht nur auf die Zeit und Kosten negativ aus, die zur Durchführung von Audits benötigt werden, sondern auch auf die Korrektheit und Glaubwürdigkeit erzeugter Evidenzen.

Die vorliegende Arbeit führt ein neues Audit-Modell ein, das diese Mängel behebt, und beschreibt den Aufbau, die Eigenschaften und die Implementierung seiner wesentlichen Komponenten, nämlich BBox und ExaMINA. Ähnlich einem Flugschreiber ist die BBox eine digitale Black-Box zur Gewährleistung authentischer und manipulationssicherer Aufzeichnung von Ereignisprotokollen, welche auch die Erzeugung gefilterter Ereignisprotokolle ermöglicht und damit den Aufwand für Audits reduziert.

Anhand einer beispielhaften Sprache zum Ausdruck von Richtlinien, führt ExaMINA automatisierte Audits durch und generiert dabei Evidenzen über die Einhaltung der Richtlinien. Zur Durchführung von Audits verwendet ExaMINA die Falsifikation: anstatt zu zeigen, dass das System die Regeln einer Richtlinie einhält, durchsucht ExaMINA die Ereignisprotokolle nach Gegenbeispielen. Da die Existenz eines Gegenbeispiels zur Falsifikation genügt, ermöglichen gegenbeispiel-orientierte Audits eine schnellere Erzeugung von Evidenzen im Falle von Verletzungen.


SWD-Schlagwörter: Computersicherheit , Privatsphäre , Revision <Wirtschaft> , Logdatei , Algorithmus , Computerforensik
Freie Schlagwörter (deutsch): Automatisierte Audit , Falsifikation , Gegenbeispiele , Sichere Aufzeichnung , Digitale evidenz
Freie Schlagwörter (englisch): Automated Audits , Falsification , Counterexample , Digital Evidence , Secure Logging
CCS Klassifikation Public Pol , Management , Regulation , Distribute , Security a
Institut: Institut für Informatik
Fakultät: Technische Fakultät (bisher: Fak. f. Angew. Wiss.)
DDC-Sachgruppe: Informatik
Dokumentart: Dissertation
Erstgutachter: Müller, Günter (Prof. Dr.)
Sprache: Englisch
Tag der mündlichen Prüfung: 07.11.2008
Erstellungsjahr: 2008
Publikationsdatum: 01.12.2008
Bemerkung: Verwandte Veröffentlichungen . S. Sackmann, J. Strüker, R. Accorsi. Personalization in Privacy-Aware Highly Dynamic Systems Comm. ACM, vol. 49(9), pp. 32-38, Sept. 2006 . R. Accorsi. Automated Privacy Audits to Complement the Notion of Control for Identity Management. Vol. 261 of IFIP, Springer-Verlag, 2008. . Rafael Accorsi. On the Relationship of Privacy and Secure Remote Logging in Dynamic Systems. Vol. 201 of IFIP, Springer-Verlag, 2008. . R. Accorsi and A. Hohl. Delegating Secure Logging in Pervasive Computing Systems. Security in Pervasive Computing. Vol. 3934 of LNCS, Springer-Verlag 2006.
Indexliste