Formale Verifikation und Beweisassistenten

Die formale Verifikation stellt durch maschinell überprüfte mathematische Beweise sicher, dass Software ihre Spezifikation erfüllt; Beweisassistenten sind die Werkzeuge, die solche Beweise erstellen und überprüfen.

Definition

Formale Verifikation ist die Konstruktion eines rigorosen, maschinell überprüften Beweises, dass ein System eine formale Spezifikation erfüllt, und ein Beweisassistent ist eine Software, die einen Benutzer bei der Entwicklung solcher Beweise unterstützt und deren Gültigkeit mechanisch überprüft.

Scope

Dieses Thema behandelt deduktive Verifikation und interaktives Theorembeweisen: Beweisassistenten, die auf Typentheorie oder Logik höherer Ordnung basieren (wie Coq, Isabelle, Lean und Agda), den LCF-Ansatz für vertrauenswürdige Beweise, die Grundlage der Propositionen-als-Typen, Beweisautomatisierung und Taktiken sowie wegweisende verifizierte Artefakte einschließlich Compiler und Betriebssystemkerne.

Core questions

• Wie kann die vollständige funktionale Korrektheit bewiesen und maschinell überprüft werden?
• Warum sind Beweisassistenten vertrauenswürdig, und was ist die vertrauenswürdige Rechenbasis?
• Wie verbindet die Curry-Howard-Korrespondenz Beweise und Programme?
• Was ist erforderlich, um reale Systeme wie Compiler und Kerne zu verifizieren?

Key theories

LCF-Ansatz für vertrauenswürdige Beweise

Gordons, Milners und Wadsworths Edinburgh LCF führte einen kleinen vertrauenswürdigen Beweiskernel ein, durch den alle Theoreme passieren müssen, sodass selbst komplexe Automatisierung keine fehlerhaften Beweise erzeugen kann.

Verifizierter Compiler (CompCert)

Leroys CompCert ist ein C-Compiler, dessen Korrektheit in einem Beweisassistenten bewiesen wurde, mit einem maschinell überprüften Theorem, dass der generierte Code die Semantik des Quellprogramms verfeinert.

Verifizierter Betriebssystemkern (seL4)

Klein und Kollegen erstellten einen maschinell überprüften Beweis der funktionalen Korrektheit für den seL4-Mikrokernel und demonstrierten damit eine End-to-End-Verifikation von Low-Level-Systemsoftware.

Clinical relevance

Die mechanisierte Verifikation bietet die höchste verfügbare Sicherheit für kritische Software, indem sie Compiler, Kerne und kryptografische Bibliotheken mit nachgewiesenen Garantien anstelle von testbasiertem Vertrauen produziert. Beweisassistenten werden auch zunehmend zur Formalisierung der Mathematik selbst eingesetzt.

History

Das interaktive Theorembeweisen begann in den 1970er Jahren mit Edinburgh LCF, dessen ML-Metasprache und vertrauenswürdiger Kernel spätere Systeme prägten. Typentheorie-basierte Assistenten wie Coq und Agda sowie Systeme der Logik höherer Ordnung wie Isabelle/HOL entwickelten sich in den folgenden Jahrzehnten weiter und mündeten in wegweisende verifizierte Artefakte: den CompCert-Compiler (2009) und den seL4-Kernel (2009).

Debates

Kosten der Verifikation versus gewonnene Sicherheit

Der Aufbau maschinell überprüfter Beweise großer Systeme erfordert enormen Aufwand, was zu Debatten darüber führt, wo eine vollständige Verifikation gerechtfertigt ist, wo leichtere Methoden ausreichen und wie viel Beweis automatisiert werden kann.

Key figures

• Robin Milner
• Michael Gordon
• Xavier Leroy
• Gerwin Klein
• Robert Harper

Seminal works

• gordon1979
• leroy2009
• klein2009
• harper2016

Frequently asked questions

Was ist ein Beweisassistent?

Ein Beweisassistent ist eine Software, in der ein Benutzer interaktiv formale Beweise konstruiert, während das System jeden Schritt mechanisch überprüft, sodass ein abgeschlossener Beweis bis zu einem kleinen, gut überprüften Kernel vertrauenswürdig ist.

Wie unterscheidet sich die Verifikation eines Programms vom Testen?

Das Testen überprüft das Verhalten bei ausgewählten Eingaben und kann nur das Vorhandensein von Fehlern aufzeigen, während die formale Verifikation die Korrektheit für alle durch die Spezifikation erlaubten Eingaben beweist und das Fehlen der spezifizierten Fehler feststellt.