Correctness-by-Construction for Pancake Programs

In sicherheitskritischen Umgebungen werden häufig Betriebssysteme eingesetzt. Daher müssen sie strikte Anforderungen an ihre funktionale Korrektheit erfüllen, was sie zu einem geeigneten Ziel für die Anwendung formaler Techniken macht, beispielsweise für formale Verifikation. Bestehende Forschungsarbeiten, zum Beispiel die Arbeiten zum seL4-Mikrokernel, zeigen, dass die Verifikation von Systemsoftware zeitaufwändig und kostspielig ist. Die Systemprogrammiersprache Pancake geht dieses Problem durch ihr Sprachdesign an, das einen verifizierten Compiler umfasst, der auf einer im interaktiven Theorembeweiser HOL4 formalisierten Semantik basiert.
... mehr

Die bestehenden formalen Techniken für Systemprogrammiersprachen beschränken sich jedoch auf Post-Hoc-Ansätze, das heißt die Verifikation einer abgeschlossenen Implementierung gegen eine Spezifikation. Da diese Spezifikation in der Regel bereits vor der Implementierung bekannt ist, besteht hier Verbesserungspotenzial. Im Gegensatz zu Post-Hoc-Ansätzen nutzen Refinement-basierte Techniken wie Correctness-by-Construction (CbC) dieses Wissen, indem sie die Spezifikation als Ausgangspunkt für korrektheitserhaltende Refinement-Schritte verwenden, was zu einem Programm führt, das die ursprüngliche Spezifikation a priori erfüllt. Die Refinement-Schritte in CbC bestehen in der benutzergeführten Anwendung formal bewiesener Refinement-Regeln, welche die Auswahl korrekter Refinement-Schritte vereinfachen.

In dieser Arbeit stellen wir einen CbC-Kalkül für eine Turing-vollständige Teilmenge der Systemprogrammiersprache Pancake vor, der es Entwicklern ermöglicht, Pancake-Programme zu implementieren, indem sie eine Hoare-Spezifikation unter Verwendung von 26 Refinement-Regeln zu einem Pancake-Programm zu verfeinern. Unser CbC-Kalkül ist in HOL4 implementiert und nutzt die formale Semantik von Pancake, um beweisbare Ende-zu-Ende-Korrektheit zu erreichen. Um die Machbarkeit unseres Ansatzes zu zeigen, präsentieren wir eine Implementierung der linearen Suche als Fallstudie sowie einen Ansatz zur Automatisierung der Refinement-Beweise.

In safety-critical environments, operating systems are commonly used. Therefore, they need to satisfy strict requirements on their functional correctness, making them a suitable target for the application of formal techniques, such as formal verification. Existing research on the verification of systems software, e.g., work on the seL4 microkernel, shows that this process is time consuming and expensive. The systems programming language Pancake addresses this issue through its language design, featuring a verified compiler, based on a semantics formalized in the interactive theorem prover HOL4.
... mehr

However, existing formal techniques for systems programming languages are limited to post-hoc approaches, i.e., the verification of a completed implementation against a specification. Since this specification is typically known before implementation, there is potential for improvement. In contrast to post-hoc approaches, refinement-based techniques like Correctness-by-Construction (CbC) exploit this knowledge by using the specification as the origin for correctness-preserving refinement steps, resulting in a program which fulfills the initial specification a priori. The refinement steps in CbC consist of the user-guided application of proven-correct refinement rules which simplify selecting correct refinement steps.

In this thesis, we introduce a CbC calculus for a Turing-complete subset of the systems programming language Pancake which allows developers to implement Pancake programs by refining a Hoare-style specification into programs using a set of 26 refinement rules. Our CbC calculus is implemented in HOL4, leveraging the formal semantics of Pancake to achieve provable end-to-end correctness. To demonstrate the feasibility of our approach, we present an implementation of linear search as a case study as well as an approach to automate the refinement proofs.