Schritte zu einer zertifizierten Informationsflussanalyse von Geschäftsprozessen Thomas S. Heinze Institut für Informatik Friedrich-Schiller-Universität Jena t.heinze@uni-jena.de Abstract. This paper introduces an easy to use methodology to analyze the information flow within business processes based on different confi- dentiality 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äftsprozessen auf Grundlage von Vertraulichkeitsstufen vorgestellt. Die Korrektheit der Analyse wird anhand einer maschinenprüfbaren Formalisierung in Coq nachgewiesen. 1 Einführung und Motivation Die statische Datenflussanalyse ist ein geeignetes Werkzeug zur Unterstützung der Geschäftsprozessmodellierung und -analyse. Wie bereits in [8] ausgeführt, bietet sie nicht nur ein allgemein einsetzbares Rahmenwerk zur Prozessanalyse, sondern beruht gleichzeitig auch auf der wohldefinierten Theorie der abstrakten Interpre- tation [6], die sich leicht zum formalen Korrektheitsnachweis heranziehen lässt. In Verbindung mit modernen maschinengestützten Beweisassistenten gestattet die Formalisierung von Datenflussanalysen auf Grundlage der abstrakten Interpre- tation schließlich die Definition sogenannter zertifizierter Analysen. Grundlage einer solchen zertifizierten Analyse bildet dabei ein maschinenprüfbarer Beweis der Analysekorrektheit, aus dem sich die Analyseimplementierung extrahieren lässt. Der Vorteil liegt dann auf der Hand, da ein Anwender nun nicht mehr auf die Korrektheit der Implementierung vertrauen muss, sondern stattdessen den Korrektheitsbeweis automatisiert nachvollziehen kann. In einem Auditszenario ließe sich derart die Compliance-Prüfung von Geschäftsprozessen [2] durch eine orthogonale Prüfung zur Vertrauenswürdigkeit des Audits selbst ergänzen. Ein Beispiel für ein solches Szenario ist die Analyse von Informationsflüssen, oder genauer die Untersuchung des Flusses von Informationen in einem Prozess- modell, mit der sich etwa Compliance-Regeln zur vertraulichen Verarbeitung von sensitiven Informationen, beispielsweise Gesundheitsdaten, überprüfen lassen. In diesem Beitrag wird eine erste einfache statische Datenflussanalyse zur Analyse N. Herzberg, C. Hochreiner, O. Kopp, J. Lenhard (Eds.): 10th ZEUS Workshop, ZEUS 2018, Dresden, Germany, 8-9 February 2018, published at http://ceur-ws.org/Vol-2072 Zertifizierte Informationsflussanalyse von Geschäftsprozessen 25 $rating = $request.risk $request.risk = $score otherwise 4. Assign Rating 1. Create 2. Receive 3. Estimate 6. Send $request $score Risk $rating 5. Create $request.insurant = ’premium’ $rating Abb. 1. Beispielprozess in BPMN-Notation des Informationsflusses in Geschäftsprozessen auf Grundlage von Vertraulich- keitsstufen vorgestellt. Die Analyse beruht auf dem Verfahren der Andersen- Analyse [16] und wurde mit Hilfe des Beweisassistenten Coq 1 formal definiert, so dass der Nachweis der Analysekorrektheit als maschinenprüfbarer Beweis zur Verfügung steht. Der Beitrag kann somit als ein Schritt zu einer zertifizierten Informationsflussanalyse von Geschäftsprozessen verstanden werden. Im sich anschließenden Abschnitt 2 wird das Analyseszenario genauer abge- grenzt und die Analyse vorgestellt. Die formale Entwicklung und der Korrektheits- nachweis zur Analyse auf Grundlage der Theorie der abstrakten Interpretation erfolgt in Abschnitt 3. In Abschnitt 4 wird ein kurzer Überblick zu verwandten Arbeiten gegeben, bevor der Beitrag mit einer Zusammenfassung und einem Ausblick auf weiterführende Arbeiten in Abschnitt 5 endet. 2 Analyse des Informationsflusses Eine Informationsflussanalyse [7] untersucht einen Prozess hinsichtlich des Flus- ses von Informationen, wobei verschiedene Vertraulichkeitsstufen berücksichtigt werden können. Im einfachsten Fall werden die zwei Stufen H (vertraulich) und L (öffentlich) betrachtet. Zur Sicherstellung der Vertraulichkeit sollte dann kein Informationsfluss von einer mit H ausgezeichneten Quelle an eine mit L ausge- zeichnete Senke existieren. In Abbildung 1 ist ein Beispielprozess dargestellt, in dem die Risikobewertung für eine Versicherung bestimmt und versendet wird. Dazu wird zunächst ein Formular in $request erzeugt und der vertrauliche Score- Wert $score abgefragt. In Abhängigkeit 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 fü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 Informati- onsflusses in Prozessmodellen definiert werden. Gegenstand der Analyse sind explizite Datenflüsse, wie im obigen Beispiel, jedoch keine impliziten Informati- onsflüsse oder Seitenkanäle (vergleiche den impliziten Fluss von $request.insurant 1 https://coq.inria.fr, letzter Zugriff am 8. März 2018 26 Thomas Heinze i : Receive L x/ i : Create L x : oL i ∈ pt(x) H H i : Receive x/ i : Create x: oH i ∈ pt(x) x=y: pt(y) ⊆ pt(x) oL i ∈ pt(y) oH i ∈ pt(y) x = y.f : pt(oi .f ) ⊆ pt(x) pt(oi .f ) ⊆ pt(x) oL i ∈ pt(x) oH i ∈ pt(x) x.f = y : pt(y) ⊆ pt(oi .f ) pt(y) ⊆ pt(oi .f ) Abb. 2. Regelsystem zur statischen Informationsflussanalyse nach $rating über die Kontrollabhängigkeit der Variablendefinition). Unter die- sen Anforderungen lässt sich die Analyse als Taint-Analyse [14] auffassen und auf das Verfahren der Andersen-Analyse [16] zurückführen. Durch dieses Ver- fahren 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ösung des dadurch charakterisierten Regelsystems ergibt dann einen Fixpunkt als Abschätzung zum Datenfluss im analysisertem Prozess. In Abbildung 2 sind die Regeln der Analyse für einen kleinen Sprachausschnitt dargestellt. Auf der linken Seite stehen die Prozessaktivitäten und auf der rechten Seite die zugehörigen Regelschemata. Zusätzlich zu einer herkömmlichen Ander- sen-Analyse wird hier zwischen öffentlichen und vertraulichen Informationsquellen unterschieden, so dass die Aktivitäten Receive und Create eine entsprechende Auszeichnung mit L oder H aufweisen müssen. Komplexere Sprachkonstrukte, etwa die Zuweisung x.f.g = y.h, lassen sich durch die Einführung zusätzlicher Variablen ebenfalls abbilden. Ferner wird von atomaren Nachrichten ausgegangen. Durch die Regeln wird für jede Prozessaktivität beschrieben, wie deren Ausführung die den Variablen und Komponenten zugeordneten Mengen pt mit abstrakten Objekten beeinflusst. Als Fixpunktlösung ergibt sich für die Regeln dann eine Überabschätzung des Datenflusses, da Ausführungsreihenfolge und -kontext von Aktivitäten unberücksichtigt bleiben (fluss-/kontextinsensitiv [16]). Zudem wird pro Receive- und Create-Aktivität i nur jeweils ein abstraktes Objekt oi unterschieden, unabhängig davon wie oft die Aktivität ausgeführt wird. Wird der Beispielprozess in Abbildung 1 betrachtet, und von einer vertraulichen Quelle $score sowie einer öffentlichen Quelle $request ausgegangen, ergibt sich unter Anwendung der Regeln die folgende Ableitung und somit eine Vertraulichkeitsver- letzung, unter Annahme der Vertraulichkeitsstufe L für die ausgehende Nachricht $rating (Regelanwendungen sind mit der zugehörigen Aktivitäts-Id angegeben): 1 oL 1 ∈ pt($request) 1 3 2 oL 1 ∈ pt($request) pt($score) ⊆ pt(o1 .risk) oH 2 ∈ pt($score) 4 pt(o1 .risk) ⊆ pt($rating) oH 2 ∈ pt(o1 .risk) oH 2 ∈ pt($rating) Zertifizierte Informationsflussanalyse von Geschäftsprozessen 27 Receive L x/ Create L x, (vars, heap, high, l) → (vars[x ← l + 1], heap, high, l + 1) Receive H x/ Create H x, (vars, heap, high, l) → (vars[x ← l + 1], heap, high ∪ {l + 1}, l + 1) x = y, (vars, heap, high, l) → (vars[x ← vars(y)], heap, high, l) heap(vars(y)) ̸= 0 x = y.f, (vars, heap, high, l) → (vars[x ← heap(vars(y))], heap, high, l) heap(vars(y)) = 0 x = y.f, (vars, heap, high, l) → (vars, heap, high, l) vars(x) ̸= 0 x.f = y, (vars, heap, high, l) → (vars, heap[vars(x) ← vars(y)], high, l) vars(x) = 0 x.f = y, (vars, heap, high, l) → (vars, heap, high, l) Abb. 3. Konkrete Semantik (Prä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 maschinenprüfbarer Beweis zur Analysekorrektheit2 zur Verfü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. Für die formale Entwicklung einer statischen Analyse kann auf die abstrakten Interpretation zurückgegriffen werden [6]. In der abstrakten Interpretation wird ein Prozess nicht auf konkreten sondern auf abstrakten Werten ausgefü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 Ausführung auf konkreten Werten definiert die konkrete Semantik und die Ausführung auf abstrakten Werten die abstrakte Semantik. Letztere wird zur Definition der Analyse verwendet, fü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 für jeden Zustand aus der konkreten Semantik ergebenden konkreten Werte abschätzt. Zur Formalisierung der Informationsflussanalyse wird die in Abbildung 3 dargestellte konkrete Semantik genutzt. Darin werden Variablen, Komponenten und Objekte als natü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 aufzählt und l ∈ N das zuletzt erzeugte Objekt bezeichnet. Die konkrete Semantik definiert 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 Zugriff am 8. März 2018 28 Thomas Heinze Receive L x#k/ Create L x#k, (avars, aheap, ahigh) → (avars[x ← avars(x) ∪ {k}], aheap, ahigh) Receive H x#k/ Create H 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) ∪ aheap(k)], aheap, ahigh) k∈avars(y) x.f = y, (avars, aheap, ahigh) → (avars, aheap[k ← aheap(k) ∪ avars(y) | k ∈ avars(x)], ahigh) Abb. 4. Abstrakte Semantik (Prädikat [abstract exec] in Coq-Formalisierung) auf diesem ausgeführten Prozessaktivität i und dem sich daraus ergebenden Fol- gezustand s′ . Durch die Relation wird beispielsweise für eine Aktivität Create H x im Folgezustand ein neues Objekt l + 1 erzeugt, der Menge vertraulicher Objekt hinzugefügt und der Verweis der Variablen x auf das Objekt l + 1 gesetzt. In der abstrakten Semantik in Abbildung 4 werden abstrakte Zustände be- trachtet, die Tupel (avars, aheap, ahigh) sind, wobei avars, aheap : N → P(N) nun die möglichen Verweisziele von Variablen und Komponenten in Form von Mengen abschätzen (vergleiche auch Abbildung 2), ahigh fasst alle vertraulichen Objekte zusammen. Im Gegensatz zur konkreten Semantik wird nicht mehr für jede Ausführung einer Receive- oder Create-Aktivität ein neues Objekt erzeugt, sondern für dieselbe Aktivität nur ein Objekt verwendet. Die Aktivitäten werden dazu durchnummeriert, so dass sich das Objekt aus dem Index k ergibt. Fü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 Prädikat, das ausgehend von einer Variablen v, unter einen gegebenen konkreten Zustand s beziehungsweise abstrakten Zustand a, eine eventuell leere Sequenz p von Kompontenenzugriffen auf ein Objekt n be- schreibt. Vereinfacht gesprochen bezeichnet ein Objektpfad die Möglichkeit unter Zustand s beziehungsweise a über die Variable v auf das Objekt n zuzugreifen. Wie in Abbildung 5 definiert, ist ein abstrakter Zustand a dann eine Abschätzung für einen konkreten Zustand s, falls zusätzlich zu gewissen Nebenbedingungen folgende zwei Bedingungen erfüllt sind: (1) Für jedes Objekt l′ auf das im Zustand s über Objektpfade v1 :: p :: l′ und v2 :: q :: l′ zugegriffen werden kann, existiert im Zustand a ein entsprechendes Objekt k auf das über Objektpfade v1 :: p′ : k Zertifizierte Informationsflussanalyse von Geschäftsprozessen 29 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 Konservativitä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 zugegriffen werden kann. (2) Für jedes vertrauliche Objekt l′ auf das über einen Objektpfad v :: p :: l′ im Zustand s zugegriffen werden kann, existiert im Zustand a ein entsprechendes vertrauliches Objekt k auf das über einen Objektpfad v :: q :: k zugegriffen werden kann. Anhand dieser Definitionen lässt sich zeigen, dass die abstrakte Semantik eine konservative Abschätzung für die konkrete Semantik ist, das heißt für alle erreichbaren konkreten Zustände s existiert ein erreichbarer abstrakter Zustand a, der eine Abschätzung für s ist. Als Folgerung aus dieser Beziehung zwischen konkreter und abstrakter Se- mantik kann auf die Korrektheit der Informationsflussanalyse geschlossen werden. So lässt sich zeigen, dass für alle Variablen v gilt, falls v unter allen erreichbaren abstrakten Zuständen a auf kein vertrauliches Objekt verweist, so verweist v auch unter allen erreichbaren konkreten Zuständen s auf kein vertrauliches Objekt. Unter Anwendung der Analyse kann somit ein Fluss von einer vertraulichen Quelle an eine öffentliche Senke, in Form einer Variablen v, sicher ausgeschlossen werden. Neben der Korrektheit der Analyse kann auch deren Terminierung gezeigt werden. Aus Platzgrü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äftsprozessen zunächst allgemein motiviert, in diesem Beitrag konnte die Machbarkeit des Ansatzes nun konkret am Beispiel der Analyse des Informationsflusses von Geschäftsprozessen gezeigt werden. Die Prüfung des Informationsflusses ist dabei ein Standard- problem der statischen Analyse [7]. Es gibt zahlreiche Varianten, die neben expliziten Datenflüssen auch Seitenkanäle, zum Beispiel das Zeitverhalten oder den Energieverbrauch, einbeziehen. Informationsflussanalysen werden neben dem hier betrachteten Aufdecken von Informationslecks insbesondere zur Identifizie- rung von Sicherheitslücken eingesetzt, oft in Form einer Taint-Analyse [14]. Eine geläufige Technik zur Taint-Analyse ist das Andersen-Verfahren [16]. Für dieses wird zwischen inter- und intraprozeduralen, fluss- und kontextsensitiven sowie 30 Thomas Heinze -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 erfährt eine stetig wachsende Verbreitung. Insbesondere Coq spielt eine herausra- gende Rolle, wie nicht zuletzt an der erfolgreichen Verifikation eines realistischen optimierenden Compilers im CompCert-Projekt [13] deutlich wird. Im Allgemei- nen wird zum Nachweis der Analysekorrektheit analog dem Vorgehen in diesem Beitrag auf die Theorie der abstrakten Interpretation zurückgegriffen [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ür Geschäftsprozesse beschrieben, eine Übersicht kann etwa [1] entnommen werden. Die hier vorgestellte Analyse bezieht sich dabei auf den expliziten Datenfluss und Vertraulichtkeitsstufen (Mandatory Access Control). Vergleichbare Arbeiten für Geschäftsprozesse beruhen meist auf höheren Petrinetzen und Methoden des Model-Checking [3,12]. Damit ergeben sich aber zwei Problemstellungen, die für den in dieser Arbeit beschriebenen Ansatz nicht auftreten. So stellen sich für das Model-Checking auf hö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äftsprozesse. Ferner ist dem Autor kein Ansatz zur zertifizierten Informationsflussanalyse, das heißt maschinell verifizierten Analyse, für Geschäftsprozesse bekannt. 5 Zusammenfassung und Ausblick In diesem Beitrag wird eine einfache statische Analyse zur Untersuchung des Informationsflusses in Geschäftsprozessen vorgestellt. Mit Hilfe der Analyse lassen sich Datenflüsse von sensitiven Datenquellen an öffentliche Senken für einen Prozess sicher ausschließen. Die Analyse beruht auf dem Verfahren der Andersen- Analyse und ist mittels der Theorie der abstrakten Interpretation formalisiert, so dass sich Korrektheit und Terminierung im Beweisassistent Coq maschinenprüfbar beweisen lassen. Da zudem die Möglichkeit besteht, die Analyseimplementierung aus dem Beweis zu extrahieren, handelt es sich um einen ersten Schritt zu einer zertifizierten Informationsflussanalyse für Geschäftsprozesse. In weiterführenden Arbeiten sollen Fragen zur Präzision und Skalierbar- keit der Analyse untersucht werden. So kann die Präzision durch Definition einer flusssensitiven Analyse erhöht werden, etwa unter Verwendung erweiter- ter 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 für die Bereitstellung der Coq-Quellen zur Andersen-Analyse. Zertifizierte Informationsflussanalyse von Geschäftsprozessen 31 Literatur 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édéric ; Cachera, David ; Jensen, Thomas ; Pichardie, David: Certi- fied 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: Communi- cations 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 Po- licies 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 Applica- tions 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