qualitätssicherung von software (swqs) prof. dr. holger schlingloff humboldt-universität zu berlin...
Post on 05-Apr-2015
108 Views
Preview:
TRANSCRIPT
Qualitätssicherung von Software (SWQS)
Prof. Dr. Holger Schlingloff
Humboldt-Universität zu Berlinund
Fraunhofer FOKUS
6.6.2013: Statische Analyse
Folie 2H. Schlingloff, Software-Qualitätssicherung
Fragen zur Wiederholung
• Was ist der Unterschied Software-HW Model Checking?
• Was versteht man unter Zustandsraumexplosion?
• Was kann dagegen tun?
Folie 3H. Schlingloff, Software-Qualitätssicherung
statische Analyse
• ohne semantische Konsequenzen Coding Rules Checker, Linker, …
• mit semantischer Bedeutung Variableninitialisierung Range and Bounds Checker Pointer and Storage Allocation Race Condition
• Verifikationswerkzeuge Modellprüfer, Äquivalenzprüfung interaktive Beweisverfahren
zunehm
ende
Mäch
tig
keit
zunehm
ende
Kom
ple
xit
ät
Folie 4H. Schlingloff, Software-Qualitätssicherung
Statische Analyse: Compiler
• Typkorrektheit
• Initialisierung von Variablen
• Programmflussgraph Unerreichbarer Code Unveränderliche Felder Konstante Terme und Bedingungen
• Feldgrenzenverletzung ?
• Nullzeiger-Dereferenzierung ?
• Synchronisationsfehler ?
Folie 5H. Schlingloff, Software-Qualitätssicherung
statische Analysewerkzeuge
• Es gibt „viele“http://en.wikipedia.org/wiki/
List_of_tools_for_static_code_analysis
• einfache Tools, in Compiler oder IDE integriert
• Spezialwerkzeuge zur tiefergehenden Analyse Lint (Splint, PCLint,…) ESC/Java2 PolySpace Verifier …
• Unterschiedliche Analysetiefe, unterschiedliche Ergebnisrate
• Hauptproblem: false positives
Folie 6H. Schlingloff, Software-Qualitätssicherung
Lint
• Grundidee Programmierer annotiert das Programm Lint prüft ob Annotationen erfüllt sind
• Einfache (schnelle!) Datenflussanalyse!Beispiel:
Folie 7H. Schlingloff, Software-Qualitätssicherung
anderes Beispiel: only
•einzige Referenz zu besagtem Objekt
•explizite Abgabe der Besitzrechte am Objekt
Folie 8H. Schlingloff, Software-Qualitätssicherung
Buffer Overflow
• Verantwortlich für viele Sicherheitslücken• Annotation der Puffergröße in Splint
Folie 9H. Schlingloff, Software-Qualitätssicherung
Probleme bei Abstraktionen
• falsche Positive Überapproximation des Programms Bsp.: if (p&&q) ... if (p) ... mangelnde Korrektheit: Fehler die evtl. keine sind erhöhter QS-Aufwand
• falsche Negative• Unterapproximation des Programms• Bsp.: if (p) ... if (p&&q) ...• mangelnde Vollständigkeit: manche Fehler werden nicht
erkannt• trügerische Sicherheit
Folie 10H. Schlingloff, Software-Qualitätssicherung
Bsp.: Cppcheck
Folie 11H. Schlingloff, Software-Qualitätssicherung
Bsp.: ESC/Java2
Folie 12H. Schlingloff, Software-Qualitätssicherung
Abstrakte Interpretation
• Wie findet man solche Probleme? Ausführung des Programms mit symbolischen
Werten (bzw. „Mengen von Werten“) Berechnung der möglichen Werte jeder
Variablen an jeder Programmstelle („collecting semantics“)
•Was kann man daraus ableiten? Initialisierungen, Überlauf, Division durch Null,
Indexüberschreitung, … Keine Aussage über Terminierung oder
korrekte Funktionalität
Folie 13H. Schlingloff, Software-Qualitätssicherung
Beispiel
•{x{2,4,6}} x=3*x+1 {x{7,13,19}}
AB
C
D
E F
G H
Folie 14H. Schlingloff, Software-Qualitätssicherung
allgemeine Vorgehensweise
• ergibt ein (rekursives) Gleichungssystem• Lösung als kleinster Fixpunkt
Folie 15H. Schlingloff, Software-Qualitätssicherung
Fixpunktsatz von Knaster und Tarski
• jede monotone Funktion f in einem vollständigen Verband hat einen kleinsten Fixpunkt, nämlich inf{x|x≤f(x)}
• wenn f stetig ist, so ist der kleinste Fixpunkt gegeben durch lim fn(0)
• Für die statische Analyse bedeutet das starte mit allen Gleichungswerten undefiniert berechne den Wert der (n+1)-ten Iteration einer
Gleichung aus den Werten der n-ten Iteration solange, bis sich nichts mehr ändert
Folie 16H. Schlingloff, Software-Qualitätssicherung
Probleme
•Terminierung des Verfahrens ist nicht garantiert!(Limesbildung über transfinite Ordinalzahlen)
•Rechnen mit symbolischen Zustandsmengen z.B. Menge der Quadratzahlen, symbolische
Ausdrücke wie x2+3x+5 usw. Gleichheit von beliebigen
Mengenausdrücken unentscheidbar!
Folie 17H. Schlingloff, Software-Qualitätssicherung
nochmal: Abstraktion
• Beispiel x*y=z (xmod n * ymod n) mod n = zmod n
• „mod n“ ist eine Abstraktion, die einen unendlichen Wertebereich auf {0,1,...,n-1} abbildet
• um zu prüfen, ob eine Multiplikation korrekt ausgeführt wurde, kann man die Abstraktion prüfen 8*7=56 2 * 1 = (8mod 3 * 7mod 3) mod 3 = 56mod 3
(8mod 3 * 7mod 3) mod 3 57mod 3 8*757 aber: 8*7 65, obwohl (8mod 3 * 7mod 3) mod 3 = 65mod 3
• „false positives“: Der abstrakte Check findet keinen Fehler, obwohl noch einer enthalten ist (vgl. Test)
Folie 18H. Schlingloff, Software-Qualitätssicherung
• Datenabstraktion x x mod 3 x*y ((x mod 3) * (y mod 3) mod 3)
• eigentlich Rechnen mit Mengen von Werten konkreter Datenraum wird partitioniert in Mengen
von Restklassen 0, 1, 2 konkrete Operationen werden abgebildet auf
abstrakte; Rechnen mit Repräsentanten
• Eigenschaftserhaltung C erfüllt P A erfüllt P A verletzt P C verletzt P
Folie 19H. Schlingloff, Software-Qualitätssicherung
Wie abstrahieren?
•Restklassen
•Positiv/Null/Negativ (vgl. Grenzwertanalyse)
•Polyeder-Verband Konjunktionen linearer Ungleichungen z.B. 17≤x≤32 & 1≤y<100
•Rechnungen in diesem Verband lassen sich in polynomialer Zeit (schnell!) nachvollziehen z.B. x = x+y ergibt 18≤x≤132
top related