💻 computer science

Access Hoare Logic

Die Arbeit stellt die „Access Hoare Logic" als ein neues, von der klassischen Hoare-Logik grundlegend verschiedenes formales System zur Verifikation von Zugriffssicherheit vor, dessen Korrektheit und Vollständigkeit bewiesen sowie der Zusammenhang zu anderen Logiken wie der Incorrectness Logic aufgezeigt wird.

Ursprüngliche Autoren: Arnold Beckmann, Anton Setzer

Veröffentlicht 2026-04-01

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Arnold Beckmann, Anton Setzer

Originalarbeit lizenziert unter CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dies ist eine KI-generierte Erklärung des untenstehenden Papers. Sie wurde nicht von den Autoren verfasst oder gebilligt. Für technische Genauigkeit konsultieren Sie das Originalpaper. Vollständigen Haftungsausschluss lesen

Das große Problem: Der falsche Blickwinkel

Stell dir vor, du bist ein Sicherheitsinspektor für Computerprogramme. Bisher gab es nur eine Art, diese Programme zu prüfen: die sogenannte Hoare-Logik (erfunden von Tony Hoare).

Diese klassische Methode funktioniert wie ein Vorhersage-Tool:

Die Frage: „Wenn ich mit diesem Zustand starte (z. B. ein gültiger Schlüssel liegt auf dem Tisch), wird das Programm dann am Ende dieses Ergebnis liefern (z. B. die Tür öffnet sich)?"
Die Logik: Vorbedingung $\rightarrow$ Programm $\rightarrow$ Nachbedingung.
Das Ziel: Sicherstellen, dass das Programm korrekt funktioniert.

Aber: Das reicht nicht für Zugangssicherheit (Access Security).
Bei Zugangssicherheit wollen wir wissen: „Darf diese Person überhaupt hier reinkommen?"

Die neue Frage: „Wenn die Tür offen ist (das Ergebnis), muss dann zwingend ein gültiger Schlüssel vorhanden gewesen sein (die Voraussetzung)?"
Das Problem: Die klassische Hoare-Logik sagt uns nur, was passiert, wenn wir starten. Sie sagt uns nicht, ob der Startzustand notwendig war, um das Ergebnis zu erreichen.

Die Lösung: Access Hoare Logic (aHl)

Die Autoren (Beckmann und Setzer) haben eine neue Methode erfunden: Access Hoare Logic.

Stell dir das wie einen Rückwärts-Spürhund vor.

Klassische Logik (Vorwärts): „Ich habe einen Hund, der rennt. Wenn er hier startet, kommt er dort an."
Access Hoare Logic (Rückwärts): „Ich sehe einen Hund, der dort steht. Muss er hier gestartet sein? Oder könnte er auch von woanders gekommen sein?"

In der Access-Logik fragen wir: Ist die Vorbedingung zwingend notwendig für das Ergebnis?
Wenn das Ergebnis (z. B. Zugang gewährt) eintritt, muss dann der Startzustand (z. B. gültiger Ausweis) wahr gewesen sein? Wenn ja, ist das Programm sicher. Wenn nein (z. B. die Tür öffnet sich immer, egal ob Schlüssel da ist oder nicht), ist es unsicher.

Drei Beispiele aus dem Papier

Um das greifbar zu machen, nutzen die Autoren drei Szenarien:

1. Das Hotel mit den elektronischen Schlüsseln

Stell dir ein Hotel vor. Ein Gast bekommt eine Karte.

Szenario A (Sicher): Die Karte enthält zwei Schlüssel. Wenn der Gast die Tür öffnet, wird der alte Schlüssel im Schloss gelöscht und durch den neuen ersetzt.
- Rückwärts-Check: Wenn die Tür offen ist, muss der Gast entweder den alten oder den neuen Schlüssel gehabt haben. Das ist sicher.
Szenario B (Unsicher): Der Programmierer hat einen Fehler gemacht. Das Programm sagt: „Wenn der Schlüssel passt, öffne die Tür. Aber egal was passiert, setze am Ende Zugang = WAHR."
- Rückwärts-Check: Die Tür ist offen. Muss der Gast einen Schlüssel gehabt haben? Nein! Das Programm hat die Tür einfach so aufgemacht.
- Ergebnis: Die klassische Logik würde sagen: „Hey, die Tür geht auf, das Programm läuft!" Aber die Access Hoare Logic schreit: „Stopp! Die Vorbedingung war nicht notwendig! Das ist unsicher!"

2. Bitcoin und die digitale Kasse

Bitcoin-Transaktionen sind wie kleine Programme, die prüfen, ob du das Geld hast.

Die Aufgabe: Jemand will Bitcoins an Alice senden.
Die Prüfung: Das Programm (das „Locking Script") muss sicherstellen, dass nur jemand mit dem richtigen digitalen Fingerabdruck (Signatur) das Geld bewegen kann.
Die Anwendung: Mit Access Hoare Logic können wir beweisen: „Wenn die Transaktion erfolgreich war (Geld ist bei Alice), dann musste zwingend eine gültige Signatur vorliegen." Ohne diese Logik könnte man theoretisch beweisen, dass das Geld auch ohne Signatur transferiert werden könnte (was katastrophal wäre).

3. Die Liste der Passwörter

Stell dir ein Programm vor, das prüft, ob ein Passwort in einer Liste steht.

Die Logik: Das Programm durchsucht die Liste.
Der Trick: Wenn das Programm am Ende sagt „Zugang gewährt", muss es zwingend das Passwort in der Liste gefunden haben.
Die Access Hoare Logic hilft uns, genau diese „Notwendigkeit" mathematisch zu beweisen, damit kein Hacker durch einen Trick (z. B. einen Fehler im Schleifen-Code) Zugang bekommt, ohne das Passwort zu kennen.

Warum ist das so wichtig?

Stell dir vor, du baust eine Burg.

Die klassische Hoare-Logik prüft: „Wenn ich die Burgmauer baue, wird sie stehen bleiben?" (Korrektheit).
Die Access Hoare Logic prüft: „Wenn ich drin sitze, muss ich zwingend durch das Haupttor gekommen sein?" (Sicherheit).

Ohne Access Hoare Logic könnten wir Programme schreiben, die zufällig Zugang gewähren, ohne dass wir es merken. Mit dieser neuen Logik können wir beweisen, dass nur diejenigen rein kommen, die auch wirklich reinkommen dürfen.

Zusammenfassung in einem Satz

Die Autoren haben eine neue Art des Denkens entwickelt, die nicht fragt „Was passiert, wenn ich starte?", sondern „Was muss passiert sein, damit das Ergebnis eintritt?", um sicherzustellen, dass Computerprogramme wirklich sicher vor unbefugtem Zugriff sind.

Sie haben gezeigt, dass man diese Logik mathematisch sauber aufbauen kann (sie ist „sound" und „vollständig") und dass sie sich perfekt für moderne Technologien wie Blockchain und Smart Contracts eignet.

1. Problemstellung

Die klassische Hoare-Logik, eingeführt von Tony Hoare, ist ein etabliertes Framework zur Verifikation der Korrektheit von Programmen. Sie basiert auf Hoare-Tripeln $\{P\} C \{Q\}$ , die ausdrücken, dass eine Vorbedingung $P$ hinreichend ist, damit nach der Ausführung des Programms $C$ die Nachbedingung $Q$ gilt (sofern das Programm terminiert). Das Ziel ist hier die Vorwärtsrichtung: Von $P$ zu $Q$ .

Das Paper identifiziert jedoch eine Lücke bei der Verifikation von Zugriffssicherheit (Access Security), insbesondere im Kontext von Zugriffskontrolle (Access Control) und Blockchain-Smart Contracts. Bei Zugriffssicherheit geht es nicht darum, zu garantieren, dass ein gewünschtes Ergebnis erreicht wird, wenn bestimmte Bedingungen erfüllt sind. Stattdessen muss garantiert werden, dass ein bestimmter Zustand (z. B. der Zugriff auf eine Ressource) nur dann erreicht wird, wenn spezifische Voraussetzungen vor der Ausführung erfüllt waren.

Das Problem besteht darin, dass die Standard-Hoare-Logik die Notwendigkeit der Vorbedingung nicht direkt ausdrückt. Für Zugriffssicherheit ist die logische Richtung umgekehrt: Wenn das Programm in einem Zustand endet, der die Nachbedingung erfüllt, muss die Vorbedingung bereits vorher erfüllt gewesen sein. Dies erfordert eine Rückwärtslogik (von Post- zu Pre-Conditions), die mit den Standardwerkzeugen der Hoare-Logik nicht intuitiv oder effizient abbildbar ist.

2. Methodik

Die Autoren führen eine neue formale Methode ein, die sie Access Hoare Logic (aHl) nennen.

Access Hoare Tripel: Anstelle des klassischen Tripels $\{P\} C \{Q\}$ ${P} C {Q}$ definieren sie das Access Hoare Tripel $\langle P \rangle C \langle Q \rangle$ $⟨ P ⟩ C ⟨ Q ⟩$ .
- Semantik: $\forall s, s' [s \xrightarrow{C} s' \land Q(s') \to P(s)]$ .
- Dies bedeutet: Wenn die Ausführung von $C$ von einem Zustand $s$ zu einem Zustand $s'$ führt, in dem $Q$ gilt, dann muss $P$ im Zustand $s$ bereits gegolten haben. $P$ ist also eine notwendige Bedingung für $Q$ .
Kalkül-Design: Die Autoren entwickeln einen direkten Kalkül für aHl, der dem der Hoare-Logik ähnelt, aber signifikante Unterschiede in den Regeln aufweist, um der Rückwärtsrichtung gerecht zu werden:
- Konsequenzregel: Im Gegensatz zur Hoare-Logik (wo man die Vorbedingung stärken und die Nachbedingung schwächen kann), erlaubt aHl das Abschwächen der Vorbedingung und das Stärken der Nachbedingung. Dies spiegelt wider, dass wir die minimal notwendigen Bedingungen suchen.
- Bedingte Anweisungen (If-Else): Die Regeln für if B then S else T ändern sich von Konjunktionen zu Implikationen. Die Vorbedingung für den then-Zweig wird zu $B \to P$ , und für den else-Zweig zu $\neg B \to P$ .
- Schleifen (While): Die Regel für while B do S verwendet eine Invariante $P$ , wobei die Nachbedingung des Schleifenkörpers auf Zustände beschränkt ist, die $\neg B$ erfüllen.
Vermeidung von Negation: Obwohl ein Tripel $\langle P \rangle C \langle Q \rangle$ äquivalent zu $\{\neg P\} C \{\neg Q\}$ ist (Theorem 3.1), lehnen die Autoren eine Reduktion auf die Standard-Hoare-Logik über Negation ab. Dies liegt daran, dass die Umwandlung von Implikationen in ihre Kontraposition ( $\neg B \to \neg A$ statt $A \to B$ ) die Verifizierung erschwert, insbesondere in intuitionistischen Theorembeweisern (wie Coq), die in der Praxis häufig eingesetzt werden.

3. Wichtige Beiträge

Formale Definition von Access Hoare Logic: Einführung des Tripels $\langle P \rangle C \langle Q \rangle$ und eines zugehörigen Kalküls mit Axiomen und Inferenzregeln.
Korrektheitsbeweise (Soundness & Completeness):
- Soundness: Es wird bewiesen, dass alle im Kalkül ableitbaren Tripel semantisch gültig sind.
- Completeness: Es wird gezeigt, dass jedes semantisch gültige Tripel im Kalkül beweisbar ist. Dies geschieht durch die Konstruktion der stärksten Vorbedingung ( $P_s$ ) und den Nachweis, dass diese ableitbar ist.
Beziehung zur Standard-Hoare-Logik:
- Die Autoren zeigen, dass für terminierende Programme die stärkste Vorbedingung (Strongest Pre-Condition) der Access Hoare Logik identisch mit der schwächsten Vorbedingung (Weakest Pre-Condition) der Standard-Hoare-Logik ist, wenn man die Menge der Zustände betrachtet, in denen das Programm terminiert.
- Dies stellt eine theoretische Brücke zwischen den beiden Logiken her.
Unterscheidung zu Incorrectness Logic: Das Paper grenzt aHl von der „Incorrectness Logic" (die Unterapproximationen für Fehleranalyse nutzt) ab. Während Incorrectness Logic eine komplementäre Sichtweise im Kontext von Vorwärts-Transformern bietet, ist aHl die komplementäre Sichtweise im Kontext von Rückwärts-Transformern.
Anwendungsbeispiele:
- Elektronische Schlüsselsysteme: Analyse von Hotel-Türschlössern, um zu zeigen, dass eine bestimmte Programmstruktur (P1) Zugriffssicherheit garantiert, während eine andere (P2), die in der Standard-Hoare-Logik korrekt wäre, dies nicht tut.
- Bitcoin Smart Contracts: Formale Verifikation des scriptPubKeyP2PKH Skripts, um sicherzustellen, dass ein Zugriff auf Bitcoins nur möglich ist, wenn eine gültige Signatur und Adresse vorliegen.
- Schleifen-basierte Zugriffskontrolle: Verifikation eines Programms, das den Zugriff gewährt, wenn ein Schlüssel in einer Liste gefunden wird.

4. Ergebnisse

Der Kalkül der Access Hoare Logic ist sound und vollständig unter einer allgemeinen semantischen Interpretation.
Es wurde nachgewiesen, dass die direkte Behandlung von Zugriffssicherheit durch aHl effizienter und intuitiver ist als die Umwandlung in Standard-Hoare-Logik durch Negation, da letztere die Verifizierung in intuitionistischen Systemen brechen oder erschweren kann.
Die Analyse der Beispiele zeigt, dass Programme, die in der Standard-Hoare-Logik als „korrekt" gelten (weil sie eine Nachbedingung erreichen, wenn eine Vorbedingung erfüllt ist), in der Access Hoare Logic als unsicher entlarvt werden können, wenn die Vorbedingung nicht notwendig für das Erreichen der Nachbedingung ist (z. B. wenn das Programm die Nachbedingung auch ohne die Vorbedingung erreicht).

5. Bedeutung und Ausblick

Die Arbeit ist von großer Bedeutung für die Sicherheit von Software, insbesondere in Bereichen wie Blockchain, Smart Contracts und verteilten Systemen, wo Zugriffskontrolle eine zentrale Rolle spielt.

Praktische Relevanz: Sie bietet ein Werkzeug, um Sicherheitsanforderungen („Zugriff darf nur unter Bedingung X gewährt werden") formal zu verifizieren, was mit herkömmlichen Korrektheitsbeweisen oft nicht direkt möglich ist.
Theoretischer Fortschritt: Sie erweitert das Spektrum der formalen Verifikation um eine dedizierte Logik für Sicherheitsanforderungen, die auf der Notwendigkeit statt auf der Hinlänglichkeit basiert.
Zukunft: Die Autoren deuten an, dass viele Aspekte der Hoare-Logik (Syntax, Axiomatisierung, Predicate Transformer Semantik) nun im Kontext von aHl neu untersucht werden müssen. Zudem wird auf ein Patent zur Verifikation von Zugriffssicherheit verwiesen, das auf diesen Erkenntnissen aufbaut.

Zusammenfassend etabliert das Paper die Access Hoare Logic als notwendiges und formales Fundament, um Zugriffssicherheit in Programmen rigoros zu beweisen, indem es die logische Richtung der Verifikation von „Vorbedingung $\to$ Nachbedingung" auf „Nachbedingung $\to$ Notwendige Vorbedingung" umkehrt.