Correctness-by-Construction (CbC) ist ein Ansatz zur inkrementellen Erstellung korrekter Programme. CbC beginnt mit einem abstrakten Hoare-Tripel {P} S {Q}, das aus einer Vorbedingung P, einer abstrakten Anweisung S und einer Nachbedingung Q besteht. Hoare-Tripel stellen vollständige Korrektheitsaussagen dar, die nur dann als wahr bewertet werden, wenn, ausgehend von der Vorbedingung, die Nachbedingung nach Ausführung des schließlich definierten konkreten Programms erfüllt ist. Bei CbC wird das Hoare-Tripel mit Hilfe einer Menge von Verfeinerungsregeln sukzessive zu einer konkreten Implementierung verfeinert, die die Spezifikation erfüllt. Die Korrektheit ist garantiert, da jede Verfeinerungsregel als solide bewiesen ist und die Korrektheit des Programms bewahrt. CbC ist in dem Werkzeug CorC implementiert. CorC ist eine grafische und textuelle IDE zur Konstruktion von Algorithmen nach dem Correctness-by-Construction-Ansatz. Es unterstützt CbC-Entwickler dabei, ein Programm durch eine Abfolge von Verfeinerungsschritten zu verfeinern und die Korrektheit dieser Verfeinerungsschritte mit Hilfe eines Theoremprüfers zu verifizieren.

Informationsflusskontrolle durch Konstruktion

Neben der Verifikation der funktionalen Korrektheit können Verfeinerungsregeln auch zur Gewährleistung der Sicherheit von Programmen eingesetzt werden. Eine Informationsfluss-Policy definiert, wie Informationen in einem Programm fließen dürfen (z.B. ist ein Fluss von öffentlichen zu geheimen Daten erlaubt, aber der andere Weg ist verboten). Die Erweiterung von CbC zur Gewährleistung der Sicherheit wird als Information Flow Control-by-Construction (IFbC) bezeichnet. Programme werden inkrementell unter Verwendung von Verfeinerungsregeln konstruiert, um einer Informationsfluss-Policy zu folgen. In jedem Verfeinerungsschritt wird die Sicherheit und funktionale Korrektheit des Programms garantiert, so dass unsichere Programme durch Konstruktion verhindert werden. Die Informationsfluss-Policy kann in einem beliebigen begrenzten oberen Semilattice spezifiziert werden (d. h. die Sicherheitsstufen sind in einer teilweise geordneten Menge angeordnet, die die zulässige Richtung des Informationsflusses darstellt). IFbC ist in einer Erweiterung von CorC implementiert.

Correctness-by-Construction für Software-Produktlinien

Software-Produktlinien bieten eine systematische Wiederverwendung von Software und anderen Artefakten, gepaart mit Variabilitätsmechanismen im Code, um ganze Produktfamilien und nicht nur einzelne Softwareprodukte zu implementieren. Die Gemeinsamkeiten und Unterschiede der einzelnen Varianten werden als Features kommuniziert, deren Beziehungen oft in Feature-Modellen modelliert werden. Die Gewährleistung der Korrektheit einer Produktlinie ist aufgrund der Anzahl möglicher Varianten, die sich aus der Anzahl der Feature-Konfigurationen und der variablen Codestrukturen ergeben, eine besondere Herausforderung. Um eine korrekte Produktlinie mit CbC zu erstellen, haben wir daher den ursprünglichen CbC-Ansatz um eine neue Verfeinerungsregel für einen Variabilitätsmechanismus in den Aussagen des Hoare-Tripels erweitert und mit einer Vertragskomposition für Variabilität in der Vor- und Nachbedingung kombiniert. Wir nennen diese Erweiterung Variational Correctness-by-Construction. VarCorC verwendet FeatureIDE und variationales CbC, um die Entwicklung von Correctness-by-Construction Software-Produktlinien zu unterstützen.

Publikationen

• M. Kodetzki, T. Bordis, T. Runge, and I. Schaefer. Partial Proofs to Optimize Deductive Verification of Feature-Oriented Software Product Lines. In 18th International Working Conference on Variability Modelling of Software-Intensive Systems (VaMoS'24), 2024.
• T. Runge, T. Bordis, A. Potanin, T. Thüm, and I. Schaefer. Flexible Correct-by-Construction Programming. In Logical Methods in Computer Science, Volume 19, 2023.
• T. Runge. Correctness-by-Construction for Correct and Secure Software Systems. Dissertation, 2023.
• T. Runge, M. Servetto, A. Potanin, and I. Schaefer. Immutability and Encapsulation for Sound OO Information Flow Control. In ACM Transactions on Programming Languages and Systems, Volume 45, 2023.
• T. Runge, A. Potanin, T. Thüm, and I. Schaefer. Traits for Correct-by-Construction Programming. In CoRR 2022.
• T. Bordis, T. Runge, D. Schultz, and I.Schaefer. Family-Based and Product-Based Development of Correct-by-Construction Software Product Lines. In Journal of Computer Languages (COLA), 2022.
• T. Bordis, L. Cleophas, A. Kittelmann, T. Runge, I. Schaefer, and B. W. Watson. Re-CorC-ing KeY: Correct-by-Construction Software Development Based on KeY. In The Logic of Software. A Tasting Menu of Formal Methods, 2022.
• T. Runge, A. Potanin, T. Thüm, and I. Schaefer. Traits: Correctness-by-Construction for Free. In FORTE 2022.
• A. Kittelmann, T. Runge, T. Bordis, and I. Schaefer. Runtime Verification of Correct-by-Construction Driving Maneuvers. ISoLA 2022.
• T. Bordis, M. Kodetzki, T. Runge, and I. Schaefer. VarCorC: Developing Object-Oriented Software Product Lines Using Correctness-by-Construction. In SEFM Workshops, 2022.
• T. Runge, A. Kittelmann, M. Servetto, A. Potanin, and I. Schaefer. Information Flow Control-by-Construction for an Object-Oriented Language. SEFM 2022.
• I. Schaefer, T. Runge, L. Cleophas, and B. W. Watson. Tutorial: The Correctness-by-Construction Approach to Programming Using CorC. SecDev, 2021.
• T. Runge, T. Bordis, T. Thüm, and I. Schaefer. Teaching Correctness-by-Construction and Post-hoc Verification - The Online Experience. FMTea, 2021.
• T. Bordis, T. Runge, and I. Schaefer. Correctness-by-Construction for Feature-Oriented Software Product Lines. In GPCE, 2020.
• T. Runge, A. Knüppel, T. Thüm, and I. Schaefer. Lattice-Based Information Flow Control-by-Construction for Security-by-Design. In FormaliSE, 2020.
• A. Knüppel, T. Runge, and I. Schaefer. Scaling Correctness-by-Construction. ISoLA, 2020.
• T. Bordis, T. Runge, A. Knüppel, T. Thüm, and I. Schaefer. Variational Correctness-by-Construction. In 14th International Working Conference on Variability Modelling of Software-Intensive Systems (VaMoS'20), 2020.
• T. Runge, T. Thüm, L. Cleophas, I. Schaefer, and B. W. Watson: Comparing Correctness-by-Construction with Post-Hoc Verification - A Qualitative User Study. In REFINE, 2019.
• T. Runge, I. Schaefer, L. Cleophas, T. Thüm, D. G. Kourie, and B. W. Watson: Tool Support for Correctness-by-Construction, Proc. of the International Conference on Fundamental Approaches to Software Engineering (FASE), Springer, 2019.
• T. Runge, I. Schaefer, A. Knüppel, L. Cleophas, D. G. Kourie, and B. W. Watson: Tool support for Confidentiality by Construction. In HILT 2018 Workshop on Languages and Tools for Ensuring Cyber-Resilience in Critical Software-Intensive Systems (HILT'18), 2018.
• I. Schaefer, T. Runge, A. Knüppel, L. Cleophas, D. G. Kourie, and B. W. Watson: Towards Confidentiality-by-Construction. In International Symposium on Leveraging Applications of Formal Methods, Springer, 2018.