Formal Methods: Best of 2010
| Typ: | Seminar |
|---|---|
| Links: | Aushang.pdf |
| Lehrstuhl: | Anwendungsorientierte Formale Verifikation; Logik und Formale Methoden |
| Semester: | Hauptdiplom |
| Ort: | Gebäude 50.34, SR 131 |
| Zeit: | Blockveranstaltung am Semesterende |
| Beginn: | 13.04.2011 |
| Dozierende: |
Prof. B. Beckert Prof. P. H. Schmitt Thorsten Bormer Daniel Bruns David Faragó Christoph Gladisch Dr. Vladimir Klebanov Christoph Scheben Mattias Ulbrich |
| SWS: | 2 |
| ECTS: | 3 |
Thema
Software-basierte Systeme sind aus unserem Alltag nicht mehr wegzudenken. Sie halten Einzug in nahezu alle Bereiche unseres Lebens. Allerdings bleibt die Qualität der Software trotz ihrer wachsenden Bedeutung nur allzuoft auf der Strecke. In manchen Bereichen mag dies tolerierbar sein, sobald aber durch fehlerhafte Software Menschenleben gefährdet sind (z. B. Eisenbahnwesen oder Anwendungen in der Medizin) oder hohe finanzielle Schäden zu befürchten sind (z. B. Internet-Banking), muss auf die Qualität - insbesondere auf die Korrektheit - der Software besonderer Wert gelegt werden.
Deswegen gibt es umfangreiche Forschung zu (formalen) Methoden, deren Anwendung es tatsächlich ermöglicht, fehlerfreie Software zu entwickeln oder zumindest die Qualität der Software deutlich zu erhöhen. In diesem Seminar wird eine Auswahl an aktuellen Ergebnissen aus dieser Forschung vorgestellt.
Die Seminarteilnehmer bereiten unter Anleitung durch einen Betreuer einen Vortrag zu einem dieser Forschungsergebnisse vor. Ziel ist, dass der Vortragende selbst sich ein gründliches Verständnis des Themas erarbeitet und dem Auditorium in der Kürze der zur Verfügung stehenden Zeit die wesentlichen Informationen und Einsichten vermittelt.
Organisatorisches
- Anmeldung bei Frau Beckert in Raum 321
- Vorbesprechung am Mi 13.04.11, 13:15-14:00 Uhr in SR 131
- Vorbereitungstermin am Di 17.05.11, 13:15-14:00 Uhr, voraussichtlich in SR 131
- jeder Teilnehmer stellt in ca. 5 min die Gliederung seines Vortrags vor
- dazu höchstens 5 Folien
- Für die Ausarbeitung gilt:
- 5-10 Seiten
- auf Deutsch oder auf Englisch
- mit LaTeX und der verbindlichen IEEE Formatvorlage erstellt
- Vorträge am 8. Juli, 14:00-17:15 in SR 236, im Rahmen des Research-Seminars
- jeweils ca. 45 min + 10 min Diskussion
- auf Deutsch oder auf Englisch
Vortragsthemen
-
Testing with Model Checkers: a survey. Chapter 3: Coverage-based test case generation
(Software Testing, Verification and Reliability, 2009, Paper)
Testing remains the most important method to check the quality and reliability of software. Formal model-based testing techniques can use model checkers to create counterexamples, which are then interpreted as test cases.
This journal article thoroughly introduces model checking and testing with model checkers in Sections 2. In this seminar, Section 3 about coverage-based test case generation should be presented, and the corresponding parts of the discussion in Section 5. -
When BDDs Fail: Conformance Testing with Symbolic Execution and SMT solving
(IEEE International Conference on Software Testing, Verification and Validation, 2010, Paper)
In domains where data plays an essential part, specifications with explicit data enumeration often lead to state space explosion. As alternative, symbolic transition systems can be used for specification. Model-based conformance testing can then use new symbolic test case generation techniques based on symbolic execution and on satisfiability (modulo theory; SMT) solving.
After some introduction, the paper explains the test case generation algorithm in Section 3, which should be the focus in this seminar. Section 4 gives two case studies (the Conference Protocol and the Session Initiation Protocol used in Voice-over-IP), one of which can optionally be presented. -
Local Reasoning and Dynamic Frames for the Composite Pattern
(Intern. Conference on Verified Software: Theories, Tools and Experiments, 2010, Paper)
Einer der Fortschritte, welche die formale Programmverifikation in den letzten Jahren gemacht hat, besteht darin nicht nur Vor- und Nachbedingungen für Prozeduren (Methoden) zu betrachten, sondern auch die Spezifikation von Objekten, oder feinkörniger von "locations", die von einer Prozedur verändert werden und/oder von denen ihr Ergebniss abhängt. In der betrachteten Arbeit benutzen die Autoren dafür den Begriff "read-write-effects". Analog kann man auch, meist automatisch, ermitteln von welchen "locations" die Gültigkeit einer Formel der Spezifikationssprache abhängt. Damit lassen sich dann logische Schlüsse der folgenden Art ziehen:* vor Ausführung der Prozedur P ist die Invariantenformel I wahr
Das erklärt das Konzept "local reasoning" im Titel der Arbeit. Der Text selbst beschreibt die Einzelheiten anhand eines durchgängigen Beispiels, der Spezifikation des "composite pattern".
* die Prozedur verändert nur die "locations" R1
* die Gültigkeit von I hängt höchstens von den "locations" R2 ab
* R1 und R2 sind disjunkt,
dann gilt I auch nach Ausführung von P. -
Temporallogische Laufzeitprüfung - temporaljmlc: A JML Runtime Assertion Checker Extension for Specification and Checking Temporal Properties
(IEEE International Conference on Software Engineering and Formal Methods, 2010, Paper)
Beim Spezifizieren von Programmen werden Methoden typischerweise mit Vor- und Nachbedingungen versehen. Dies erlaubt jedoch nicht temporale Aussagen wie "Methode x wird irgendwann in der Zukunft aufgerufen", die für die Verifikation von Sicherheitseigenschaften benötigt werden.
Mit "temporaljmlc" stellten Hussain und Leavens ein Werkzeug zur Laufzeitprüfung auf der Konferenz "Software Engineering and Formal Methods" (SEFM 2010) vor. Die Spezifikationen sind in einer Variante der Java Modeling Language (JML) geschrieben, die um die aus der linearen temporalen Logik (LTL) bekannten Operatoren erweitert wurde. -
Spezifikationsverfeinerung - A Refinment Methodology for Object-oriented Programs
(Formal Verification of Object-oriented Software, 2010, Paper)
Verfeinerung ist eine beliebte Methode in der Gewinnung von Programmen aus Spezifikationen. Sie wird jedoch meist in abstrakteren Spezifikationssprachen angewandt; dabei werden Phänomene der objektorientierten Programmierung (wie Aliasing) nicht berücksichtigt.
Tafat et al. haben auf der Konferenz "Formal Verification of Object-oriented Software" (FoVeOOS 2010) ein Verfahren vorgestellt, das Verfeinerung auch in einer implementierungsnahmen Spezifikation (wie sie etwa JML bietet) möglich macht. -
HOL-Boogie - An Interactive Prover-Backend for the Verifying C Compiler
(Journal of Automated Reasoning, Paper)
Boogie is a verification condition generator for an imperative core language and has front-ends for many programming languages. Boogie’s verification conditions are usually transferred to automated theorem provers. In this paper, a proof environment, HOL-Boogie, that combines Boogie with the interactive theorem prover Isabelle/HOL is presented. In particular, the authors Böhme, Moskal, Schulte, and Wolff present specific techniques combining automated and interactive proof methods for code verification. The main goal of the environment is to help program verification engineers in their task to “debug” annotations and to find combined proofs where purely automatic proof attempts fail. -
Local Reasoning about While-Loops
(VSTTE Theory WS, Paper)
Loops are one of the major challenges when assuring correctness of programs with formal methods. Current logic-based verification approaches require the verification engineer to provide a suitable loop invariant. Local reasoning is a powerful feature that often allows simpler specifications and correctness proofs. However, this power is not used to reason about while-loops. In this paper an inference rule is presented that allows using local reasoning to verify the partial correctness of while-loops. Instead of loop invariants this inference rule uses pre- and post-conditions for loops. This provides a different view of while-loops that is even without local reasoning often beneficial. -
Applying SMT in Symbolic Execution of Microcode
((best paper award) FMCAD, 2010, Paper)
Abstract—Microcode is a critical component in modern microprocessors, and substantial effort has been devoted in the past to verify its correctness. A prominent approach, based on symbolic execution, traditionally relies on the use of boolean SAT solvers as a backend engine. In this paper, the authors investigate the application of Satisfiability Modulo Theories (SMT) to the problem of microcode verification, and experimentally evaluate the effectiveness of some optimizations. The results demonstrate the potential of SMT technologies over pure boolean SAT for which the authors have received a best paper award at the FMCAD conference. -
Predictive Black-Box Mitigation of Timing Channels
(ACM conference on Computer and communications security (CCS), 2010, Paper)
The topic of this paper is information flow security. Information flow is the transfer of information from a variable x to a variable y in a given process. Not all flows may be desirable. For example, a system shouldn't leak any secret (partially or not) to public observers (from Wikipedia). The source of the leakage of information is categorized in terms of channels. One of those categories are timing channels: attacks exploit the timing of cryptographic operations, of cache operations, and of web server responses to learn about secret information. These attacks work even without cooperation of any software on the system being timed. Controlling timing channels is difficult but important. This paper introduces a scheme for mitigating timing channels.
-
Paralocks - Role-Based Information Flow Control and Beyond
(ACM Symposium on Principles of Programming Languages, 2010, Paper)
In dem Papier wird eine sehr flexible Sprache, genannt Paralocks, zur Formulierung von Sicherheitsvorschriften (security policies) vorgestellt. Aus logischer Sicht handelt es sich dabei um universelle Hornklauseln. Anhand einer simplen Programmiersprache wird exemplarisch gezeigt, wie sich die Überwachung/Verifikation einer Paralock Spezifikation durch eine geeignetes Typsystem realisieren lässt. Als Vorausetzung zur Feststellung, daß das Typsystem das Gewünschte tut, wird zunächst formal definiert, was Informationsflusssicherheit im Kontext von Paralock bedeutet. Das ist eine Variante des üblichen "non-interfernce" Begriffs. -
From Dynamic to Static and Back: Riding the Roller Coaster of Information-Flow Control Research
(Perspectives of Systems Informatics 2009, Paper)
The topic of this paper is information flow security. Information flow is the transfer of information from a variable x to a variable y in a given process. Not all flows may be desirable. For example, a system shouldn't leak any secret (partially or not) to public observers (from Wikipedia). Historically, dynamic techniques for enforcement of information flow policies are the pioneers of the area in the 70's. In their seminal work, Denning and Denning suggest a static alternative for information flow analysis. Following this work, the 90's see the domination of static techniques for information flow. This paper demonstrates that it is possible for a purely dynamic enforcement to be as secure as Denning-style static information flow analysis. /li> -
Verifikation eines Microkernels: L4.verified
(Communications of the ACM, 2009, Paper)
Die formale Verifikation komplexer, großer Softwaresysteme stellt eine besondere Herausforderung dar. Ein Beispiel eines solchen Vorhabens ist das Projekt "L4.verified". Ziel dieses Projekts ist der Korrektheitsbeweis der Implementation eines L4-basierten Microkernels, "seL4". Eine Übersicht über das Projekt und die darin erzielten Ergebnisse der Ende 2009 abgeschlossenen Verifikation wurden 2010 in den Communications of the ACM vorgestellt.
Der Inhalt des Vortrages sollte eine Übersicht der zugesicherten Korrektheitseigenschaften umfassen, die im Projekt verwendete Verifikationsmethodik erläutern, sowie einen Vergleich des Vorhabens mit ähnlichen Verifikationsprojekten ermöglichen.
Dokumente von springerlink.com sind von innerhalb des KIT-Netzwerkes erreichbar.