Schritte zu einer zertifizierten Informationsflussanalyse von Gesch¨aftsprozessen

Abstract

This paper introduces an easy to use methodology to analyze the information flow within business processes based on diferent confidentiality levels. Furthermore, this paper also provides a formal proof based on Coq for this methodology. Zusammenfassung. In diesem Beitrag wird eine einfache Methode zur Analyse des Informationsflusses in Gesch ¨aftsprozessen auf Grundlage von Vertraulichkeitsstufen vorgestellt. Die Korrektheit der Analyse wird anhand einer maschinenpru¨fbaren Formalisierung in Coq nachgewiesen.

-

3. Estimate

Risk 6. Send $rating $request.risk = $score otherwise $request.insurant = ’premium’ 4. Assign Rating 5. Create $rating

Abb. 1. Beispielprozess in BPMN-Notation

des Informationsflusses in Gesch ¨aftsprozessen auf Grundlage von Vertraulichkeitsstufen vorgestellt. Die Analyse beruht auf dem Verfahren der AndersenAnalyse [ 16 ] und wurde mit Hilfe des Beweisassistenten Coq1 formal definiert, so dass der Nachweis der Analysekorrektheit als maschinenpru¨fbarer Beweis zur Verfu¨gung steht. Der Beitrag kann somit als ein Schritt zu einer zertifizierten Informationsflussanalyse von Gescha¨ftsprozessen verstanden werden.

Im sich anschließenden Abschnitt 2 wird das Analyseszenario genauer abgegrenzt und die Analyse vorgestellt. Die formale Entwicklung und der Korrektheitsnachweis zur Analyse auf Grundlage der Theorie der abstrakten Interpretation erfolgt in Abschnitt 3. In Abschnitt 4 wird ein kurzer U¨berblick zu verwandten Arbeiten gegeben, bevor der Beitrag mit einer Zusammenfassung und einem Ausblick auf weiterfu¨hrende Arbeiten in Abschnitt 5 endet. 2

Analyse des Informationsflusses

Eine Informationsflussanalyse [ 7 ] untersucht einen Prozess hinsichtlich des Flusses von Informationen, wobei verschiedene Vertraulichkeitsstufen beru¨cksichtigt werden ko¨nnen. Im einfachsten Fall werden die zwei Stufen H (vertraulich) und L (o¨fentlich) betrachtet. Zur Sicherstellung der Vertraulichkeit sollte dann kein Informationsfluss von einer mit H ausgezeichneten Quelle an eine mit L ausgezeichnete Senke existieren. In Abbildung 1 ist ein Beispielprozess dargestellt, in dem die Risikobewertung fu¨r eine Versicherung bestimmt und versendet wird. Dazu wird zuna¨chst ein Formular in $request erzeugt und der vertrauliche ScoreWert $score abgefragt. In Abh¨angigkeit vom Versichertenstatus wird entweder ein Standardwert oder der Score-Wert als Risikobewertung $rating verwendet und weitergeleitet. Wird in diesem Beispiel die eingehende Nachricht $score mit der Vertraulichkeitsstufe H und die ausgehende Nachricht $rating mit der Stufe L ausgezeichnet, liegt fu¨r den oberen Pfad ein Informationsfluss von H nach L und somit eine Verletzung der Informationsvertraulichkeit vor.

Hier soll eine statische Datenflussanalyse zur Untersuchung des Informationsflusses in Prozessmodellen definiert werden. Gegenstand der Analyse sind explizite Datenfl u¨sse, wie im obigen Beispiel, jedoch keine impliziten Informationsfl u¨sse oder Seitenkana¨le (vergleiche den impliziten Fluss von $request.insurant 1 https://coq.inria.fr, letzter Zugrif am 8. M a¨rz 2018 i : ReceiveL x/ i : CreateL x : i : ReceiveH x/ i : CreateH x : oiL ∈ pt(x) oiH ∈ pt(x) x = y : x = y.f : x.f = y :

oiL ∈ pt(y) pt(oi.f ) ⊆ pt(x)

oiL ∈ pt(x) pt(y) ⊆ pt(oi.f ) pt(y) ⊆ pt(x)

oiH ∈ pt(y) pt(oi.f ) ⊆ pt(x)

oiH ∈ pt(x) pt(y) ⊆ pt(oi.f )

Abb. 2. Regelsystem zur statischen Informationsflussanalyse

nach $rating u¨ber die Kontrollabh¨angigkeit der Variablendefinition). Unter diesen Anforderungen l¨asst sich die Analyse als Taint-Analyse [ 14 ] aufassen und auf das Verfahren der Andersen-Analyse [ 16 ] zuru¨ckfu¨hren. Durch dieses Verfahren werden Variablen, und deren Komponenten im Fall zusammengesetzter Variablentypen, Mengen mit abstrakten Objekten zugewiesen. Weiterhin werden Regeln zwischen den Mengen in Form von Element-/Teilmengenbeziehungen definiert. Die L ¨osung des dadurch charakterisierten Regelsystems ergibt dann einen Fixpunkt als Abscha¨tzung zum Datenfluss im analysisertem Prozess.

In Abbildung 2 sind die Regeln der Analyse fu¨r einen kleinen Sprachausschnitt dargestellt. Auf der linken Seite stehen die Prozessaktivita¨ten und auf der rechten Seite die zugeho¨rigen Regelschemata. Zusa¨tzlich zu einer herko¨mmlichen Andersen-Analyse wird hier zwischen o¨fentlichen und vertraulichen Informationsquellen unterschieden, so dass die Aktivit¨aten Receive und Create eine entsprechende Auszeichnung mit L oder H aufweisen mu¨ssen. Komplexere Sprachkonstrukte, etwa die Zuweisung x.f.g = y.h, lassen sich durch die Einfu¨hrung zus¨atzlicher Variablen ebenfalls abbilden. Ferner wird von atomaren Nachrichten ausgegangen.

Durch die Regeln wird fu¨r jede Prozessaktivit¨at beschrieben, wie deren Ausfu¨hrung die den Variablen und Komponenten zugeordneten Mengen pt mit abstrakten Objekten beeinflusst. Als Fixpunktl ¨osung ergibt sich fu¨r die Regeln dann eine U¨berabsch¨atzung des Datenflusses, da Ausf u¨hrungsreihenfolge und -kontext von Aktivita¨ten unberu¨cksichtigt bleiben (fluss-/kontextinsensitiv [ 16 ]). Zudem wird pro Receive- und Create-Aktivita¨t i nur jeweils ein abstraktes Objekt oi unterschieden, unabha¨ngig davon wie oft die Aktivita¨t ausgefu¨hrt wird. Wird der Beispielprozess in Abbildung 1 betrachtet, und von einer vertraulichen Quelle $score sowie einer ¨ofentlichen Quelle $ request ausgegangen, ergibt sich unter Anwendung der Regeln die folgende Ableitung und somit eine Vertraulichkeitsverletzung, unter Annahme der Vertraulichkeitsstufe L fu¨r die ausgehende Nachricht $rating (Regelanwendungen sind mit der zugeho¨rigen Aktivita¨ts-Id angegeben): L o1 ∈ pt($request) 1

4 pt(o1.risk) ⊆ pt($rating)

H o2 ∈ pt($rating)

L o1 ∈ pt($request) 1

3 pt($score) ⊆ pt(o1.risk)

H o2 ∈ pt(o1.risk)

H o2 ∈ pt($score) 2

Abb. 3. Konkrete Semantik (Pra¨dikat [exec] in Coq-Formalisierung)

3

Zertifizierte Informationsflussanalyse

Im Folgenden soll die im vorangegangenen Abschnitt vorgestellte Analyse formal definiert und deren Korrektheit bewiesen werden. Die Formalisierung erfolgte mit Hilfe des Beweisassistenten Coq, so dass ein maschinenpru¨fbarer Beweis zur Analysekorrektheit2 zur Verfu¨gung steht und die Implementierung der Analyse aus dem Beweis extrahiert werden kann. Der Coq-Formalismus beruht dabei wesentlich auf bestehenden Coq-Quellen3 zur Andersen-Analyse.

Fu¨r die formale Entwicklung einer statischen Analyse kann auf die abstrakten Interpretation zuru¨ckgegrifen werden [ 6 ]. In der abstrakten Interpretation wird ein Prozess nicht auf konkreten sondern auf abstrakten Werten ausgefu¨hrt. Anstatt mit int-Werten wird etwa mit den Werten odd und even gerechnet, so dass sich die Addition aus den Regeln even + even = even, even + odd = odd, odd + even = odd und odd + odd = even ergibt. Die Ausfu¨hrung auf konkreten Werten definiert die konkrete Semantik und die Ausfu¨hrung auf abstrakten Werten die abstrakte Semantik. Letztere wird zur Definition der Analyse verwendet, fu¨r die ausgehend von einem Startzustand durch kontinuierliche Anwendung der abstrakten Semantik auf einen Prozess ein Fixpunkt errechnet wird. Zum Nachweis der Korrektheit muss gezeigt werden, dass der Fixpunkt die sich fu¨r jeden Zustand aus der konkreten Semantik ergebenden konkreten Werte abscha¨tzt.

Zur Formalisierung der Informationsflussanalyse wird die in Abbildung 3 dargestellte konkrete Semantik genutzt. Darin werden Variablen, Komponenten und Objekte als natu¨rliche Zahlen kodiert. Ein Zustand s enstpricht einem Tupel (vars, heap, high, l), wobei vars, heap : N → N Variablen und Komponenten die Objekte zuordnet, auf die sie im Zustand s verweisen, high ⊆ N alle vertraulichen Objekte aufza¨hlt und l ∈ N das zuletzt erzeugte Objekt bezeichnet. Die konkrete Semantik denfiiert damit eine Relation i, s → s′ zwischen einem Zustand s, einer 2 https://gitlab.com/t.heinze/zeus2018.git 3 http://adam.chlipala.net/itp/coq/src, letzter Zugrif am 8. M a¨rz 2018 ReceiveL x#k/ CreateL x#k, (avars, aheap, ahigh)

→ (avars[x ← avars(x) ∪ {k}], aheap, ahigh) ReceiveH x#k/ CreateH x#k (avars, aheap, ahigh)

→ (avars[x ← avars(x) ∪ {k}], aheap, ahigh ∪ {k}) x = y, (avars, aheap, ahigh) → (avars[x ← avars(x) ∪ avars(y)], aheap, ahigh) x = y.f, (avars, aheap, ahigh) → (avars[x ← avars(x) ∪

[ k∈avars(y)

aheap(k)], aheap, ahigh) x.f = y, (avars, aheap, ahigh)

→ (avars, aheap[k ← aheap(k) ∪ avars(y) | k ∈ avars(x)], ahigh)

Abb. 4. Abstrakte Semantik (Pra¨dikat [abstract exec] in Coq-Formalisierung)

auf diesem ausgefu¨hrten Prozessaktivita¨t i und dem sich daraus ergebenden Folgezustand s′. Durch die Relation wird beispielsweise fu¨r eine Aktivita¨t CreateH x im Folgezustand ein neues Objekt l + 1 erzeugt, der Menge vertraulicher Objekt hinzugefu¨gt und der Verweis der Variablen x auf das Objekt l + 1 gesetzt.

In der abstrakten Semantik in Abbildung 4 werden abstrakte Zust¨ande betrachtet, die Tupel (avars, aheap, ahigh) sind, wobei avars, aheap : N → P(N) nun die m¨oglichen Verweisziele von Variablen und Komponenten in Form von Mengen abscha¨tzen (vergleiche auch Abbildung 2), ahigh fasst alle vertraulichen Objekte zusammen. Im Gegensatz zur konkreten Semantik wird nicht mehr fu¨r jede Ausfu¨hrung einer Receive- oder Create-Aktivit¨at ein neues Objekt erzeugt, sondern fu¨r dieselbe Aktivita¨t nur ein Objekt verwendet. Die Aktivita¨ten werden dazu durchnummeriert, so dass sich das Objekt aus dem Index k ergibt.

Fu¨r den Nachweis der Korrektheit werden die konkrete und die abstrakte Semantik in Beziehung gesetzt, dies mittels sogenannter Objektpfade: s = (vars, heap, high, l) s = (vars, heap, high, l) s ⊢ p :: l′ l′ ̸= 0 s ⊢ v :: vars[v] s ⊢ p :: l′ :: heap[l′] a = (avars, aheap, ahigh) k ∈ avars[v]

a ⊢ v :: k a = (avars, aheap, ahigh) a ⊢ p :: k k′ ∈ aheap[k]

a ⊢ p :: k :: k′

Ein Objektpfad v :: p :: n ist ein Pra¨dikat, das ausgehend von einer Variablen v, unter einen gegebenen konkreten Zustand s beziehungsweise abstrakten Zustand a, eine eventuell leere Sequenz p von Kompontenenzugrifen auf ein Objekt n beschreibt. Vereinfacht gesprochen bezeichnet ein Objektpfad die Mo¨glichkeit unter Zustand s beziehungsweise a u¨ber die Variable v auf das Objekt n zuzugreifen. Wie in Abbildung 5 definiert, ist ein abstrakter Zustand a dann eine Abscha¨tzung fu¨r einen konkreten Zustand s, falls zus¨atzlich zu gewissen Nebenbedingungen folgende zwei Bedingungen erfu¨llt sind: (1) Fu¨r jedes Objekt l′ auf das im Zustand s u¨ber Objektpfade v1 :: p :: l′ und v2 :: q :: l′ zugegrifen werden kann, existiert im Zustand a ein entsprechendes Objekt k auf das u¨ber Objektpfade v1 :: p′ : k a = (avars, aheap, ahigh) approximates s = (vars, heap, high, l) ⇔df heap(0) = 0 ∧ ∀l′ > l : heap(l′) = 0 ∧ ∀l′ : s ⊢ p :: l′ ⇒ l′ ≤ l ∧ ∀l′ ∈ high : l′ ≤ l ∧ ∀v1, v2, l′ ̸= 0 : s ⊢ v1 :: p :: l′ ∧ v2 :: q :: l′ ⇒ ∃k : a ⊢ v1 :: p′ :: k ∧ a ⊢ v2 :: q′ :: k ∧ ∀v, l′ ̸= 0 : s ⊢ v :: p :: l ∧ l ∈ high ⇒ ∃k : a ⊢ v :: q :: k ∧ k ∈ ahigh

Konservativita¨t der abstrakten Semantik:

∀a′, s′, s : s′ ⇝ s ∧ a′ approximates s′ ⇒ ∃a : a′ ⇝ a ∧ a approximates s ⊓⊔ v not H ⇔df ∀s = (vars, heap, high, l) : init ⇝ s ⇒ vars(v) ∈/ high

Korrektheit der Informationsflussanalyse:

∀v : (∀a = (avars, aheap, ahigh) : ainit ⇝ a ⇒ ∀k ∈ avars(v) : k ∈/ ahigh) ⇒ v not H ⊓⊔ Abb. 5. Korrektheit der Analyse (Theorem [analysis sound] in Coq-Formalisierung) und v2 :: q′ :: k zugegrifen werden kann. (2) F u¨r jedes vertrauliche Objekt l′ auf das u¨ber einen Objektpfad v :: p :: l′ im Zustand s zugegrifen werden kann, existiert im Zustand a ein entsprechendes vertrauliches Objekt k auf das u¨ber einen Objektpfad v :: q :: k zugegrifen werden kann. Anhand dieser Definitionen la¨sst sich zeigen, dass die abstrakte Semantik eine konservative Abscha¨tzung fu¨r die konkrete Semantik ist, das heißt fu¨r alle erreichbaren konkreten Zust¨ande s existiert ein erreichbarer abstrakter Zustand a, der eine Abscha¨tzung fu¨r s ist.

Als Folgerung aus dieser Beziehung zwischen konkreter und abstrakter Semantik kann auf die Korrektheit der Informationsflussanalyse geschlossen werden. So la¨sst sich zeigen, dass fu¨r alle Variablen v gilt, falls v unter allen erreichbaren abstrakten Zusta¨nden a auf kein vertrauliches Objekt verweist, so verweist v auch unter allen erreichbaren konkreten Zust¨anden s auf kein vertrauliches Objekt. Unter Anwendung der Analyse kann somit ein Fluss von einer vertraulichen Quelle an eine o¨fentliche Senke, in Form einer Variablen v, sicher ausgeschlossen werden. Neben der Korrektheit der Analyse kann auch deren Terminierung gezeigt werden. Aus Platzgru¨nden wird auf eine entsprechende Diskussion verzichtet und stattdessen auf die Coq-Formalisierung (Definition [fixed point]) verwiesen. 4

Verwandte Arbeiten

In [ 8 ] wurde der Ansatz zur zertifizierten Analyse von Gesch a¨ftsprozessen zuna¨chst allgemein motiviert, in diesem Beitrag konnte die Machbarkeit des Ansatzes nun konkret am Beispiel der Analyse des Informationsflusses von Gesch a¨ftsprozessen gezeigt werden. Die Pru¨fung des Informationsflusses ist dabei ein Standardproblem der statischen Analyse [ 7 ]. Es gibt zahlreiche Varianten, die neben expliziten Datenfl u¨ssen auch Seitenkan¨ale, zum Beispiel das Zeitverhalten oder den Energieverbrauch, einbeziehen. Informationsflussanalysen werden neben dem hier betrachteten Aufdecken von Informationslecks insbesondere zur Identizfiierung von Sicherheitslu¨cken eingesetzt, oft in Form einer Taint-Analyse [ 14 ]. Eine gela¨ufige Technik zur Taint-Analyse ist das Andersen-Verfahren [ 16 ]. Fu¨r dieses wird zwischen inter- und intraprozeduralen, fluss- und kontextsensitiven sowie -insensitiven Varianten unterschieden. Das hier beschriebene Verfahren setzt eine sehr einfache intraprozedurale und fluss-/kontextinsensitive Analyse um.

Der Einsatz von Beweisassistenten zur Verifikation von statischen Analysen erfa¨hrt eine stetig wachsende Verbreitung. Insbesondere Coq spielt eine herausragende Rolle, wie nicht zuletzt an der erfolgreichen Verifikation eines realistischen optimierenden Compilers im CompCert-Projekt [ 13 ] deutlich wird. Im Allgemeinen wird zum Nachweis der Analysekorrektheit analog dem Vorgehen in diesem Beitrag auf die Theorie der abstrakten Interpretation zuru¨ckgegrifen [ 4,5 ]. Neben den auch dieser Arbeit zugrundeliegenden Coq-Quellen zum Andersen-Verfahren von Adam Chlipala existieren weitere entsprechende Formalisierungen [ 11,15 ].

Eine Reihe von typischerweise petrinetzbasierten Techniken zur Analyse des Informationsflusses wird auch f u¨r Gescha¨ftsprozesse beschrieben, eine U¨ bersicht kann etwa [ 1 ] entnommen werden. Die hier vorgestellte Analyse bezieht sich dabei auf den expliziten Datenfluss und Vertraulichtkeitsstufen ( Mandatory Access Control). Vergleichbare Arbeiten fu¨r Gescha¨ftsprozesse beruhen meist auf ho¨heren Petrinetzen und Methoden des Model-Checking [ 3,12 ]. Damit ergeben sich aber zwei Problemstellungen, die fu¨r den in dieser Arbeit beschriebenen Ansatz nicht auftreten. So stellen sich fu¨r das Model-Checking auf ho¨heren Petrinetzen aufgrund potentieller Zustandsraumexplosion grundlegende Skalierungsprobleme. Durch eine geschickte Wahl der Abstraktion in den Petrinetzmodellen lassen sich diese zwar prinzipiell umgehen, jedoch bedingt dies dann eine aufwendige und nicht triviale manuelle Modellierung der zu analysierenden Gesch¨aftsprozesse. Ferner ist dem Autor kein Ansatz zur zertifizierten Informationsflussanalyse, das heißt maschinell verifizierten Analyse, f u¨r Gescha¨ftsprozesse bekannt. 5

Zusammenfassung und Ausblick

In diesem Beitrag wird eine einfache statische Analyse zur Untersuchung des Informationsflusses in Gesch ¨aftsprozessen vorgestellt. Mit Hilfe der Analyse lassen sich Datenfl u¨sse von sensitiven Datenquellen an o¨fentliche Senken f u¨r einen Prozess sicher ausschließen. Die Analyse beruht auf dem Verfahren der AndersenAnalyse und ist mittels der Theorie der abstrakten Interpretation formalisiert, so dass sich Korrektheit und Terminierung im Beweisassistent Coq maschinenpru¨fbar beweisen lassen. Da zudem die Mo¨glichkeit besteht, die Analyseimplementierung aus dem Beweis zu extrahieren, handelt es sich um einen ersten Schritt zu einer zertifizierten Informationsflussanalyse fu¨r Gescha¨ftsprozesse.

In weiterfu¨hrenden Arbeiten sollen Fragen zur Pr¨azision und Skalierbarkeit der Analyse untersucht werden. So kann die Pr¨azision durch Definition einer flusssensitiven Analyse erh ¨oht werden, etwa unter Verwendung erweiterter Workflow-Graphen [ 9,10 ]. In diesem Fall ist aber eine Formalisierung der Transformation in erweiterte Workflow-Graphen in Coq notwendig. Danksagung. Ich danke Adam Chlipala fu¨r die Bereitstellung der Coq-Quellen zur Andersen-Analyse.

Literatur

References

1. Accorsi , Rafael ; Lehmann, Andreas ; Lohmann, Niels: Information leak detection in business process models: Theory, application, and tool support . In: Information Systems 47 ( 2015 ), S. 244 - 257

2. Accorsi , Rafael ; Lowis, Lutz ; Sato, Yoshinori: Automated Certification for Compliant Cloud-based Business Processes . In: Business & Information Systems Engineering 3 ( 2011 ), Nr . 3, S. 145- 154

3. Barkaoui , Kamel ; Ayed, Rahma B. ; Boucheneb , Hanifa ; Hicheur, Awatef: Verification of Workflow Processes Under Multilevel Security Considerations . In: Proceedings, Third International Conference on Risks and Security of Internet and Systems , CRiSIS 2008 , Tozeur, Tunisia, October 28-30 , 2008 , IEEE, 2008 , S. 77 - 84

4. Bertot , Yves: Structural Abstract Interpretation: A Formal Study Using Coq . In: Language Engineering and Rigorous Software Development, International LerNet ALFA SummerSchool 2008 , Piriapolis, Urugay, February 24-March 1 , 2008 , Revised Tutorial Lectures. Springer, 2009 (LNCS 5520), S. 153 - 194

5. Besson , Fr´ed´eric ; Cachera, David ; Jensen, Thomas ; Pichardie, David: Certiifed Static Analysis by Abstract Interpretation . In: Foundations of Security Analysis and Design V. Springer, 2009 (LNCS 5705), S. 223 - 257

6. Cousot , Patrick ; Cousot, Radhia: Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs . In: Proceedings of the 4th ACM Symposium on Principles of Programming Languages, ACM , 1977 , S. 238 - 252

7. Denning , Dorothy E.: A Lattice Model of Secure Information Flow . In: Communications of the ACM 19 ( 1976 ), Nr . 5, S. 236- 243

8. Heinze , Thomas S.: Towards Certified Data Flow Analysis of Business Processes . In: 9th ZEUS Workshop , ZEUS 2017, Lugano, Switzerland, 13 -14 February 2017 , Proceedings, CEUR-WS.org, 2017 (CEUR Workshop Proceedings 1826 ), S. 1-3

9. Heinze , Thomas S. ; Amme, Wolfram ; Moser, Simon: A Restructuring Method for WS-BPEL Business Processes Based on Extended Workflow Graphs . In: Business Process Management, 7th International Conference, BPM 2009, Ulm, Germany, September 8- 10 , 2009 , Proceedings, Springer, 2009 (LNCS 5701), S. 211 - 228

10. Heinze , Thomas S. ; Amme, Wolfram ; Moser, Simon: Static analysis and process model transformation for an advanced business process to Petri net mapping . In: Software: Practice and Experience 48 ( 2018 ), Nr . 1, S. 161- 195

11. Jourdan , Jacques-Henri ; Laporte, Vincent ; Blazy, Sandrine ; Leroy, Xavier ; Pichardie, David: A Formally-Verified C Static Analyzer . In: ACM SIGPLAN Notices 50 ( 2015 ), Nr . 1, S. 247- 259

12. Juszczyszyn , Krzysztof: Verifying Enterprise's Mandatory Access Control Policies with Coloured Petri Nets . In: 12th International Workshops on Enabling Technologies: Infrastructure for Collaborative Enterprises , IEEE, 2003 , S. 184 - 189

13. Leroy , Xavier: Formal Verification of a Realistic Compiler . In: Communications of the ACM 52 ( 2009 ), Nr . 7, S. 107- 115

14. Livshits , V. B. ; Lam , Monica S.: Finding Security Vulnerabilities in Java Applications with Static Analysis . In: Proceedings of the 14th USENIX Security Symposium, USENIX Association , 2005 , S. 271 - 286

15. Robert , Valentin ; Leroy, Xavier: A Formally-Verified Alias Analysis . In: Certified Programs and Proofs , Second International Conference, CPP 2012, Kyoto, Japan, December 13-15 , 2012 , Proceedings, Springer, 2009 (LNCS 7679), S. 11 - 26

16. Sridharan , Manu ; Chandra, Satish ; Dolby, Julian ; Fink, Stephen J. ; Yahav, Eran: Alias Analysis for Object-Oriented Programs . In: Aliasing in Object-Oriented Programming . Springer, 2013 (LNCS 7850), S. 196 - 232