Post on 05-Apr-2015
1
Computergestützte Verifikation
28.6.2002
2
Beispiel für Shape-Analysis
Insert in Liste:
x : nichtleere Liste x
malloc(y) xy
y -> n = x xy
x = y xy
Coarsening xy
3
Beispiel statisch
1 read(n);2 i := 1;3 sum := 0;4 product := 1;5 while i <= n do6 sum := sum + 1;7 product := product * i;8 i := i + 1; end9 write(sum);10 write(product);
(product,10)
1 read(n);2 i := 1;
4 product := 1;5 while i <= n do
7 product := product * i;8 i := i + 1; end
10 write(product);
4
9. Sonstiges
Ziel: In einigen weiteren Domains Tragfähigkeit dergelernten Konzepte testen
5
9.1 Hybride Systeme
hybrid = kontinuierliche + diskrete Variablen
Hybrider Automat:
Einlaufen Auslaufen
h>= max
h <= minh’ [ -0.5,0.7]h’ [ -0.8,0.9]
(Der hier ist ein linearer Automat: x’ [c1,c2])
6
Verifikation linearer hybrider Automaten
geometrische Abstraktionen, z.B. Polyeder – analog Zonen
mehrere andere geometrische Formen, u.a. Ellipsen
Tool:HyTech (Berkeley)
7
Verifikation allg. hybrider Automaten
numerische Verfahren Fehlerbetrachtung notwendig
Tool: CheckMate (CMU)
“Flowpipe”1
2
3
4
5
6
7
8
9
10
4 3,6,7
8
9.2 Kompositionale Verifikation
System in Komponenten zerlegen
Komponenten verifizieren
Eigenschaft des Gesamtsystems schlußfolgern
Assume-Guarantee-Reasoning
9
Komponierte Systeme
Interessant vor allem: parallele Komposition
Komponente = Transitionssystem (mit benannten Aktionen)
Parallele Komposition S1 || S2:
S = S1 x S2
Übergänge: synchronisiert, wenn Aktion in A1 A2, sonst allein
10
Assume-Guarantee
{} S {}
, z.B. aus LTL-X
heißt: Jeder Pfad, der erfüllt und in S möglich ist,erfüllt .
11
Eine Kompositionsregel
unglaublich, aber wahr:
{} S1 {}{} S2 {}____________{} S1 || S2 {}
Grund: Jeder Pfad in S1 || S2 ist auch in S1 möglich
12
Problem: Zyklen
Mit || kann man keine ringförmige Argumentation aufbauen,und Assume-Guarantee in Ringen taugt nix
Aus {i} Si {(i+1) mod k}
folgt nichts für Gesamtsystem
13
Invarianten in Systemen mit Zyklen
Wenigstens geht Verifikation von Invarianten (G ) auch in ringförmigen Systemen
{i} Familie von Formeln mit Halbordnung
Zeigen für alle j,k in Komponenten:Ausi gilt bis Schritt k, falls i i
- i gilt bis Schritt k-1, sonstfolgt - j gilt in Schritt k
Dann gilt G (1... n ) im Gesamtsystem
14
9.3 Parametrisierte Systeme
Unendliche Familie gleich strukturierter Komponenten(z.B. Ring mit beliebig vielen Komponenten)
Wollen Resultat, das für jede Instanz gilt
15
Induktion
A) gilt für System mit 0 oder 1 Komponente Model Checking
I) Wenn für System mit max. k Komponenten, so auch mit k+1 Komponenten
kompliziert. Meist manuell.z.B.:Versuche, 2 oder mehr Komponenten derart zu abstrahieren,daß sich Resultat wie 1 Komponente verhält
.... .....
16
Small Model Properties
Viele Logiken, auch temporale, haben Eigenschaftender Form
Wenn in irgendeinem Modellgilt, so gibt es auch ein Modell der Größe k, wo gilt.
k z.B. Anzahl der freien Variablen in
Parametrisiertes Problem kann auf endlich viele Model Checking Probleme reduziert werden
17
9.4 Security-Protokolle
Betrachten nicht: Verschlüsselung/Entschlüsselung,
sondern vor allem: Verbindungsaufbau, Authentifizierung,...
“Perfekte Verschlüsselung”= Inhalt einer verschlüsselten Nachricht ist ohne Schlüssel nicht verfügbar
“Begrenzter Zufall”= Wenn eine Zufallszahl (“Nonce”) Bestandteil einer verschlüsselten Nachricht ist, gibt es keine Möglichkeit, den Wert dieser Zahl zu ermitteln, als die Nachricht zu entschlüsseln.
Beide Annahmen falsch, aber sinnvoll.
18
Beispiel 1
Austausch geheimer Information NA, NB (z.B. Session Key)
A B
{A,NA}PKB
{NA,NB}PKA
{NB}PKB
Attacke:
A B
{A,NA}PKB
{NA,NC}PKA
{NC}PKB
C
{A,NA}PKC
{NA,NC}PKA
{NC}PKC
C glaubt, mit Azu kommunizieren,anstatt mit B
19
Beispiel 2
A B: AB A: NB
A B: {NB}KAS
B S: {A,{NB}KAS}KBS
S B {NB}KBS
Attacke:
C B : A C B: CB A(C): NB
B C: NB’C B: {NB}KCS
C B: {NB}KCS
B S:{A,{NB}KCS}KBS
B S: {C,{NB}KCS}KBS
S B:{NB}KBS
S B: error
20
Elemente von Security-Protokollen
Teilnehmer (A,B, Server, Intruder,....)Kanäle (unsicher, d.h. Intruder kann abfangen, selbst senden usw.)Inhalte (Daten, Nonces, Timestamps)Schlüssel (symmetrisch oder asymmetrisch)Verschlüsselte Nachrichten { ... }K
Ableitbares Wissen:1. Jede gesendete Nachricht2. { bla }K + K bla3. bla + K { bla }K
21
Model Checking
Zustand: -ehrliche Teilnehmer + Abarbeitungszustand-Intruder, evt. personifiziert als ehrlicher Teilnehmer + abgeleitetes Wissen-1 oder mehrere Protokollinstanzen
Übergänge:ehrliche Agenten: laut ProtokollIntruder: beliebiger Nichtdeterminismus, außerAnnahmen nach perfekter Verschlüsselung, nach jedemSchritt Abschluss bzgl. ableitbarem Wissen
22
Alternative: Modale Logik
“A glaubt ”
“Wenn A glaubt, Nachricht M kommt von B, dannkommt Nachricht M von B”
Beweissysteme, “SPI-Calculus”,spezifische Model Checker für solche modalen Logiken
Andere Typen von Attacken brauchen andereVerifikationstechniken, z.B. Denial-of-Service
E-Commerce: “A glaubt ” reicht nicht, stattdessen: “A kann Dritten gegenüber nachweisen”
23
9.5 Worst-Case-Execution-Time-Analyse
geg: Programm, Prozessor, Taktfrequenz
ges: max. Abarbeitungszeit T: jede Ausführung braucht garantiert nicht länger als T T möglichst klein
Probleme im Low-Level und im High-Level-Bereich
24
Low-Level Probleme
-Pipelining-Pre-Fetch, Branch-Prediction-Instruction Cache, Datencache
nicht unbedingt unser Problem, aber es gibt z.B.zur Cache-Analyse Ansätze, die auf Abstract Interpretationberuhen
25
High-Level Probleme
Wie oft werden Schleifen durchlaufen?
if B1 then {7 ms} else {5 ms} end; if B2 then {8 ms} else {3 ms} end;
Max. 15? Nur wenn B1 B2 erfüllbar
Model Checking könnte helfen, High Level-Probleme zu lösen.
(in etablierten Tools werden max. Durchlaufzahlen vomNutzer vorgegeben)
26
Model Checking für HL-WCET
geg.: WCET für Basic Blocks (verzweigungsfreie Teile) aus LL-WCET Analyse
Programm annotieren:
wcet := 0...if B then wcet += k1; ... else wcet += k2; ... end...while B do wcet += k3; ... end...
27
...
while-Schleifen k Iterationen abwickeln, k+1-te Iteration mitLabel L markieren.Programm zu SAT-Checker schicken:
- falls EF L erfüllbar, k vergrößern
- Per Binärschachtelung kleinstes T finden, wo AG wcet < T gilt
Ausgabe T