Details

Autor(en) / Beteiligte

• Jakobs, Marie-Christine
• Wehrheim, Heike[Akademischer Betreuer]
• Beyer, Dirk[Akademischer Betreuer]
• Bodden, Eric[Akademischer Betreuer]
• Platzner, Marco[Akademischer Betreuer]
• Platenius, Marie Christin[Akademischer Betreuer]

Titel

On-The-Fly safety checking - customizing program certification and program restructuring

Ort / Verlag

Paderborn

Erscheinungsjahr

2017

Verknüpfte Titel

Beschreibungen/Notizen

• Tag der Verteidigung: 05.05.2017
• ger: Viele Alltagsgegenstände führen Software aus. Daher sollte sie fehlerfrei sein. Firmen betreiben viel Aufwand, .z.B. formale Verifikation, um Fehler in der Software zu eliminieren oder deren Abwesenheit zu zeigen. Software aufwändig validiert wurde, kann bedenkenlos installiert werden.Früher installierten Verbraucher Software aus großen Softwarehäusern, von denen sie Software bereits nutzten. Aufgrund langzeitiger Geschäftsbeziehung konnten Verbraucher die Softwarequalität dieser Hersteller abschätzen. Heute wird Software vermehrt von unbekannten Entwicklern geschrieben. Daher kann nicht erwartet werden, dass der Verbraucher auf die Fehlerfreiheit der Software vertraut.In dieser Arbeit entwickeln wir Techniken, die ohne Vertrauen in den Hersteller auskommen und den Verbraucher von der Fehlerfreiheit einer Software überzeugen. Die Techniken basieren auf formaler Verifikation, sind automatisch und können an die zu prüfende Eigenschaft und die Verifikationstechnik angepasst werden. Die Idee ist, dass der Hersteller die Informationen aus der aufwändigen Verifikation nutzt, um die Nachprüfung des Verbrauchers zu vereinfachen. Wir verfolgen zwei Ansätze, und deren Integration. In der konfigurierbaren Programmzertifizierung liefert der Hersteller das Programm und ein Zertifikat (Teile des Verifikationsbeweises). Der Verbraucher prüft, ob das Zertifikat bezeugt, dass die Verifikation erfolgreich war. Das Konzept Programs from Proofs nutzt die Informationen der Verifikation, um ein Programm zu erzeugen, dass der Verbraucher mit einer Datenflussanalyse verifizieren kann. Wir beweisen für alle Techniken, dass im Falle einer erfolgreichen Nachprüfung das Softwareprodukt die geprüfte Eigenschaft erfüllt, und, dass die Nachprüfung bei regelkonformen Produzenten erfolgreich ist. Alle Techniken wurden auch praktisch evaluiert.
• eng: Many artifacts that we use run software. Thus, software should be error free. To eliminate errors, companies extensively validate their software. For example, formal verification is used to find errors and to finally show error freeness. Software originating from a company running an extensive validation phase can be installed on our systems without any further checks.In the past, users often installed software from large companies from which they used and experienced different software already. Due to the long-term business relationship, users could estimate the quality of the software produced by these companies. However, nowadays software is also written by unknown software producers. There is no reason why one should trust that these producers build error free software products.In this thesis, we develop techniques that eliminate the trust in the producer while convincing a consumer that a software product is error free. Our techniques are based on formal verification, are fully automatic, and configurable to the property of interest and the verification technique. The idea is that the producer performs the expensive verification and uses the proof obtained by the verification to simplify the consumer's reinspection. We present techniques from two directions. In our configurable program certification approaches, the producer attaches some witness information (parts of the proof) to the program and the consumer solely checks that the attached information is a proper witness. The Programs from Proofs approach uses the proof to restructure the program such that a simple dataflow analysis is sufficient to verify the restructured program. Finally, we discuss the integration of the two directions. For all approaches, we show that a successful reinspection implies that the program fulfills the checked property and the reinspection succeeds when the producer does not ...