Vorlesung Modellierung, Analyse, Veri kation ... · Programmveri kation Man m ochte zeigen, dass...
Transcript of Vorlesung Modellierung, Analyse, Veri kation ... · Programmveri kation Man m ochte zeigen, dass...
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Vorlesung Modellierung, Analyse, VerifikationWintersemester 2018/19
Prof. Barbara Konig
Barbara Konig Modellierung, Analyse, Verifikation 1
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Programmanalyse
Das heutige Programm:
Organisatorisches
Einfuhrendes Beispiel
Problemstellung (Was ist Programmanalyse?)
Anwendungsgebiete
Inhaltsangabe
Syntax und Semantik von While-Programmen
Barbara Konig Modellierung, Analyse, Verifikation 2
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Vorstellung
Dozentin: Prof. Barbara Konig
Raum LF 264
E-Mail: barbara [email protected]
Sprechstunde: nach Vereinbarung
Web-Seite:www.uni-due.de/theoinf/teaching/ws201819 mav.php
Barbara Konig Modellierung, Analyse, Verifikation 3
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Vorlesungstermine
Termine:
Dienstag, 8:30–10:00 Uhr, im Raum LC 137
Donnerstag, 8:30–10:00 Uhr, im Raum LC 137(jede 2. Woche)
Barbara Konig Modellierung, Analyse, Verifikation 4
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Ubung
Termin der Ubung:
Donnerstag, 8:30-10:00 Uhr, LC 137 (jede 2. Woche)
In der Regel wird jeden zweiten Donnerstag statt derVorlesung eine Ubung stattfinden.
Die erste Ubung findet am Donnerstag, den 25.10., statt.
Weitere Ubungstermine: siehe Webseite
Das Ubungsblatt wird eine Woche vor der Ubung auf derWebseite bereitgestellt, das erste Blatt am 18.10. Bittebereiten Sie sich mit Hilfe des Ubungsblattes auf die Ubungvor!
Barbara Konig Modellierung, Analyse, Verifikation 5
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Ubung
Bonusregelung:
In diesem Semester gibt es keine Bonusregelung. Bitte bearbeitenSie im eigenen Interesse trotzdem selbstandig die Ubungsaufgabenund stellen Sie Fragen in der Ubung.
Barbara Konig Modellierung, Analyse, Verifikation 6
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Prufung
Master “Angewandte Informatik”
Titel: Modellierung, Analyse, Verifikation (3V+1U)Bereich: Vertiefung der Informatik
Die Prufung wird als mundliche Prufung voraussichtlich anfolgenden Terminen stattfinden:
7./8. Februar 2019
Anmeldung uber das Prufungsamt
Barbara Konig Modellierung, Analyse, Verifikation 7
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Literatur
Flemming Nielson, Hanne Riis Nielson, Chris Hankin:Principles of Program Analysis, Springer-Verlag, 1999.
David Schmidt: Abstract interpretation and static analysis,International Winter School on Semantics and ApplicationsMontevideo, Uruguay, Juli 2003.santos.cis.ksu.edu/schmidt/Escuela03/home.html
Weitere Literatur: siehe Skript
Barbara Konig Modellierung, Analyse, Verifikation 8
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Folien & Skript
Folien werden
im Web bereitgestellt und
regelmaßig aktualisiert.
Die Folien des Vorjahres sind ebenfalls verfugbar.
Skript:
Es gibt ein relativ ausfuhrliches Skript (siehe Webseite), daswahrend der Vorlesung vermutlich noch etwas angepasst wird.
Trotzdem kann es sinnvoll sein, wenn Sie sich wahrend derVorlesung eigene Notizen machen.
Barbara Konig Modellierung, Analyse, Verifikation 9
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Verwendete Software
PAG/WWW – Programmanalyse-Generator
gcc – wie optimiert ein C-Compiler?
jasmin – Assembler fur Java-Bytecode (zum Testen des JavaBytecode Verifiers)
Barbara Konig Modellierung, Analyse, Verifikation 10
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel: Programmoptimierung
Eingabe: a,b Ausgabe: x
x:=a+b;y:=a*b;while (y>a+b) do
x:=0;a:=a+1;x:=a+b
od;if (a>2)
then x := x*yelse x := x*y+a
fi
Barbara Konig Modellierung, Analyse, Verifikation 11
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Was ist Programmanalyse? (I)
Berechnung semantischer Eigenschaften eines Programms, ohnedieses Programm auszufuhren(Daher oft auch statische Analyse genannt.)
Moment mal, was ist eigentlich mit dem Satz von Rice?
Jede nichttriviale Eigenschaft einer Turingmaschine (einesProgramms), die sich auf die von der Turingmaschine be-rechnete Funktion bezieht, ist unentscheidbar.
Zum Beispiel: Halteproblem fur Turingmaschinen
Ist das nicht ein Widerspruch?
Barbara Konig Modellierung, Analyse, Verifikation 12
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Was ist Programmanalyse? (II)
Losung: wir berechnen kein exaktes Analyseergebnis, sondern(uber-)approximieren nur (einseitiger Irrtum)
Exaktes Ergebnis
Ergebnis der Analyse
Gesamtmenge
Zum Beispiel: Menge der Variablen, die an einem bestimmtenProgrammpunkt lebendig sind (d.h. noch gebraucht werden)
Barbara Konig Modellierung, Analyse, Verifikation 13
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Anwendungsgebiete
Optimierung im Compilerbau
Typsysteme zum Aufdecken von Laufzeitfehlern (Typinferenz)
ProgrammverifikationMan mochte zeigen, dass ein Programm erwunschteEigenschaften (Terminierung, Abwesenheit vonLaufzeitfehlern, wechselseitiger Ausschluss, etc.) hat und dasses gegen boswillige Angriffe von außen (z.B. Zugriff aufgeheime Daten) geschutzt ist.
Barbara Konig Modellierung, Analyse, Verifikation 14
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Anwendungsgebiete
Allgemeiner:
Besseres Verstandnis von Programmen bzw.Software-Systemen
Fehler fruher aufdecken (moglichst noch in der Planungsphaseoder in fruhen Phasen der Software-Entwicklung)
Vermeiden von verhangnisvollen Software-Fehlern und Crashs,insbesondere bei sicherheitskritischen Anwendungen
Statische Analyse ist eine von mehreren Techniken, die man dazueinsetzen kann (neben Testen, Diagnose, Model-Checking,Theorem-Beweiser, . . . )
Die Forschung in diesem Bereich ist bei weitem noch nichtabgeschlossen!
Barbara Konig Modellierung, Analyse, Verifikation 15
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Software-Bugs
Es gibt in der Geschichte der Informatik und der Computer zahlloseBeispiele fur schwerwiegende Software-Fehler, die viel Geld undteilweise sogar Menschenleben gekostet haben:
www5.in.tum.de/persons/huckle/bugse.html
www.devtopics.com/20-famous-software-disasters/
de.wikipedia.org/wiki/Liste von Programmfehlerbeispielen
Viele von ihnen hatten durch Anwendung geeigneterProgrammanalyse-Techniken verhindert werden konnen.
Verifikations- und Analysetechniken zur Erkennung und Vemeidungvon Fehlern werden bereits in großerem Stil beim Chip-Designeingesetzt und halten langsam (aber sicher) auch Einzug in dieAnalyse von Softwaresystemen.
Barbara Konig Modellierung, Analyse, Verifikation 16
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Inhaltsangabe
While-Programme
Datenflussanalyse
Fixpunkttheorie
Java Bytecode Verifier
Abstrakte Interpretation
GrundlagenPradikatabstraktion und Abstraktionsverfeinerung
Barbara Konig Modellierung, Analyse, Verifikation 17
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Datenflussanalyse
Analyse eines Programms anhand desFlussdiagramms
Bei Verzweigungen werden im Allgemeinen beide Moglichkeitenbetrachtet
Anwendung: Optimierung im Compilerbau, aber auchProgrammverifikation
Barbara Konig Modellierung, Analyse, Verifikation 18
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Java Bytecode Verifier
...
Stack
...
Register
Typkorrektheit von Java Bytecode wirduberpruft
Beispiel: Kein Integer-Wert darf als Referenz benutzt werden
Ziel: Vermeidung von Laufzeitfehlern und inkorrekter Verwendungvon Datentypen, was zu Sicherheitslucken fuhren kann
Technik: Datenflussanalyse + Typsystem
Barbara Konig Modellierung, Analyse, Verifikation 19
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Abstrakte Interpretation
γ
α
Interpretation eines Programms aufabstrakten Werten
Beispiele:
“gerade”, “ungerade” statt Integer verwenden
“negativ”, “null”, “positiv” statt Integer verwenden
Allgemein: Abstraktionsfunktion α und Konkretisierungsfunktion γ
Anwendung: Verifikation von Programmen, wird auch furnebenlaufige und reaktive Systeme eingesetzt
Barbara Konig Modellierung, Analyse, Verifikation 20
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Abgrenzung: “Analyse von Algorithmen”
Analyse vonAlgorithmen Programmanalyse
Analyse von Laufzeitverhalten, SemantischeZeit/Platz-Komplexitat Eigenschaften,
Korrektheit
Benotigte O-Notation, Partielle Ordnungen,Mathematik Kombinatorik, Verbande,
Rekursions- Fixpunkttheoriegleichungen
Barbara Konig Modellierung, Analyse, Verifikation 21
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
While-Programme
Variablenbelegungen State = Var→ ZArithmetische Ausdrucke AExp mit AuswertungsfunktionA : AExp× State→ ZBoolesche Ausdrucke BExp mit AuswertungsfunktionB : BExp× State→ {true, false}Syntax:Zuweisung: [x:=a]`
Skip-Anweisung: [skip]`
Bedingte Anweisung: if [b]` then S1 else S2 fi
Schleife: while [b]` do S od
Sequentielle Komposition: S1;S2
Barbara Konig Modellierung, Analyse, Verifikation 22
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispielprogramm
[x:=a+b]1;[y:=a*b]2;while [y>a+b]3 do
[a:=a+1]4;[x:=a+b]5
od;
[z:=x]6
Barbara Konig Modellierung, Analyse, Verifikation 23
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Programme als Flussgraphen
[x:=a+b]1 [y:=a*b]2
[a:=a+1]4
yes [y>a+b]3no
[z:=x]6[x:=a+b]5
flow(S) = {(1, 2), (2, 3), (3, 4), (4, 5), (5, 3), (3, 6)}init(S) = 1
final(S) = {6}
Barbara Konig Modellierung, Analyse, Verifikation 24
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Analyse verfugbarer Ausdrucke
Wir wollen nun fur den Eingang und Ausgang jedes Blocksfolgende Menge bestimmen:
Die Menge aller arithmetischen Ausdrucke, die auf allenPfaden bis zu diesem Programmpunkt bereits berechnetwurden und nicht zwischendurch modifiziert wurden.
Barbara Konig Modellierung, Analyse, Verifikation 25
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Erwunschtes Analyseergebnis
` A◦(`) A•(`)
1 ∅ {a+b}2 {a+b} {a+b, a*b}3 {a+b} {a+b}4 {a+b} ∅5 ∅ {a+b}6 {a+b} {a+b}
[x:=a+b]1 [y:=a*b]2
[a:=a+1]4
yes [y>a+b]3no
[z:=x]6[x:=a+b]5
Barbara Konig Modellierung, Analyse, Verifikation 26
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Berechnung des Analyseergebnisses
kill- und gen-Funktionen
kill(`) =
{a′ ∈ AExp∗ | x ∈ Var(a′)}
falls block(`) = (x:=a)∅ sonst
gen(`) =
{a′ ∈ AExp(a) | x 6∈ Var(a′)}
falls block(`) = (x:=a)∅ falls block(`) = skip
AExp(b) falls block(`) = b
A•(`) = A◦(`)\kill(`) ∪ gen(`)
Barbara Konig Modellierung, Analyse, Verifikation 27
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Datenflussanalyse: Gleichungssystem
A◦(1) = ∅A◦(2) = A•(1)
A◦(3) = A•(2)
∩ A•(5)
A◦(4) = A•(3)
A◦(5) = A•(4)
A◦(6) = A•(3)
A•(1) = A◦(1) ∪ {a + b}A•(2) = A◦(2) ∪ {a ∗ b}A•(3) = A◦(3) ∪ {a + b}A•(4) = A◦(4)
\{a + b, a ∗ b, a + 1}A•(5) = A◦(5) ∪ {a + b}A•(6) = A◦(6)
Barbara Konig Modellierung, Analyse, Verifikation 28
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Ordnungen
Eine Ordnung (partielle Ordnung) auf einer Menge L ist eineRelation v ⊆ L× L, fur die gilt:
1 v ist reflexiv: ∀l ∈ L : (l v l).
2 v ist transitiv: ∀l1, l2, l3 ∈ L : (l1 v l2, l2 v l3 ⇒ l1 v l3).
3 v ist antisymmetrisch: ∀l1, l2 ∈ L : (l1 v l2, l2 v l1 ⇒ l1 = l2).
Barbara Konig Modellierung, Analyse, Verifikation 29
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Obere Schranken, maximale Elemente
Gegeben: Menge L mit Ordnung v.
Obere Schranke von Y ⊆ L: Element s ∈ L mit ∀l ∈ Y : l v s.
Kleinste obere Schranke/Supremum von Y : Element s fur dasgilt:
s ist eine obere Schranke von Y undfur jede andere obere Schranke s ′ von Y gilt s v s ′.
Maximales Element: m ∈ Y ist ein maximales Element von Y ,wenn fur jedes Element l ∈ Y mit m v l folgt, dass m = l .
Barbara Konig Modellierung, Analyse, Verifikation 30
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Untere Schranken, minimale Elemente, Notation
Analog: Definition von unterer Schranke, großter unterer Schranke(Infimum), minimalem Element
Notation:
Supremum von Y :⊔Y bzw. l1 t l2 =
⊔{l1, l2}
Infimum von Y :d
Y bzw. l1 u l2 =d{l1, l2}
Barbara Konig Modellierung, Analyse, Verifikation 31
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Vollstandiger Verband
Ein geordnete Menge (L,v) heißt vollstandiger Verband, wenn
jede Teilmenge Y von L eine kleinste obere und eine großteuntere Schranke hat.
Dies gilt auch fur Y = ∅ und Y = L. Man definiert:
⊥ =d
L (bottom, kleinstes Element im Verband)
> =⊔
L (top, großtes Element im Verband)
Barbara Konig Modellierung, Analyse, Verifikation 32
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Eigenschaften von Ordnungen, Ketten
Eine Ordnung v heißt total, wenn fur zwei Element l1, l2 ∈ Limmer l1 v l2 oder l2 v l1 gilt.
Y ⊆ L heißt Kette, wenn v eingeschrankt auf Y ×Y total ist.
Aufsteigende Kette: endliche oder unendliche Folgel0, l1, l2, l3, . . . mit li v li+1 fur alle i ∈ N0.Man schreibt auch (ln)n∈N0
.
v erfullt die Ascending Chain Condition, wenn es fur jedeunendliche aufsteigende Kette (ln)n einen Index m gibt mitlj = lj+1 fur j ≥ m.
Barbara Konig Modellierung, Analyse, Verifikation 33
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Eigenschaften von Funktionen
Gegeben: geordnete Mengen (L1,v1), (L2,v2)
Eine Funktion f : L1 → L2 heißt
monoton, falls fur alle l1, l2 ∈ L1 gilt: aus l1 v1 l2 folgt stetsf (l1) v2 f (l2).
additiv, falls fur l ,m ∈ L1 stets f (l tm) = f (l) t f (m) gilt.
multiplikativ, falls fur l ,m ∈ L1 stets f (l um) = f (l) u f (m)gilt.
In den letzten beiden Fallen muss man voraussetzen, dass (L1,v1)und (L2,v2) Verbande sind, damit die Definition Sinn macht.
Barbara Konig Modellierung, Analyse, Verifikation 34
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Fixpunkte
Gegeben: f : L→ L, wobei (L,v) ein vollstandiger Verband ist.
Menge aller Fixpunkte: Fix(f ) = {l ∈ L | f (l) = l}Menge aller Prafixpunkte: Pre(f ) = {l ∈ L | f (l) v l}Menge aller Postfixpunkte: Post(f ) = {l ∈ L | f (l) w l}
Außerdem definieren wir:
lfp(f ) =d
Fix(f )
gfp(f ) =⊔
Fix(f )
Achtung: lfp/gfp soll zwar fur least fixed-point/greatest fixed-pointstehen, aber es ist noch nicht klar, ob diese Elemente tatsachlichFixpunkte sind.
Barbara Konig Modellierung, Analyse, Verifikation 35
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Satz von Knaster-Tarski
Sei (L,v) ein vollstandiger Verband und f : L→ L eine monotoneFunktion. Dann gilt:
lfp(f ) =l
Pre(f ) ∈ Fix(f )
gfp(f ) =⊔
Post(f ) ∈ Fix(f ).
Folgerung: Eine monotone Funktion f auf einem vollstandigenVerband hat einen großten und einen kleinsten Fixpunkt (diemoglicherweise ubereinstimmen).
Frage: Wie konnen diese Fixpunkte bestimmt werden?
Barbara Konig Modellierung, Analyse, Verifikation 36
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Satz von Kleene
Sei (L,v) ein vollstandiger Verband, f : L→ L eine monotoneFunktion.Falls f stetig ist, das heißt fur jede aufsteigende Kette (ln)n gilt:
f (∞⊔n=0
ln) =∞⊔n=0
f (ln),
dann folgt lfp(f ) =∞⊔n=0
f n(⊥).
Verband erfullt die Ascending Chain Condition Verfahren zurBestimmung von Fixpunkten:
Berechne f (⊥), f (f (⊥)), f 3(⊥), . . . bis die Folge stationarwird, d.h., f i (⊥) = f i+1(⊥). Man erhalt dadurch denkleinsten Fixpunkt.
Barbara Konig Modellierung, Analyse, Verifikation 37
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Wiederholung: Fixpunkttheorie
Sei (L,v) ein vollstandiger Verband und f : L→ L eine monotoneFunktion. Dann gilt:
Großter und kleinster Fixpunkt:Die Funktion f besitzt einen kleinsten Fixpunkt lfp(f ) undeinen großten Fixpunkt gfp(f ).
Fixpunktiteration:Falls f stetig ist, d.h., fur jede aufsteigende Kette (ln)n gilt:f (⊔∞
n=0 ln) =⊔∞
n=0 f (ln), so folgt
lfp(f ) =∞⊔n=0
f n(⊥).
Analoges gilt fur den großten Fixpunkt.
Barbara Konig Modellierung, Analyse, Verifikation 38
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Datenflussanalyse: Gleichungssystem
A◦(1) = ∅A◦(2) = A•(1)
A◦(3) = A•(2)
∩ A•(5)
A◦(4) = A•(3)
A◦(5) = A•(4)
A◦(6) = A•(3)
A•(1) = A◦(1) ∪ {a + b}A•(2) = A◦(2) ∪ {a ∗ b}A•(3) = A◦(3) ∪ {a + b}A•(4) = A◦(4)
\{a + b, a ∗ b, a + 1}A•(5) = A◦(5) ∪ {a + b}A•(6) = A◦(6)
F (N1, . . . ,N6,X1, . . . ,X6) = (∅,X1,X2 ∩ X5,X3,X4,X3,
N1 ∪ {a + b},N2 ∪ {a ∗ b},N3 ∪ {a + b},N4\{a + b, a ∗ b, a + 1},N5 ∪ {a + b},N6)
Barbara Konig Modellierung, Analyse, Verifikation 39
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Fixpunktiteration (I)
F 0(AExp∗, . . . ) = (AExp∗, . . . ,AExp∗)
F 1(AExp∗, . . . ) = (∅,AExp∗,AExp∗,AExp∗,AExp∗,AExp∗,
AExp∗,AExp∗,AExp∗, ∅,AExp∗,AExp∗)
F 2(AExp∗, . . . ) = (∅,AExp∗,AExp∗,AExp∗, ∅,AExp∗,
{a + b},AExp∗,AExp∗, ∅,AExp∗,AExp∗)
F 3(AExp∗, . . . ) = (∅, {a + b},AExp∗,AExp∗, ∅,AExp∗,
{a + b},AExp∗,AExp∗, ∅, {a + b},AExp∗)
F 4(AExp∗, . . . ) = (∅, {a + b}, {a + b},AExp∗, ∅,AExp∗,
{a + b}, {a + b, a ∗ b},AExp∗, ∅, {a + b},AExp∗)
F 5(AExp∗, . . . ) = (∅, {a + b}, {a + b},AExp∗, ∅,AExp∗,
{a + b}, {a + b, a ∗ b}, {a + b}, ∅, {a + b},AExp∗)
Barbara Konig Modellierung, Analyse, Verifikation 40
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Fixpunktiteration (II)
F 5(AExp∗, . . . ) = (∅, {a + b}, {a + b},AExp∗, ∅,AExp∗,
{a + b}, {a + b, a ∗ b}, {a + b}, ∅, {a + b},AExp∗)
F 6(AExp∗, . . . ) = (∅, {a + b}, {a + b}, {a + b}, ∅, {a + b},{a + b}, {a + b, a ∗ b}, {a + b}, ∅, {a + b},AExp∗)
F 7(AExp∗, . . . ) = (∅, {a + b}, {a + b}, {a + b}, ∅, {a + b},{a + b}, {a + b, a ∗ b}, {a + b}, ∅, {a + b}, {a + b})
F 8(AExp∗, . . . ) = (∅, {a + b}, {a + b}, {a + b}, ∅, {a + b},{a + b}, {a + b, a ∗ b}, {a + b}, ∅, {a + b}, {a + b})
Barbara Konig Modellierung, Analyse, Verifikation 41
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Erwunschtes Analyseergebnis
F 8(AExp∗, . . . ) = (∅, {a + b}, {a + b}, {a + b}, ∅, {a + b},{a + b}, {a + b, a ∗ b}, {a + b}, ∅, {a + b}, {a + b})
` AE◦(`) AE•(`)
1 ∅ {a+b}2 {a+b} {a+b, a*b}3 {a+b} {a+b}4 {a+b} ∅5 ∅ {a+b}6 {a+b} {a+b}
[x:=a+b]1 [y:=a*b]2
[a:=a+1]4
yes [y>a+b]3no
[z:=x]6[x:=a+b]5
Barbara Konig Modellierung, Analyse, Verifikation 42
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Analyse lebendiger Variablen
Eine Variable heißt lebendig am Ausgang eines Blocks, wenn esmoglicherweise einen Pfad von diesem Block zu einem anderenBlock gibt, der diese Variable in einer Bedingung oder auf derrechten Seite einer Zuweisung benutzt, ohne dass die Variablevorher neu definiert wird.
Beispielprogramm: [x:=2]1;[y:=4]2;[x:=1]3;if [y>x]4
then [z:=2*x]5
else [z:=y*y]6
fi;
[x:=z]7
Barbara Konig Modellierung, Analyse, Verifikation 43
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Analyse lebendiger Variablen
Idee: Ruckwartsanalyse mit Vereinigung
Verband: (P(Var∗),⊆)
kill- und gen-Funktionen:
kill(`) =
{{x} falls block(`) = (x:=a)∅ sonst
gen(`) =
Var(a) falls block(`) = (x:=a)Var(b) falls block(`) = b∅ sonst
Barbara Konig Modellierung, Analyse, Verifikation 44
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Parameter bei der Datenflussanalyse (I)
Vorwartsanalyse Ruckwartsanalyse
Schnitt Verfugbare Ausdrucke ?
Vereinigung ? lebendige Variable
Auf jeden Fall in der Vergangenheit . . . Schnitt + Vorwartsanalyse
Auf jeden Fall in der Zukunft . . . Schnitt + Ruckwartsanalyse
Moglicherweise in der Vergangenheit . . . Vereinigung + Vorwartsanalyse
Moglicherweise in der Zukunft . . . Vereinigung + Ruckwartsanalyse
Barbara Konig Modellierung, Analyse, Verifikation 45
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Parameter bei der Datenflussanalyse (II)
Weitere Parameter:
Obermenge aller Analyseergebnisse (Vollstandiger Verband)
Initialer Analysewert
kill-/gen-Funktionen (allgemein: Transferfunktionen)
Flussrelation mit initialen bzw. finalen Labels
Barbara Konig Modellierung, Analyse, Verifikation 46
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Monotone Frameworks
Monotoner Framework (L,F)
(L,v) ist ein vollstandiger Verband
F ist eine Menge von monotonen Funktionen von L nach LF enthalt die Identitat und ist unter Funktionskompositionabgeschlossen.
Barbara Konig Modellierung, Analyse, Verifikation 47
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Instanz eines monotonen Frameworks
Instanz eines monotonen Frameworks (L,F): (L,F ,Lab,F ,E , ι, f·)
(L,v) ist ein vollstandiger Verband
F ist eine Menge von monotonen Funktionen(+ zusatzliche Eigenschaften)
Lab ist eine endliche Menge von Labels
F ⊆ Lab× Lab ist die Flussrelation
E ⊆ Lab ist eine Menge von sogenannten extremalen Labels
ι ∈ L ist der Wert, der jedem extremalen Label zugeordnetwird
f· bildet jedes Label ` ∈ Lab auf eine Funktion f` ∈ F ab.
Barbara Konig Modellierung, Analyse, Verifikation 48
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Gleichungssystem
Gleichungssystem zur Datenflussanalyse:
(2.1) A◦(`) =⊔{A•(`′) | (`′, `) ∈ F} t ι`E
wobei ι`E =
{ι falls ` ∈ E⊥ sonst
(2.2) A•(`) = f`(A◦(`))
Barbara Konig Modellierung, Analyse, Verifikation 49
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Reichweite von Zuweisungen
Fur jeden Block des Programms und fur jede Variable sollen alleStellen bestimmt werden, an denen dieser Variable zuletzt ein Wertzugewiesen worden sein konnte.
(x, `): x konnte zuletzt in Block ` ein Wert zugewiesen worden sein(x, ?): x wurde evtl. noch gar kein Wert zugewiesen.
Beispielprogramm:
[y := x]1;[z := 1]2;while [y>1]3 do
[z := z*y]4;[y := y-1]5
od;
[y:=0]6
Barbara Konig Modellierung, Analyse, Verifikation 50
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Reichweite von Zuweisungen
Idee: Vorwartsanalyse mit Vereinigung
Verband: (P(Var∗ × (Lab∗ ∪ {?})),⊆)
Initialer Analysewert: {(x, ?) | x ∈ Var∗}Transferfunktion:
kill(`) =
{{(x, ?)} ∪ {(x, `′) | `′ ∈ Lab∗} falls block(`) = (x:=a)∅ sonst
gen(`) =
{{(x, `)} falls block(`) = (x:=a)∅ sonst
Barbara Konig Modellierung, Analyse, Verifikation 51
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Benotigte Ausdrucke
Zu einem Block ` sollen arithmetische Ausdrucke bestimmtwerden, die auf jedem von ` ausgehenden Pfad benutzt werden,ohne vorher verandert zu werden.
Beispielprogramm:
if [x=1]1
then [y := a+b*c]2
else [y := b*c]3
fi
Barbara Konig Modellierung, Analyse, Verifikation 52
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Benotigte Ausdrucke
Idee: Ruckwartsanalyse mit Schnitt
Verband: (P(AExp∗),⊇)
Initialer Analysewert: ∅Transferfunktion:
kill(`) =
{{a′ ∈ AExp∗ | x ∈ Var(a′)} falls block(`) = (x:=a)∅ sonst
gen(`) =
AExp(a) falls block(`) = (x:=a)AExp(b) falls block(`) = b∅ sonst
Barbara Konig Modellierung, Analyse, Verifikation 53
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Monotone Frameworks (Zusammenfassung)
Verfugbare Reichweite von Benotigte Lebendige
Ausdrucke Zuweisungen Ausdrucke Variable
L P(AExp∗) P(Var∗ × (Lab∗ ∪ {?})) P(AExp∗) P(Var∗)
v ⊇ ⊆ ⊇ ⊆t ∩ ∪ ∩ ∪⊥ AExp∗ ∅ AExp∗ ∅ι ∅ {(x, ?) | x ∈ Var(S)} ∅ variabel
E {init(S)} {init(S)} final(S) final(S)
F flow(S) flow(S) flowR(S) flowR(S)
F {f : L→ L | f monoton}f` f`(A) = A\kill(`) ∪ gen(`)
Barbara Konig Modellierung, Analyse, Verifikation 54
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (I)
Eingabe: Instanz eines monotonen Frameworks
Ausgabe: MFP◦, MFP•
Schritt 1 (Initialisierung)W := F ;for all ` ∈ Lab do
if ` ∈ Ethen A[`] := ιelse A[`] := ⊥
fiod
Barbara Konig Modellierung, Analyse, Verifikation 55
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (II)
Schritt 2 (Iteration)while W 6= ∅ do
choose (`′, `) from W;W := W\{(`′, `)};if f`′(A[`′]) 6v A[`] then
A[`] := A[`] t f`′(A[`′]);for all `′′ with (`, `′′) ∈ F do
W := W ∪{(`, `′′)}od
fiod
Barbara Konig Modellierung, Analyse, Verifikation 56
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (III)
Schritt 3 (Ausgabe)for all ` ∈ Lab do
MFP◦(`) := A[`];MFP•(`) := f`(A[`])
od
Barbara Konig Modellierung, Analyse, Verifikation 57
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
Beispielprogramm:
[y := x]1;[z := 1]2;while [y>1]3 do
[z := z*y]4;[y := y-1]5
od;
[y:=0]6
Analyse der Reichweite von Zuweisungen
Barbara Konig Modellierung, Analyse, Verifikation 58
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[z:=z*y]4
[y>1]3
[y:=0]6
[y:=y-1]5
∅
∅
∅
∅
∅
{(x, ?), (y, ?), (z, ?)}
Worklist:W = (1, 2)(2, 3)(3, 6)(3, 4)(4, 5)(5, 3)
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[z:=z*y]4
[y:=y-1]5
[y:=0]6
[y>1]3
∅
∅
∅
∅
∅
{(x, ?), (y, ?), (z, ?)}
Worklist:W = (1, 2)(2, 3)(3, 6)(3, 4)(4, 5)(5, 3)
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[z:=z*y]4
[y:=y-1]5
[y:=0]6
[y>1]3
∅
∅
∅
∅
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
Worklist:W = (2, 3)(3, 6)(3, 4)(4, 5)(5, 3)
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[z:=z*y]4
[y:=y-1]5
[y:=0]6
[y>1]3
∅
∅
∅
∅
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
Worklist:W = (2, 3)(3, 6)(3, 4)(4, 5)(5, 3)
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[z:=z*y]4
[y:=y-1]5
[y:=0]6
[y>1]3
∅
∅
∅
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (z, 2)}Worklist:W = (3, 6)(3, 4)(4, 5)(5, 3)
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[z:=z*y]4
[y:=y-1]5
[y>1]3
[y:=0]6
∅
∅
∅
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (z, 2)}Worklist:W = (3, 6)(3, 4)(4, 5)(5, 3)
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[y>1]3
[z:=z*y]4
∅
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (z, 2)}
∅
{(x, ?), (y, 1), (z, 2)}
Worklist:W = (3, 4)(4, 5)(5, 3)
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[y>1]3
[z:=z*y]4
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (z, 2)}
∅
{(x, ?), (y, 1), (z, 2)}
∅
Worklist:W = (3, 4)(4, 5)(5, 3)
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[y>1]3
[z:=z*y]4
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (z, 2)}
{(x, ?), (y, 1), (z, 2)}
∅
{(x, ?), (y, 1), (z, 2)}
Worklist:W = (4, 5)(5, 3)
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[y>1]3
[z:=z*y]4
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (z, 2)}
{(x, ?), (y, 1), (z, 2)}
{(x, ?), (y, 1), (z, 2)}
∅
Worklist:W = (4, 5)(5, 3)
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[y>1]3
[z:=z*y]4
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (z, 2)}
{(x, ?), (y, 1), (z, 2)}
{(x, ?), (y, 1), (z, 2)}
{(x, ?), (y, 1), (z, 4)}
Worklist:W = (5, 3)
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[y>1]3
[z:=z*y]4
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (z, 2)}
{(x, ?), (y, 1), (z, 2)}
{(x, ?), (y, 1), (z, 4)}
{(x, ?), (y, 1), (z, 2)}
Worklist:W = (5, 3)
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[z:=z*y]4
[y>1]3
neu!
neu!
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (z, 2)}
{(x, ?), (y, 1), (z, 4)}
{(x, ?), (y, 1), (z, 2)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}Worklist:W = (3, 6)(3, 4)
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[y>1]3
[z:=z*y]4
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (z, 2)}
{(x, ?), (y, 1), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (z, 2)}
Worklist:W = (3, 6)(3, 4)
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[y>1]3
[z:=z*y]4
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (z, 2)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
Worklist:W = (3, 4)
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[y>1]3
[z:=z*y]4
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (z, 2)}
Worklist:W = (3, 4)
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[y>1]3
neu!
[z:=z*y]4
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
Worklist:W = (4, 5)
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[y>1]3
[z:=z*y]4
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (z, 4)}
Worklist:W = (4, 5)
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
neu!
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[y>1]3
[z:=z*y]4
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 4)}
Worklist:W = (5, 3)
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[y>1]3
[z:=z*y]4
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
Worklist:W = (5, 3)
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Worklist-Algorithmus (Beispiel)
[y:=x]1
[z:=1]2
[y:=y-1]5
[y:=0]6
[y>1]3
[z:=z*y]4
{(x, ?), (y, ?), (z, ?)}
{(x, ?), (y, 1), (z, ?)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 4)}
{(x, ?), (y, 1), (y, 5), (z, 2), (z, 4)}
Worklist:W = ∅
Barbara Konig Modellierung, Analyse, Verifikation 59
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Gleichungssystem
Gleichungssystem zur Datenflussanalyse:
(3.1) A◦(`) =⊔{A•(`′) | (`′, `) ∈ F} t ι`E
wobei ι`E =
{ι falls ` ∈ E⊥ sonst
(3.2) A•(`) = f`(A◦(`))
Kombiniert:
A◦(`) =⊔{f`′(A◦(`
′)) | (`′, `) ∈ F} t ι`E
Barbara Konig Modellierung, Analyse, Verifikation 60
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Werkzeuge, die Datenflussanalyse einsetzen
Eine unvollstandige Auswahl:
Compiler (C-Compiler, etc.)
Java Virtual Machine (Java Bytecode Verifier)
Programmanalyse-Generator mit WWW-Interface:PAG/WWW
Kommerzielle Anbieter von Programmanalyse-Software:
AbsInt – http://www.absint.com
PolySpace –http://www.mathworks.com/products/polyspace/
Barbara Konig Modellierung, Analyse, Verifikation 61
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Demo: Optimierung im GNU C Compiler
Verwendung des Stacks in ubersetzten Programmen beimMethodenaufruf:
Parameter k
...
Parameter 1
Lokale
Variable
Administra-
tiver Teil
Stack
Arbeits-
StackPointer
Pointer
%esp
%ebp
Administrativer Teil:Gesicherter Base-Pointer,Rucksprungadresse, etc.
Base
RichtungdesStack-Wachstums
Kleinere Adressen
Großere Adressen
In modernenRechnerarchitekturenwerden die Parameteraus Effizienzgrundeninzwischen vorrangig inRegistern ubergeben.
Barbara Konig Modellierung, Analyse, Verifikation 62
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Beispiel & FixpunkttheorieMonotone FrameworksWorklist-Algorithmus
Ausblick
Weitere Fragestellungen bei Datenflussanalyse:
Interprozedurale Analyse (Prozeduraufrufe,Parameterubergabe, Laufzeitstack)bisher: Intraprozedurale Analyse
Analyse von Pointer-Strukturen bzw. Objektstrukturen
Points-to-AnalyseAlias AnalysisShape Analysis
Barbara Konig Modellierung, Analyse, Verifikation 63
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Java BytecodeBytecode Verifier
Java Bytecode
Zwischensprache zwischen Hochsprache (Java) undMaschinensprache
Vorteil: Maschinenunabhangigkeit, Geschwindigkeitsvorteilgegenuber Interpretation
Ausfuhrung durch Java Virtual Machine (JVM)
Objekt-Orientierung ist im Bytecode sichtbar: Klassen,Methodenaufrufe, etc.
Problem: SicherheitsluckenZugriff auf beliebige Stellen des Hauptspeichers, z.B. durchVerwendung von Integers als Objekt-Referenzen
Barbara Konig Modellierung, Analyse, Verifikation 64
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Java BytecodeBytecode Verifier
Klassenhierarchie und Typen
Gegeben: Klassenhierarchie
Class
Class A
Class B Class C
Jede Klasse besitzt Felder undMethoden
Klasse B erbt von A ⇒ B hatmindestens die Felder undMethoden von A
Typen:
Integer ganze ZahlNullT Null-PointerClass cname Klasse cnameClass Super-Klasse
Menge aller Typen: Ty
Es gilt:isref (Integer) = falseisref (NullT) = trueisref (Class cname) = trueisref (Class) = true
Barbara Konig Modellierung, Analyse, Verifikation 65
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Java BytecodeBytecode Verifier
Register und Stack
Register: Satz von m lokalen Registern, die Elemente vom TypInteger, NullT und Class cname enthalten konnen
Stack: Stack mit Lange ≤ max , mit Push- undPop-Operationen
Objekt der Klasse A
Null-Pointer
17
nicht initialisiert
...
NullT Integer
Register Stack
Typ: Class A
Integer
NullT
Typ:
...
8
Barbara Konig Modellierung, Analyse, Verifikation 66
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Java BytecodeBytecode Verifier
Befehlssatz (I)
Load n: Inhalt des n-ten Registers auf den Stack (Push)
Store n: Oberstes Stack-Element in n-tes Register (Pop)
AConst Null: Null-Pointer auf Stack legen (Push)
IConst i : Integer i auf Stack legen (Push)
IAdd: Die zwei obersten Stack-Werte (Typ Integer) addierenund das Ergebnis auf Stack legen
Getfield fname ty cname: Referenz auf Objekt der Klassecname vom Stack nehmenInhalt des Feld fname vom Typ ty dieses Objekts holen undauf Stack legen.
Barbara Konig Modellierung, Analyse, Verifikation 67
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Java BytecodeBytecode Verifier
Befehlssatz (II)
Putfield fname ty cname: Erstes Stack-Element (e) undzweites Stack-Element (Referenz auf ein Objekt der Klassecname) entfernenFeld fname vom Typ ty dieses Objekts den Wert e zuweisen
New cname: Neues Objekt der Klasse cname erzeugen undauf Stack legen (Push).
Invoke cname mname ty 1 ty 2: Erstes Stack-Element(Parameter vom Typ ty 1) und zweites Stack-Element(Referenz auf ein Objekt der Klasse cname) entfernenMethode mname dieses Objekts mit dem Parameter aufrufenund Ruckgabewert (vom Typ ty 2) auf Stack legen
Barbara Konig Modellierung, Analyse, Verifikation 68
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Java BytecodeBytecode Verifier
Befehlssatz (III)
CmpEq q: Die obersten beiden Werte vom Stack nehmen undmiteinander vergleichen.Bei Gleichheit in Zeile q springen
Return: An die Aufrufstelle der Methode zuruckkehrenDer zuoberst auf dem Stack liegende Wert ist Ruckgabewert(vom Typ ty r )
Eine Methode des Bytecode besteht aus einer Liste vonKommandos der Form ` : cmd , wobei ` (das Label) von 1 bis klauft.
Barbara Konig Modellierung, Analyse, Verifikation 69
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Java BytecodeBytecode Verifier
Bosartiger Bytecode
1: IConst 10002: IConst 13: Putfield f Integer A
Die Zahl 1000 wird als Referenz auf eine Objekt der Klasse Aangesehen und dadurch an eine Speicherstelle 1000 + x der Wert 1geschrieben.
Andere Sicherheitslucken: Stack-Uberlauf, Addition vonReferenzen, etc.
Barbara Konig Modellierung, Analyse, Verifikation 70
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Java BytecodeBytecode Verifier
Bytecode Verifier
Idee zur Erkennung von bosartigem Bytecode:
Zuordnung von Typen zu Register- und Stack-Inhalten. DieMenge aller Typen bildet einen Verband.
Durch Datenflussanalyse wird fur jeden Block (jedeProgrammzeile) ein Typ bestimmt, der den moglichenRegister- und Stack-Inhalt an dieser Stelle beschreibt.
Mit Hilfe des Typs an dieser Stelle kann man ablesen, ob einbestimmter Befehl zulassig oder unzulassig ist.
Barbara Konig Modellierung, Analyse, Verifikation 71
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Java BytecodeBytecode Verifier
Verband (I)
T = {None,Err} ∪ (Ty∗ × ({Undef } ∪ Ty)m)
Partielle Ordnung (Definition in mehreren Schritten)
A vc B ⇐⇒ A ist als Klasse von B abgeleitet
ty 1, ty 2 ∈ Ty = {Integer,NullT,Class,Class A,Class B, . . .}
ty 1 vt ty 2 ⇐⇒ ty 1 = ty 2 ∨(ty 1 = NullT ∧ isref (ty 2)) ∨(isref (ty 1) ∧ ty 2 = Class) ∨(ty 1 = Class A ∧ ty 2 = Class B ∧ A vc B)
Barbara Konig Modellierung, Analyse, Verifikation 72
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Java BytecodeBytecode Verifier
Verband (II)
Partielle Ordnung aufT = {None,Err} ∪ (Ty∗ × ({Undef } ∪ Ty)m)
None vT t fur alle t ∈ Tt vT Err fur alle t ∈ T(st1, reg 1) vT (st2, reg 2) ⇐⇒
st i = [s i1, . . . , sipi
] ∧ reg i = [r i1, . . . , rim] fur i = 1, 2 ∧
p1 = p2 ∧∀ 1 ≤ j ≤ p1 : (s1
j vt s2j ) ∧
∀ 1 ≤ j ≤ m : (r1j vt r
2j ∨ r2
j = Undef )
Barbara Konig Modellierung, Analyse, Verifikation 73
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Java BytecodeBytecode Verifier
Komponenten des monotonen Frameworks
Labels: Zeilennummern des Java Bytecodes
Flussrelation F : Fur jede Programmzeile der Form` : CmpEq q enthalt die Flussrelation die Paare (`, q) und(`, `+ 1). Fur jede andere Zeile (außer beiReturn-Anweisungen) wird das Paar (`, `+ 1) hinzugefugt.
Extremales Label: 1 (die Nummer der ersten Programmzeile)
Initialer Analysewert : ι = ([], [Class C , p,Undef , . . . ,Undef ]︸ ︷︷ ︸Lange m
)
wobei C die Klasse des Objekts ist, dessen Methodeaufgerufen wird und p der Typ des Eingabeparameters ist.
Es fehlen noch: die Transferfunktionen
Barbara Konig Modellierung, Analyse, Verifikation 74
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Java BytecodeBytecode Verifier
Typregeln fur den Bytecode Verifier (I)
|st| < max , reg !n 6= Undef
(st, reg) ` Load n
|st| > 0
(st, reg) ` Store n
|st| < max
(st, reg) ` AConst Null
|st| < max
(st, reg) ` IConst i
st = [Integer, Integer] ◦ st ′
(st, reg) ` IAdd
st = [ty 0] ◦ st ′, ty 0 vt Class cname
(st, reg) ` Getfield fname ty cname
st = [ty v , ty 0] ◦ st ′, ty v vt ty , ty 0 vt Class cname
(st, reg) ` Putfield fname ty cname
Barbara Konig Modellierung, Analyse, Verifikation 75
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Java BytecodeBytecode Verifier
Typregeln fur den Bytecode Verifier (II)
|st| < max
(st, reg) ` New cname
st = [tya, ty 0] ◦ st ′, ty 0 vt Class cname, tya vt ty 1
(st, reg) ` Invoke cname mname ty 1 ty 2
st = [ty 1, ty 2] ◦ st ′, ty 1 = ty 2 = Integer ∨ (isref(ty 1) ∧ isref(ty 2))
(st, reg) ` CmpEq q
st = [ty ] ◦ st ′, ty vt ty r
(st, reg) ` Return
Barbara Konig Modellierung, Analyse, Verifikation 76
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Java BytecodeBytecode Verifier
Transferfunktionen (I)
f`(t) =
None falls t = Nonetransfer(cmd , t) falls t = (st, reg), (st, reg) ` cmd
und block(`) = cmdErr sonst
transfer(Load n, (st, reg)) = ([reg !n] ◦ st, reg)
transfer(Store n, (st, reg)) = (rest(st), reg [n 7→ first(st)])
transfer(AConst Null, (st, reg)) = ([NullT] ◦ st, reg)
transfer(IConst i , (st, reg)) = ([Integer] ◦ st, reg)
transfer(IAdd, (st, reg)) = ([Integer] ◦ rest2(st), reg)
Barbara Konig Modellierung, Analyse, Verifikation 77
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Java BytecodeBytecode Verifier
Transferfunktionen (II)
transfer(Getfield fname ty
cname, (st, reg)) = ([ty ] ◦ rest(st), reg)
transfer(Putfield fname ty
cname, (st, reg)) = (rest2(st), reg)
transfer(New cname, (st, reg)) = ([Class cname] ◦ st, reg)
transfer(Invoke cname mname
ty 1 ty 2, (st, reg)) = ([ty 2] ◦ rest2(st), reg)
transfer(CmpEq q, (st, reg)) = (rest2(st), reg)
transfer(Return, (st, reg)) = (st, reg)
Barbara Konig Modellierung, Analyse, Verifikation 78
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Java BytecodeBytecode Verifier
Beispiel fur die Analyse des Java Bytecodes
Situation: Klassenhierarchie wie oben (Klassen B, C werden vonKlasse A abgeleitet)
Alle Klassen haben eine Methode m : Integer→ Class C
Klasse C hat ein Feld f : Integer
Eine (unbenannte) Methode der Klasse A vom TypClass B → Class C wird aufgerufen.
Barbara Konig Modellierung, Analyse, Verifikation 79
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Java BytecodeBytecode Verifier
Beispiel fur die Analyse des Java Bytecodes
Aufgabe: Durchfuhren der Analyse des Java Bytecode Verifiers auffolgendem Code der aufzurufenden Methode:
1: Load 12: IConst 13: Invoke A m Integer C4: Store 05: Load 06: Getfield f Integer C7: IConst 08: CmpEq 19: Load 0
10: Return(Nummerierung der Register beginnt bei 0.)
Barbara Konig Modellierung, Analyse, Verifikation 80
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Java BytecodeBytecode Verifier
Fehlermeldungen des Java Bytecode Verifiers
Unvollstandige Liste von Fehlermeldungen:
Inconsistent stack height
Accessing value from uninitialized register
Stack size too large
Unable to pop operand off an empty stack
Expecting to find integer on stack
Expecting to find object/array on stack
Incompatible type for getting or setting field
Wrong return type in function
Mismatched stack types
Barbara Konig Modellierung, Analyse, Verifikation 81
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Java BytecodeBytecode Verifier
Korrektheit des Java Bytecode Verifiers
Man kann zeigen:
Falls fur das Analyseergebnis des Java Bytecode Verifiers gilt:A◦(`) 6= Err und A•(`) 6= Err fur alle vorkommenden Labels `, sohat das analysierte Programm keine Laufzeitfehler.
(Siehe auch die Liste der Fehlermeldungen.)
Barbara Konig Modellierung, Analyse, Verifikation 82
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Java BytecodeBytecode Verifier
Stack Map Frames
Seit Java 7 (Bytecode-Version 50): Sprungstellen mussen mit denkorrekten Stack- und Registertypen annotiert werden. DieseAnnotationen heißen Stack Map Frames.
Dadurch benotigt der Worklist-Algorithmus nur noch einenDurchlauf.
Vorteil: effizientere Verifikation
Nachteil: es ist sehr komplex eigenen Bytecode zu schreiben bzw.zu generieren
Barbara Konig Modellierung, Analyse, Verifikation 83
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Abstrakte Interpretation (I)
Grundidee: Ausfuhrung eines Programms auf abstraktenWertenBeispiel: even/odd statt ganzer Zahlen
Partielle Ordnung auf den abstrakten Werten:∅, {even}, {odd}, {even, odd} mit Inklusion
(je großer, desto ungenauer)
Sprache: While-Programme
Ziel: Programm soll auf einer endlichen Menge von abstraktenWerten (Uberdeckung des gesamten Eingabebereichs)ausgefuhrt werden Uberprufung der Korrektheit
Barbara Konig Modellierung, Analyse, Verifikation 84
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Abstrakte Interpretation (II)
Vorteile:
Bei Verzweigungen (If-Then-Else, While) muss (je nachabstrakter Wertebelegung) u.U. nur ein Zweig verfolgt werden genaueres AnalyseergebnisDurch Auswahl der Abstraktionsfunktion hat man Einfluss aufdie Gute des Analyseergebnisses und auf den AufwandZahlreiche Varianten fur verschiedene Arten von Programmen(z.B. fur nebenlaufige Systeme)Korrektheit ergibt sich automatisch, falls abstrakte Operatorengemaß der Theorie bestimmt werden
Nachteile:
i.a. hoherer Aufwand als bei DatenflussanalyseAutomatische Bestimmung der abstrakten Operatorenschwierig
Barbara Konig Modellierung, Analyse, Verifikation 85
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Inhalt (Abstrakte Interpretation)
Grundlagen (Galois-Verbindungen)
Abstrakte Semantik von While-Programmen
Automatische Herleitung einer abstrakten Semantik
Anwendung: Verifikation von 16-Bit-Multiplikation
Pradikatabstraktion
Abstraktionsverfeinerung basierend auf Gegenbeispielen
Barbara Konig Modellierung, Analyse, Verifikation 86
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Galois-Verbindung
Gegeben seien zwei Verbande (L,v) und (M,v). Ein Paar 〈α, γ〉von monotonen Funktionen
α : L→ M, γ : M → L
heißt Galois-Verbindung genau dann, wenn gilt:
∀ l ∈ L : l v γ(α(l)) ∀m ∈ M : α(γ(m)) v m
γ
α
l
γ
α
m
B B
AA
L = P(A) M = P(B)
Barbara Konig Modellierung, Analyse, Verifikation 87
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Eigenschaften von Galois-Verbindungen (I)
Sei 〈α, γ〉 eine Galois-Verbindung mit α : L→ M und γ : M → L,sowie l ∈ L und m ∈ M. Dann gilt:
α(l) v m ⇐⇒ l v γ(m).
Barbara Konig Modellierung, Analyse, Verifikation 88
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Eigenschaften von Galois-Verbindungen (II)
Sei 〈α, γ〉 eine Galois-Verbindung mit α : L→ M und γ : M → L.Dann gilt:
(i) Die Konkretisierung γ ist eindeutig durch α bestimmt und esgilt γ(m) =
⊔{l | α(l) v m}.
(ii) Die Abstraktion α ist eindeutig durch γ bestimmt und es giltα(l) =
d{m | l v γ(m)}.
Barbara Konig Modellierung, Analyse, Verifikation 89
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Eigenschaften von Galois-Verbindungen (III)
(iii) Es gilt α(⊔L′) =
⊔{α(l) | l ∈ L′} fur L′ ⊆ L. Man sagt auch
α ist vollstandig additiv.
(iv) Es gilt γ(dM ′) =
d{γ(m) | m ∈ M ′} fur M ′ ⊆ M. Man sagt
auch γ ist vollstandig multiplikativ.
(v) Außerdem gibt es zu jeder vollstandig additiven Funktionα : L→ M eine Funktion γ : M → L, so dass 〈α, γ〉 eineGalois-Verbindung ist. Des weiteren gibt es zu jedervollstandig multiplikativen Funktion γ : M → L eine Funktionα : L→ M, so dass 〈α, γ〉 eine Galois-Verbindung ist.
Barbara Konig Modellierung, Analyse, Verifikation 90
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Extraktionsfunktionen
Definition von Galois-Verbindungen mit Hilfe vonExtraktionsfunktionen:
Sei β : A1 → A2 eine Abbildung. Definition von α : P(A1)→ P(A2)und γ : P(A2)→ P(A1) in Abhangigkeit von β:
α(A′1) = β(A′1) = {β(a1) | a1 ∈ A′1} fur jedes A′1 ⊆ A1
γ(A′2) = β−1(A′2) = {a1 ∈ A1 | β(a1) ∈ A′2} fur jedes A′2 ⊆ A2
Beispiel: even/odd-Abstraktion mit Extraktionsfunktion
β : Z → {odd , even}
β(z) =
{even falls z ∈ {. . . ,−2, 0, 2, . . . }odd falls z ∈ {. . . ,−3,−1, 1, 3, . . . }
Barbara Konig Modellierung, Analyse, Verifikation 91
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Semantik von While-Programmen (I)
〈[x:=a]`, σ〉 → σ[x 7→ A(a, σ)] [ass]
〈[skip]`, σ〉 → σ [skip]
〈S1, σ〉 → 〈S ′1, σ′〉〈S1;S2, σ〉 → 〈S ′1;S2, σ
′〉 [seq1]
〈S1, σ〉 → σ′
〈S1;S2, σ〉 → 〈S2, σ′〉 [seq2]
Barbara Konig Modellierung, Analyse, Verifikation 92
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Semantik von While-Programmen (II)
〈if [b]` then S1 else S2 fi, σ〉 → 〈S1, σ〉
falls B(b, σ) = true [if1]
〈if [b]` then S1 else S2 fi, σ〉 → 〈S2, σ〉
falls B(b, σ) = false [if2]
〈while [b]` do S od, σ〉 → 〈S;while [b]` do S od, σ〉
falls B(b, σ) = true [wh1]
〈while [b]` do S od, σ〉 → σ
falls B(b, σ) = false [wh2]
Barbara Konig Modellierung, Analyse, Verifikation 93
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Definition: Abstrakte Semantik
Die abstrakte Semantik wird beschrieben durch eine Familienext#
S ,S ′ : Abs→ Abs von Funktionen fur die gilt:
α(nextS ,S ′(γ(abs))) v next#S ,S ′(abs)
fur abs ∈ Abs und alle While-Programme S , S ′ und S ′ =↓.
Wir schreiben auch
〈S , abs〉 =⇒ 〈S ′, abs ′〉, falls next#S,S ′(abs) = abs ′.
〈S , abs〉 =⇒ abs ′, falls next#S ,↓(abs) = abs ′.
Barbara Konig Modellierung, Analyse, Verifikation 94
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Hailstone-Programm
[skip]1;while [n6=1]2 do
if [even(n)]3
then [n:=n/2]4;[skip]5
else [n:=3*n+1]6;[skip]7
fi
od
Barbara Konig Modellierung, Analyse, Verifikation 95
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Abstrakte Interpretation von Hailstone
〈[skip]1;..., {[n 7→ odd ]}〉
��
{[n 7→ odd ]}
〈while [n 6=1]2 ..., {[n 7→ odd ]}〉
��
-5
〈while [n 6=1]2 ..., {[n 7→ even]}〉
��〈if [even(n)]3 ..., {[n 7→ odd ]}〉
��
〈if [even(n)]3 ..., {[n 7→ even]}〉
��〈[n:=3*n+1]6;..., {[n 7→ odd ]}〉
��
〈[n:=n/2]4;..., {[n 7→ even]}〉
��〈[skip]7;..., {[n 7→ even]}〉
+3
〈[skip]5;..., {[n 7→ even], [n 7→ odd ]}〉
��〈while [n6=1]2 ..., {[n 7→ even], [n 7→ odd ]}〉
��
ks
〈if [even(n)]3 ..., {[n 7→ even], [n 7→ odd ]}〉
+3+3
Barbara Konig Modellierung, Analyse, Verifikation 96
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Abstrakte Interpretation von While-Programmen
Extraktionsfunktion β : Z→ A
Galoisverbindung (entsteht durch Liften der Extraktionsfunktion):
α : P(State)→ P(Var→ A)
γ : P(Var→ A)→ P(State)
Auswertungsfunktionen auf abstrakten Werten:
Fur arithmetische Ausdrucke:Aabstr : AExp× (Var→ A)→ P(A)
Fur boolesche Ausdrucke:Babstr : BExp× (Var→ A)→ {0, 1, 1/2}
Barbara Konig Modellierung, Analyse, Verifikation 97
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Approximation von Operationen
Sichere Approximation von (Basis-)Operationen:Zu jedem Operator op : Zn → Z definieren wirop# : P(A)n → P(A) mit:
op#(A1, . . . ,An) = {β(op(z1, . . . , zn)) | zi ∈ β−1(Ai )}
falls Ai ⊆ A.
Barbara Konig Modellierung, Analyse, Verifikation 98
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Auswertung von arithmetischen Ausdrucken
Sei ρ ∈ (Var→ A).
Aabstr (x, ρ) = {ρ(x)} fur x ∈ Var
Aabstr (z , ρ) = {β(z)} fur z ∈ ZAabstr (op(a1, . . . , an), ρ) = op#(Aabstr (a1, ρ), . . . ,Aabstr (an, ρ))
fur a1, . . . , an ∈ AExp
Barbara Konig Modellierung, Analyse, Verifikation 99
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Approximation von Pradikaten
Sichere Approximation von Pradikaten:Zu jedem Pradikat P : Zn → {true, false} definieren wirP# : P(A)n → {0, 1, 1/2} mit
P#(A1, . . . ,An) =
0 fur alle zi ∈ β−1(Ai ) gilt
P(z1, . . . , zn) = false1 fur alle zi ∈ β−1(Ai ) gilt
P(z1, . . . , zn) = true1/2 sonst
wobei A1 ⊆ A, . . . ,An ⊆ A, Ai 6= ∅.Falls eine der Mengen Ai leer ist, kann man P# beliebigfestlegen.
Barbara Konig Modellierung, Analyse, Verifikation 100
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Dreiwertige Logik
Drei Wahrheitswerte: 0, 1, 1/2
Wahrheitstafeln:
∧ 0 1 1/2
0 0 0 01 0 1 1/2
1/2 0 1/2 1/2
∨ 0 1 1/2
0 0 1 1/21 1 1 1
1/2 1/2 1 1/2
¬0 11 0
1/2 1/2
Barbara Konig Modellierung, Analyse, Verifikation 101
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Auswertung von booleschen Ausdrucken
Sei ρ ∈ (Var→ A), P ein Pradikat,a1, . . . , an ∈ AExp, b, b1, b2 ∈ BExp.
Babstr (P(a1, . . . , an), ρ) = P#(Aabstr (a1, ρ), . . . ,Aabstr (a1, ρ))
Babstr (¬b, ρ) = ¬Babstr (b, ρ)
Babstr (b1 ∧ b2, ρ) = Babstr (b1, ρ) ∧ Babstr (b2, ρ)
Babstr (b1 ∨ b2, ρ) = Babstr (b1, ρ) ∨ Babstr (b2, ρ)
Achtung: Auf der rechten Seite werden jeweils die Operatoren derdreiwertigen Logik verwendet.
Barbara Konig Modellierung, Analyse, Verifikation 102
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Satz (Sichere Approximation)
Es sei a ein arithmetischer Ausdruck und σ : Var→ Z.Dann gilt:
β(A(a, σ)) ∈ Aabstr (a, β ◦ σ)
Des weiteren sei b ein Boolescher Ausdruck.Dann gilt:
B(b, σ) ∈ val(Babstr (b, β ◦ σ)),
wobei
val(b) =
{false} falls b = 0{true} falls b = 1{true, false} falls b = 1/2
Barbara Konig Modellierung, Analyse, Verifikation 103
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Abstrakte While-Semantik (I)
〈[x:=a]`, abs〉 =⇒
{ρ[x 7→ w ] | ρ ∈ abs,w ∈ Aabstr (a, ρ)} [ass]
〈[skip]`, abs〉 =⇒ abs [skip]
〈S1, abs〉 =⇒ 〈S ′1, abs ′〉〈S1;S2, abs〉 =⇒ 〈S ′1;S2, abs ′〉 [seq1]
〈S1, abs〉 =⇒ abs ′
〈S1;S2, abs〉 =⇒ 〈S2, abs ′〉 [seq2]
Barbara Konig Modellierung, Analyse, Verifikation 104
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Abstrakte While-Semantik (II)
〈if [b]` then S1 else S2 fi, abs〉 =⇒
〈S1, abs\{ρ | Babstr (b, ρ) = 0}〉 [if1]
〈if [b]` then S1 else S2 fi, abs〉 =⇒
〈S2, abs\{ρ | Babstr (b, ρ) = 1}〉 [if2]
〈while [b]` do S od, abs〉 =⇒
〈S;while [b]` do S od, abs\{ρ | Babstr (b, ρ) = 0}〉 [wh1]
〈while [b]` do S od, abs〉 =⇒
abs\{ρ | Babstr (b, ρ) = 1} [wh2]
Barbara Konig Modellierung, Analyse, Verifikation 105
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Abstrakte next#-Funktionen
next#S,S ′(abs) =
{abs ′ falls 〈S , abs〉 =⇒ 〈S ′, abs ′〉∅ sonst
next#S ,↓(abs) =
{abs ′ falls 〈S , abs〉 =⇒ abs ′
∅ sonst
Barbara Konig Modellierung, Analyse, Verifikation 106
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
16-Bit-Multiplikation
[out := 0]1;[overflow := 0]2;while [(f1 6=0) ∧ (overflow=0)]3 do
if [lsb(f1)=1]4
then [(overflow,out) := (out:17) + f2]5
else [skip]6
fi;
[f1 := f1 >> 1]7;if [(f1 6=0) ∧ (overflow=0)]8
then [(overflow,f2) := (f2:17)<<1]9
else [skip]10
fi
od
Barbara Konig Modellierung, Analyse, Verifikation 107
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Abstraktionsverfeinerung
Motivation: Falls die Abstraktion zu grob ist, um die gewunschteEigenschaft zu zeigen, so muss sie verfeinert werden. EineMoglichkeit hierfur ist das sogenannte Counterexample-guidedabstraction refinement (Abstraktionsverfeinerung basierend aufGegenbeispielen)
Barbara Konig Modellierung, Analyse, Verifikation 108
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Abstraktionsverfeinerung
ja
nein
Ablauf ist echtAblauf ist unecht
der P verletzt
in der Abstraktion erfullt?groben initialen Abstraktion
Verfeinere die Abstraktion
so, dass der unechte
Ablauf verschwindet
Erfolgreiche Verifikation!Starte mit einer Ist die Eigenschaft P
Finde einen Ablauf r ,
Fehler gefunden!
Barbara Konig Modellierung, Analyse, Verifikation 109
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Abstraktionsverfeinerung
Eine der erfolgreichsten Methode zur Abstraktionsverfeinerungfunktioniert wie folgt:
Extrahiere aus dem Gegenbeispiel Pradikate, d.h., logischeFormeln.
Verwende eine Galoisverbindung, die Variablenbelegungendanach klassifiziert, welche Pradikate sie erfullen (sogenanntePradikatabstraktion).
Bestimme dann – basierend auf der Pradikatabstraktion – dieneue abstrakte Semantik des While-Programms und suchenach neuen Gegenbeispielen.
Dieser Vorgang wird iteriert, wobei die Menge der Pradikate,nach denen abstrahiert wird, immer mehr anwachst.
Barbara Konig Modellierung, Analyse, Verifikation 110
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Hoare-Logik
Verwendete Pradikate bzw. Formeln:
Boolesche Ausdrucke mit Existenzquantoren (∃x) und All-quantoren (∀x).
Erweiterung der AuswertungsfunktionB : BExp× State→ {true, false} fur Boolesche Ausdrucke:
Allquantor:
B(∀x p, σ) =
{true falls fur alle z ∈ Z gilt: B(p, σ[x 7→ z ]) = truefalse sonst
Existenzquantor:
B(∃x p, σ) =
{true falls es ein z ∈ Z gibt mit B(p, σ[x 7→ z ]) = truefalse sonst
Barbara Konig Modellierung, Analyse, Verifikation 111
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Hoare-Logik
Wir schreiben σ |= b, falls B(b, σ) = true, d.h., σ ist ein Modellfur b.
Folgerung: Wir sagen, dass q eine Folgerung von p ist(p |= q), wenn fur alle σ ∈ State aus σ |= p immer σ |= qfolgt.In diesem Fall sagt man auch: p ist starker als q bzw. q istschwacher als p.
Aquivalenz: Wir sagen, dass p aquivalent zu q ist (p ≡ q),falls sowohl p |= q, als auch q |= p gilt.
Barbara Konig Modellierung, Analyse, Verifikation 112
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Hoare-Logik
Hoare-Tripel: gegeben seien zwei Formeln p (Vorbedingung,precondition), q (Nachbedingung, postcondition) und ein Block C(Zuweisung, Skip-Anweisung oder Bedingung). Wir schreiben
{p}C {q},
wenn sichergestellt ist, dass nach Ausfuhrung von C die Formel qerfullt ist, wenn vor Ausfuhrung von C die Formel p erfullt ist.
Fur eine sequentielle Komposition C1; . . . ;Cn von Blockenschreiben wir {p}C1; . . . ;Cn {q}, falls es Formeln p1, . . . , pn−1 gibtmit
{p}C1 {p1} {p1}C2 {p2} . . . {pn−2}Cn−1 {pn−1} {pn−1}Cn {q}
Barbara Konig Modellierung, Analyse, Verifikation 113
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Hoare-Logik
Anforderungen an Hoare-Tripel:
Zuweisung: Falls {p} [x:=a]` {q}, σ |= p und 〈[x:=a]`, σ〉 → σ′,dann gilt σ′ |= q.
Skip-Anweisung: Falls {p} [skip]` {q}, σ |= p und〈[skip]`, σ〉 → σ′, dann gilt σ′ |= q.
If-Then-Else-Bedingung (Then-Fall): Falls {p} [b]` {q}, σ |= p und〈if [b]` then S1 else S2 fi, σ〉 → 〈S1, σ
′〉, dann gilt σ′ |= q.
If-Then-Else-Bedingung (Else-Fall):Falls {p} [¬b]` {q}, σ |= p und〈if [b]` then S1 else S2 fi, σ〉 → 〈S2, σ
′〉, dann gilt σ′ |= q.
Barbara Konig Modellierung, Analyse, Verifikation 114
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Hoare-Logik
While-Schleife (Eintritt in die Schleife):Falls {p} [b]` {q}, σ |= p und〈while [b]` do S od, σ〉 → 〈S;while [b]` do S od, σ′〉, danngilt σ′ |= q.
While-Schleife (Terminierung):Falls {p} [¬b]` {q}, σ |= p und 〈while [b]` do S od, σ〉 → σ′,dann gilt σ′ |= q.
Barbara Konig Modellierung, Analyse, Verifikation 115
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Hoare-Logik
Schwachste Vorbedingung: Gegeben sei eine Formel q und einBlock C . Dann bezeichnen wir die schwachste Vorbedingung(weakest precondition) p, fur die {p}C {q} gilt, mit wp(C , q). Siekann folgendermaßen ermittelt werden:
Zuweisung: wp([x:=a]`, q) = q[x/a]
Skip-Anweisung: wp([skip]`, q) = q
Bedingung: wp([b]`, q) = (q ∧ b) ∨ ¬b ≡ q ∨ ¬b ≡ b → q
Barbara Konig Modellierung, Analyse, Verifikation 116
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Hoare-Logik
Starkste Nachbedingung: Gegeben sei eine Formel p und ein BlockC . Dann bezeichnen wir die starkste Nachbedingung (strongestpostcondition) q, fur die {p}C {q} gilt, mit sp(p,C ). Sie kannfolgendermaßen ermittelt werden:
Zuweisung: sp(p, [x:=a]`) = ∃x’ (p[x/x’] ∧ x = a[x/x’])
Skip-Anweisung: sp(p, [skip]`) = p
Bedingung: sp(p, [b]`) = p ∧ b
Barbara Konig Modellierung, Analyse, Verifikation 117
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Hoare-Logik
Iteriertes Bilden von schwachsten Vorbedingungen und starkstenNachbedingungen:
wp(C1; . . . ;Cn, q) = wp(C1; . . . ;Cn−1,wp(Cn, q))
sp(p,C1; . . . ;Cn) = sp(sp(p,C1),C2; . . . ;Cn)
Barbara Konig Modellierung, Analyse, Verifikation 118
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Hoare-Logik
Aufgabe: Betrachten Sie folgende Folgen von Blocken undbestimmen Sie jeweils die schwachste Vorbedingung fur q = (x<y)
und die starkste Nachbedingung fur p = (x=3).
1 [y<z]1;[x:=z+1]2;[z=3]3
2 [x<y-1]1;[skip]2;[x:=x+1]3
Barbara Konig Modellierung, Analyse, Verifikation 119
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Hoare-Logik
Undurchfuhrbare Ablaufe (= unechte Gegenbeispiele):Das Hoare-Tripel {true}C1; . . . ;Cn {false} bedeutet, dass derAblauf C1; . . . ;Cn unter keiner Variablenbelegung durchfuhrbar ist.
Beispiele fur undurchfuhrbare Ablaufe:
1 [x=1]1;[x=2]2
2 [x<y]1;[x:=x+1]2;[x>y]3
3 [x:=c]1;[c:=c+1]2;[y:=c]3;[x=m]4;[y=m]5
Barbara Konig Modellierung, Analyse, Verifikation 120
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Pradikatabstraktion
Verband fur die Galois-Verbindung:
Gegeben: Menge Var von Variablen und eine Menge {p1, . . . , pn}von Pradikaten (d.h., Formeln) uber diesen Variablen.Wir definieren den Verband Abs(p1, . . . , pn):
Zugrundeliegende Menge:
enthalt alle Konjunktionen der Pradikatep1, . . . , pn,¬p1, . . . ,¬pn (wobei kein Pradikat sowohlpositiv als auch negativ vorkommt)true (entspricht der leeren Konjunktion) undfalse (entspricht pi ∧ ¬pi ).
Verbandsordnung: Folgerung |=
Barbara Konig Modellierung, Analyse, Verifikation 121
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Pradikatabstraktion
Infimum und Supremum im Verband Abs(p1, . . . , pn):
Infimum von q1, q2 ∈ Abs(p1, . . . , pn):
q1 u q2 ≡ q1 ∧ q2 (falls Pradikate pi , ¬pi zusammentreffen, soerhalt man false)
Supremum von q1, q2 ∈ Abs(p1, . . . , pn):
q1 ∨ q2 ist nicht notwendigerweise im Verband enthalten!
q1 t q2 ist die starkste Formel q ∈ Abs(p1, . . . , pn), fur dieq1 |= q und q2 |= q gilt.
Sei q eine beliebige Formel. Wir schreiben im folgenden q fur diestarkste Formel aus Abs(p1, . . . , pn), fur die q |= q gilt.Das heißt q1 t q2 = q1 ∨ q2.
Barbara Konig Modellierung, Analyse, Verifikation 122
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Pradikatabstraktion
Galois-Verbindung fur die Pradikatabstraktion:
Variablenbelegungen σ ∈ State werden danach klassifiziert, ob siebestimmte Pradikate erfullen oder nicht erfullen.
α : P(State)→ Abs(p1, . . . , pn) γ : Abs(p1, . . . , pn)→ P(State)
α(Σ) =⊔{qσ | σ ∈ Σ} γ(q) = {σ | σ |= q}
wobei Σ ⊆ State, q ∈ Abs(p1, . . . , pn).
Außerdem ist qσ die starkste Formel in Abs(p1, . . . , pn), fur dieσ |= qσ gilt. D.h., qσ enthalt pi ∈ {p1, . . . , pn}, falls σ |= pi und¬pi , falls σ 6|= pi .
Barbara Konig Modellierung, Analyse, Verifikation 123
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Pradikatabstraktion
Abstrakte Semantik bei der Pradikatabstraktion:
〈[x:=a]`, p〉 =⇒ sp(p, [x:=a]`) [ass] 〈[skip]`, p〉 =⇒ p [skip]
〈S1, p〉 =⇒ 〈S ′1, q〉〈S1;S2, p〉 =⇒ 〈S ′1;S2, q〉
[seq1]〈S1, p〉 =⇒ q
〈S1;S2, p〉 =⇒ 〈S2, q〉[seq2]
〈if [b]` then S1 else S2 fi, p〉 =⇒ 〈S1, sp(p, [b]`)〉 [if1]
〈if [b]` then S1 else S2 fi, p〉 =⇒ 〈S2, sp(p, [¬b]`)〉 [if2]
〈while [b]` do S od, p〉 =⇒ 〈S;while [b]` do S od, sp(p, [b]`)〉 [wh1]
〈while [b]` do S od, p〉 =⇒ sp(p, [¬b]`) [wh2]
Barbara Konig Modellierung, Analyse, Verifikation 124
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Pradikatabstraktion
Beispiel: analysieren Sie folgendes Programm, um zu zeigen, dassBlock 7 nicht erreichbar ist.
if [x>y]1 then
while [y6=0]2 do
[x:=x-1]3;[y:=y-1]4
od;
if [x>y]5
then [skip]6
else [skip]7
fi
else [skip]8 fi
Verwenden Sie dazu die Pradikate p1 = (x>y) und p2 = (x≥y).
Barbara Konig Modellierung, Analyse, Verifikation 125
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Pradikatabstraktion
Problem bei der Pradikatabstraktion:
sp(p,C ) (die starkste Formel aus Abs(p1, . . . , pn)), die nach einemBlock gilt, ist im Allgemeinen nicht berechenbar(Unentscheidbarkeit!)
Mogliche Losungen:
Uber-Approximation: Berechnen von moglicherweiseschwacheren Nachbedingungen (oft mit Theorembeweisern).
Keine Multiplikation: fur bestimmte Typen von Programmenohne Multiplikation ist die Folgerungsbeziehung entscheidbar(Stichwort: Presburger-Arithmetik & SMT-Solver)
Endliche Wertebereiche: wir arbeiten nur auf n-stelligenBinarzahlen (Reprasentation von Pradikaten durch BinaryDecision Diagrams)
Barbara Konig Modellierung, Analyse, Verifikation 126
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Abstraktionsverfeinerung
ja
nein
Ablauf ist echtAblauf ist unecht
der P verletzt
in der Abstraktion erfullt?groben initialen Abstraktion
Verfeinere die Abstraktion
so, dass der unechte
Ablauf verschwindet
Erfolgreiche Verifikation!Starte mit einer Ist die Eigenschaft P
Finde einen Ablauf r ,
Fehler gefunden!
Barbara Konig Modellierung, Analyse, Verifikation 127
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Abstraktionsverfeinerung
Zu losende Probleme:
Wie bestimmt man, ob ein Ablauf unecht ist?
Wie extrahiert man aus einem unechten Ablauf die neuenPradikate?
Barbara Konig Modellierung, Analyse, Verifikation 128
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Abstraktionsverfeinerung
Wie bestimmt man, ob ein Ablauf unecht ist? (unechter Ablauf =spurious counterexample)
Gegeben sei ein Ablauf r = C1; . . . ;Cn.
Der Ablauf r ist unecht genau dann, wenn {true} r {false}.
Das ist dann der Fall wenn
wp(r , false) ≡ true oder
sp(true, r) ≡ false
(Evtl. Probleme mit der Unentscheidbarkeit der Aquivalenz.)
Barbara Konig Modellierung, Analyse, Verifikation 129
DatenflussanalyseJava Bytecode Verifier
Abstrakte Interpretation
Grundlagen der abstrakten InterpretationAbstrakte Semantik von While-ProgrammenPradikatabstraktion und Abstraktionsverfeinerung
Abstraktionsverfeinerung
Sei r = C1; . . . ;Cn ein unechter Ablauf und seien p1, . . . , pn−1
Pradikate mit
{true}C1 {p1}C2 {p2} . . . {pn−2}Cn−1 {pn−1} Cn {false}
Durch das Hinzufugen der Pradikate p1, . . . , pn−1 zum Verbandverschwindet der unechte Ablauf.
Barbara Konig Modellierung, Analyse, Verifikation 130