Correctness-by-Construction for Correct and Secure Software Systems

Die Gewährleistung der Sicherheit (funktionale Sicherheit und Datensicherheit) von Softwaresystemen ist heute wichtiger denn je, da kritische Bereiche (wie in der Automobilindustrie, der Luftfahrt oder dem Gesundheitswesen) immer softwareintensiver werden. In der Regel wird solche kritische Software umfassend getestet, aber Tests allein können die Korrektheit nicht garantieren. Daher sind formale Ansätze erforderlich, um die Sicherheit der entwickelten Software zu gewährleisten. Für funktionale Korrektheit ist die Post-hoc-Verifikation der Stand der Technik. Unter Post-hoc-Verifikation verstehen wir, dass ein Programm implementiert, mit einem Vor-/Nachbedingungsvertrag spezifiziert und dann verifiziert wird. Dieser Ansatz hat jedoch den Nachteil, dass er den Entwicklern keinen Leitfaden für das Schreiben von korrektem Code bietet. Wenn ein ohne Leitfaden entwickeltes Programm nicht verifiziert werden kann, ist es oft schwierig, die Ursachen dafür zu finden. Es kann sich um eine fehlerhafte Implementierung oder eine ungeeignete Spezifikation des Programms handeln. Dies hat zur Folge, dass es kostspielig ist, das Programm zu debuggen und erneut zu verifizieren. Im Hinblick auf die Datensicherheit ist es wichtig, die Vertraulichkeit und Integrität der verarbeiteten Daten zu gewährleisten. Hier sind statische und dynamische Taint-Analysen üblich, bei denen die Daten mit einer Sicherheitsstufe versehen werden, um zu analysieren, ob es einen Fluss von einer sicheren Quelle zu einer öffentlichen Senke gibt, der durch eine Sicherheitsrichtlinie verboten wurde. Diese Post-hoc-Analyse hat denselben Nachteil wie die Post-hoc-Verifizierung: Ein fehlerhaftes Programm muss korrigiert und dann neu analysiert werden, um sicherzustellen, dass die Schwachstelle behoben ist. Der allgemeine Nachteil von Post-hoc-Analyse- und Verifizierungstechniken besteht darin, dass sie zwar Probleme im Code aufdecken, aber nicht bei deren Behebung helfen.

Correctness-by-Construction (CbC) ist ein alternativer Ansatz zur Programmentwicklung, bei dem ein Programm direkt so konstruiert wird, dass es korrekt ist. Ausgehend von einem spezifizierten, aber abstrakten Programm wird eine Reihe von Verfeinerungsregeln angewendet, um das Programm in eine konkrete Implementierung zu verfeinern. Jede angewandte Verfeinerungsregel garantiert, dass das zu entwickelnde Programm die ursprüngliche Spezifikation erfüllt. Somit ist das resultierende Programm konstruktionsbedingt korrekt. Es wird argumentiert, dass mit dem CbC-Ansatz Fehler in einem frühen Stadium der Entwicklung entdeckt werden und durch einen strukturierten Programmentwicklungsansatz leichter behoben werden können. Trotz dieser Vorteile hat sich CbC noch nicht als Entwicklungsansatz für sicherheitskritische Software durchgesetzt. Wir haben drei Hauptgründe beziehungsweise Herausforderungen identifiziert: (1) fehlende Werkzeugunterstützung, (2) starre Programmentwicklung aufgrund der feinkörnigen Verfeinerungsregeln, die jeweils nur eine Programmanweisung hinzufügen (3) und fehlen eines CbC-Ansatzes zur Sicherstellung nicht-funktionaler Eigenschaften, wie z.B. der Informationsflusssicherheit.

In dieser Arbeit werden die zuvor genannten Herausforderungen adressiert, indem wir einen Correct-by-Construction-Programmentwicklungsansatz für funktional korrekte und datensichere Programme etablieren und unterstützen.
Insbesondere werden in dieser Arbeit die folgenden vier Beiträge geleistet. Als ersten Beitrag implementieren wir \corc, eine Werkzeugunterstützung für CbC. Wir bestimmen die Anforderungen, um eine korrekte Programmentwicklung mit CbC zu ermöglichen, und entwickeln eine entsprechende Werkzeugunterstützung. \corc stellt sicher, dass die Korrektheit des zu entwickelnden Programms in jedem Konstruktionsschritt gewährleistet ist.
Im zweiten Beitrag führen wir Benutzerstudien durch, um die Verständlichkeit und Benutzbarkeit von \corc zu ermitteln. In den Nutzerstudien können wir analysieren, wie Entwickler bei der Lösung von Programmieraufgaben vorgehen, welche Fehler sie machen und wie gerne sie das Werkzeug nutzen. Diese Ergebnisse werden mit der Programmentwicklung mit Post-hoc-Verifikation verglichen. Als dritten Beitrag adressieren wir den starren Programmentwicklungsansatz des klassischen CbC, indem wir neue Ansätze berücksichtigen, die eine flexiblere Programmkonstruktion ermöglichen. Wir führen neue Verfeinerungsregeln ein, die die Anwendung anderer Verfeinerungsregeln bündeln. Außerdem schlagen wir einen neuen Trait-basierten CbC-Entwicklungsansatz vor, der auf Programmkomposition anstelle von Verfeinerungsregeln basiert. Da CbC bis zu unserer Arbeit nur funktionale Korrektheit berücksichtigt hat, erweitern wir CbC in unserem vierten Beitrag, um auch einen sicheren Informationsfluss zu gewährleisten. Wir entwickeln Verfeinerungsregeln, die die Konformität des Programms mit den Informationsflusssicherheitsrichtlinien gewährleisten. Bei jedem Verfeinerungsschritt wird der Informationsfluss analysiert, um nur sichere Programmanweisungen zuzulassen. Die Verfeinerungsregeln werden in \corc integriert, um Werkzeugunterstützung für die konstruktive Entwicklung sicherer Software zu bieten, und wir demonstrieren die Praktikabilität von \corc, indem wir mehrere Fallstudien korrekt konstruieren. Insgesamt ermöglicht unsere Arbeit die Entwicklung von funktional korrekten und datensicheren Programmen mit Hilfe von Correctness-by-Construction. Auf dieser Grundlage kann festgestellt werden, ob CbC eine wirkliche Alternative zur Post-hoc-Verifikation oder Post-hoc-Analyse ist.