=Paper=
{{Paper
|id=Vol-2072/paper5
|storemode=property
|title=Schritte zu einer zertifizierten Informationsflussanalyse von Geschäftsprozessen (Towards a Certified Information Flow Analysis for Business Processes)
|pdfUrl=https://ceur-ws.org/Vol-2072/paper5.pdf
|volume=Vol-2072
|authors=Thomas Heinze
|dblpUrl=https://dblp.org/rec/conf/zeus/Heinze18
}}
==Schritte zu einer zertifizierten Informationsflussanalyse von Geschäftsprozessen (Towards a Certified Information Flow Analysis for Business Processes)==
https://ceur-ws.org/Vol-2072/paper5.pdf
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