Abstrakte Techniken für Programmiersprachen und sichere Kompilierung

• Antragsteller: Privatdozent Dr.-Ing. Sergey Goncharov; Dr. Stelios Tsampas
• Fachliche Zuordnung: Softwaretechnik und Programmiersprachen ; Theoretische Informatik
• Förderung: Förderung seit 2023
• Projektkennung: Deutsche Forschungsgemeinschaft (DFG) - Projektnummer 527481841

Schlussfolgern über imperative und höherstufige Programmiersprachen im Rahmen von Sicherheit und Verifikation ist eine hochkomplexe Aufgabe, die durch die Berücksichtigung abstrakter allgemeiner Eigenschaften wie Kompositionalität, Adäquatheit und vollständige Abstraktion vereinfacht werden kann. Diese Eigenschaften sind jedoch in der Praxis selbst sehr schwierig zu etablieren. Darüber hinaus sind ihre Beweise in der Regel sprachspezifisch, und geringfügige Modifikationen der Syntax, der Sprachmerkmale oder des Begriffs von beobachtbarem Verhalten und Programmäquivalenz erfordern einen neuen Beweis. In ATLaS werden wir auf dem kürzlich entwickelten Begriff des abstrakten höherstufigen GSOS aufbauen, um ein integriertes Rahmenwerk für die Semantik von imperativen und höherstufigen Sprachen mit Anwendungen zur Verifikation von sicheren Compilern zu entwickeln. Abstraktes höherstufiges GSOS ist eine Verallgemeinerung des bekannten erststufigen Gegenstücks von Turi und Plotkin. Ein erstes grundlegendes Ergebnis zeigt, dass jede in abstraktem höherstufigem GSOS spezifizierte Sprache in Bezug auf starke Varianten der applikativen Bisimilarität von Abramsky kompositional ist. Eines unserer Ziele in ATLaS besteht darin, die volle Leistungsfähigkeit des Rahmenwerks zu entfalten. Konkret wollen wir zunächst die Call-by-Value-Auswertungsstrategie mit abstraktem höherstufigem GSOS in Einklang bringen und zu diesem Zweck eine vereinheitlichende Metasprache definieren. Anschließend werden wir schwächere Begriffe von Programmäquivalenz in abstraktem höherstufigem GSOS untersuchen, insbesondere die schwache applikative Bisimilarität. Zu diesem Zweck streben wir die Entwicklung einer kategorischen Verallgemeinerung der Methode von Howe an. Ein weiteres Ziel ist die Erweiterung des Rahmenwerks auf Sprachen mit Typen und mit Seiteneffekten wie Wahrscheinlichkeit, Nichtdeterminismus und Speicher. Als wichtige und komplexe Instanz werden wir uns speziell mit Prägarben-Modellen der dynamischen Speicherzuweisung befassen, die von der abstrakten, axiomatischen Natur unseres Ansatzes besonders profitieren sollten. In ATLaS legen wir besonderen Wert auf die Formalisierung unserer Ergebnisse im Beweisassistenten Agda; dies wird Wiederverwendbarkeit und eine formale Absicherung der Korrektheit sowie die Übereinstimmung mit den Grundprinzipien der Typentheorie gewährleisten. Der wichtigste Anwendungsbereich für unsere Entwicklungen ist das aufstrebende Gebiet der sicheren Kompilierung, das sich mit Compilern mit beweisbaren Sicherheitseigenschaften, etwa der Abwesenheit von Pufferüberläufen und Speicherlecks, befasst. Hierzu werden wir Sicherheitseigenschaften von Sprachen in abstraktem GSOS modellieren und abstraktionserhaltende, d.h. sichere Compiler, mit dem formalen Begriff eines Morphismus von abstrakten GSOS-Spezifikationen in Verbindung bringen.

• DFG-Verfahren: Sachbeihilfen