💻 computer science

Language-based Security and Time-inserting Supervisor

Diese Arbeit verwendet algebraische Methoden, um sprachbasierte Sicherheitseigenschaften zu definieren, und schlägt einen zeit-einfügenden Supervisor vor, der unter den Bedingungen unvollständiger Information für sowohl den Supervisor als auch den Angreifer die Prozesssicherheit gewährleistet, indem er unerwünschte Aktionen deaktiviert oder zeitgesteuerte Ereignisse einfügt, während er gleichzeitig die Existenz und die Grenzen eines solchen Supervisors analysiert.

Ursprüngliche Autoren: Damas P. Gruska

Veröffentlicht 2026-07-01

📖 5 Min. Lesezeit🧠 Tiefgang

CC BY 4.0

Ursprüngliche Autoren: Damas P. Gruska

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

Stellen Sie sich vor, Sie leiten einen Hochsicherheits-Banktresors. Sie haben eine strikte Regel: Niemand darf jemals erraten können, welche spezifische Kombination von Tasten gedrückt wurde, um den Tresor zu öffnen. Dies ist das Konzept der Opazität: Das „Geheimnis“ (der spezifische Pfad, der genommen wurde) vor einem Beobachter verborgen zu halten.

Normalerweise haben Sie bei einem unsicheren System zwei Möglichkeiten:

Den Tresor neu bauen: Das gesamte System so umgestalten, dass es von vornherein sicher ist. (Dies ist teuer, schwierig und oft unmöglich, wenn die Maschine bereits gebaut ist).
Einen Wachmann (Supervisor) einstellen: Einen Wachmann vor den Tresor stellen, der die Tasten beobachtet. Wenn er sieht, dass jemand eine „schlechte“ Taste drücken will, stoppt der Wachmann ihn.

Das Problem mit traditionellen Wachmännern:
Das Paper weist auf einen Fehler im „Wachmann“-Ansatz hin. Einige Angriffe beziehen sich nicht darauf, welche Tasten gedrückt werden, sondern wie schnell sie gedrückt werden. Dies wird als Timing-Attacke bezeichnet.

Beispiel: Wenn der Tresor 2 Sekunden braucht, um sich bei dem Code „1-2-3“ zu öffnen, aber nur 1 Sekunde bei dem Code „1-2-4“, muss ein Hacker nicht sehen, welche Tasten gedrückt werden. Er braucht nur eine Stoppuhr. Die Geschwindigkeit selbst verrät das Geheimnis.
Ein traditioneller Wachmann, der nur „Stopp!“ oder „Go!“ sagen kann, kann dies nicht beheben. Wenn er den Prozess stoppt, öffnet sich der Tresor nicht. Wenn er ihn gewähren lässt, verrät die Geschwindigkeit dennoch das Geheimnis.

Die Lösung des Papers: Der „aktive“ Wachmann
Der Autor, Damas P. Gruska, schlägt eine neue Art von Wachmann vor, den Aktiven Supervisor. Dieser Wachmann besitzt eine Superkraft: Zeitmanipulation.

Stellen Sie sich diesen Wachmann nicht nur als Türsteher vor, sondern als DJ oder Verkehrsleiter, der zwei Dinge tun kann:

Das Auto blockieren: Eine bestimmte Aktion stoppen, wenn sie gefährlich ist (wie ein traditioneller Wachmann).
Eine rote Ampel setzen: Wenn das Auto sicher fährt, aber zu schnell ist (was ein Geheimnis verrät), kann der Wachmann eine künstliche „Pause“ oder eine „Verzögerung“ einfügen, um alles zu verlangsamen.

Durch das Hinzufügen dieser künstlichen Pausen lässt der Wachmann den „schnellen“ geheimen Pfad genauso langsam erscheinen wie den „langsamen“ öffentlichen Pfad. Für den Hacker mit der Stoppuhr sehen beide Pfade identisch aus. Das Geheimnis bleibt gewahrt.

Der Haken: Der Wachmann ist blind
Hier kommt der knifflige Teil, den das Paper untersucht: Der Wachmann sieht nicht alles.

Der Hacker hat eine Brille, mit der er einige Dinge sehen kann, aber nicht alle.
Der Wachmann hat eine andere Brille. Vielleicht sieht der Wachmann weniger als der Hacker, oder er sieht vielleicht ganz andere Dinge.
Der Wachmann muss Entscheidungen basierend auf dieser verschwommenen, unvollständigen Sichtweise treffen.

Das Paper stellt die Frage: Können wir immer einen Wachmann finden, der das Sicherheitsproblem angesichts dieser Einschränkungen lösen kann?

Die Ergebnisse (Die „Ja, Nein und Vielleicht“-Liste)
Der Autor verwendet komplexe Mathematik (wie ein sehr fortgeschrittenes Regelbuch für die Denkweise von Maschinen), um herauszufinden, wann dies möglich ist:

Die „unmögliche“ Zone: Manchmal lautet die Antwort Nein. Wenn der Wachmann zu blind ist (er kann die gefährlichen Aktionen nicht kommen sehen) und die Maschine zu komplex ist (wie eine Turing-Maschine, die so intelligent wie ein Computer ist), gibt es keine Möglichkeit zu garantieren, dass das Geheimnis sicher bleibt. Es ist mathematisch bewiesen, dass kein Algorithmus dies für jedes mögliche Szenario lösen kann.
Die „machbare“ Zone: Wenn das System einfacher ist (wie eine endliche Menge von Zuständen, vergleichbar mit einer einfachen Ampelschaltung) und die Regeln klar sind, können wir mathematisch beweisen, dass ein Wachmann existiert, und ihn sogar konstruieren.
Der „perfekte“ Wachmann: Das Paper versucht, den „besten“ Wachmann zu finden – einen, der das System so wenig wie möglich einschränkt. Wir wollen, dass der Tresor so schnell wie möglich öffnet und nur dann Verzögerungen hinzufügt, wenn es absolut notwendig ist. Das Paper zeigt, wie man einen solchen „maximalen“ Wachmann in einfacheren Systemen findet.

Die große Metapher
Stellen Sie sich ein Spiel wie „Flüstern durch die Reihe“ vor, bei dem eine geheime Nachricht weitergegeben wird.

Der Angreifer hört dem Flüstern zu.
Das System ist die Reihe von Menschen, die die Nachricht weitergeben.
Die Timing-Attacke ist, wenn der Angreifer bemerkt, dass die Menschen schneller flüstern, wenn die Nachricht „Geheim“ ist als wenn sie „Öffentlich“ ist.
Der Aktive Supervisor ist ein Schiedsrichter, der in der Reihe steht. Der Schiedsrichter kann nicht alles perfekt hören, kann aber die Leute auf die Schulter klopfen, um sie für eine Sekunde innehalten zu lassen.
Das Ziel: Der Schiedsrichter klopft die „schnellen“ Flüsterer gerade so weit an, dass alle die exakt gleiche Zeit benötigen, um die Nachricht weiterzugehen. Der Angreifer kann durch das Timing nicht mehr unterscheiden, ob die Nachricht „Geheim“ oder „Öffentlich“ war.

Zusammenfassung
Dieses Paper führt eine neue Art vor, Computersysteme vor „Timing-Attacken“ (bei denen die Geschwindigkeit ein Geheimnis verrät) zu schützen. Anstatt nur schlechte Aktionen zu blockieren, schlägt es einen intelligenten Controller vor, der auch künstliche Verzögerungen einfügen kann, um das Timing zu verbergen. Das Paper nutzt schwere Mathematik, um genau zu bestimmen, wann dies möglich ist und wann es unmöglich ist, abhängig davon, wie viel der Controller sieht und wie komplex das System ist.

Technisches Resümee: Aktive supervisory Kontrolle zur Erhaltung der Opazität

Problemstellung

Das moderne System Engineering stützt sich zunehmend auf formale Methoden zur Verifizierung von Sicherheit. Wenn jedoch festgestellt wird, dass ein System unsicher ist, erweist sich eine grundlegende Neugestaltung oft als prohibitiv kostspielig oder unmöglich, insbesondere bei Legacy-Systemen oder eingebetteten Systemen. Die klassische Theorie der supervisory Kontrolle adressiert dies durch die dynamische Einschränkung der Systemausführungspfade, indem sie kontrollierbare Aktionen ermöglicht oder deaktiviert, um Sicherheits- oder Schutzrichtlinien durchzusetzen. Dieser klassische Paradigma der Aktionsbeschränkung ist jedoch unzureichend gegenüber Timing-Angriffen, einer bedeutenden Klasse von Seitenkanalangriffen, bei denen Angreifer sensible interne Daten durch das Messen von Variationen in der Ausführungs- und Antwortzeit erschließen.

In solchen Szenarien reicht das bloße Blockieren von Aktionen nicht aus, da das Tempo der Ereignisse selbst kritische Informationen preisgibt. Um diese Schwachstellen zu mildern, müssen Systeme das zeitliche Verhalten manipulieren, oft durch das Einfügen künstlicher Zeitverzögerungen, um temporale Varianzen zu glätten. Darüber hinaus konzentrierte sich die bestehende Forschung zur Opazität (eine sprachbasierte Sicherheitseigenschaft, die sicherstellt, dass Geheimnisse vor Beobachtern verborgen bleiben) weitgehend auf endliche Automaten oder zustandsbasierte Modelle. Diese Arbeit adressiert die Lücke bei der Handhabung von sprachbasierter Opazität innerhalb eines Timed Process Algebra (TPA) Frameworks, speziell für Systeme, die Turing-Maschinen äquivalent sind, wobei weder der Supervisor noch der Angreifer über vollständige Informationen über das Verhalten des Systems verfügen.

Methodik

Die Arbeit verwendet ein Timed Process Algebra (TPA) Framework, eine Erweiterung des Calculus of Communicating Systems (CCS) von Milner. TPA führt eine diskrete Zeitaktion ( $t$ ) ein, um das Verstreichen von Zeit zu modellieren, was die formale Darstellung von Timing-Angriffen und Informationslecks ermöglicht.

Kernkonzepte

Opazität und Beobachtungsfunktionen:
- Opazität ist definiert als die Eigenschaft, dass für jeden Pfad (Trace), der ein Geheimnisprädikat $\phi$ erfüllt, ein anderer Pfad existiert, der $\phi$ nicht erfüllt und unter einer spezifischen Beobachtungsfunktion $O$ ununterscheidbar ist.
- Die Arbeit formalisiert verschiedene Beobachtungsfunktionen ( $O$ $O$ ), um unterschiedliche Fähigkeiten von Angreifern zu modellieren:
  - Statisch: Aktionen werden unabhängig vom Kontext beobachtet.
  - Dynamisch: Die Beobachtung einer Aktion hängt von der Historie der vorangegangenen Aktionen ab.
  - Orwellian/m-Orwellian: Die Beobachtung hängt von der gesamten Historie oder einem Fenster von $m$ vorangegangenen Aktionen ab.
- Das Framework geht von asymmetrischer Information aus: Der Angreifer ( $O$ ) und der Supervisor ( $O_S$ ) können unterschiedliche Beobachtungsfunktionen und eine Teil-Sichtbarkeit besitzen.
Aktiver Supervisor:
- Im Gegensatz zu traditionellen Supervisoren, die lediglich Aktionen deaktivieren, besitzt der vorgeschlagene Aktive Supervisor eine duale Fähigkeit:
  1. Aktions-Deaktivierung: Er kann spezifische kontrollierbare Aktionen aus einer Menge $C$ verbieten.
  2. Zeit-Einfügung: Er kann dynamisch Sequenzen von Zeitaktionen ( $t$ ) in den Ausführungsstrom injizieren.
- Der Supervisor operiert unter Teil-Beobachtbarkeit ( $O_S$ ) und zielt darauf ab, sicherzustellen, dass der resultierende supervidierte Pfad zu einer Menge von Sicheren Pfaden ( $K_{P,\phi,O}$ ) gehört, in denen das Geheimnisprädikat $\phi$ vom Angreifer nicht deduziert werden kann.
Formale Modellierung:
- Beobachtungsfunktionen, Prädikate und Supervisoren werden als Prozesse innerhalb des TPA-Frameworks modelliert. Dies ermöglicht die Nutzung von Standard-Verifizierungstechniken (Pfadäquivalenz, Bisimulation), um die Interaktionen zwischen dem System, dem Supervisor und dem Angreifer zu analysieren.
- Das System wird als Kontext $C(P, O_S, Sup)$ modelliert, wobei der Supervisor den Prozess $P$ unter Beobachtung von $O_S$ abfängt und modifiziert.

Hauptbeiträge

Die Arbeit leistet drei primäre Beiträge:

Neuartiges Framework für Aktive Supervisoren unter Teil-Sichtbarkeit:
Die Autoren führen ein Supervisor-Modell ein, das unter asymmetrischer und unvollständiger Information operiert. Dieses Modell kombiniert einzigartig die Fähigkeiten der Aktions-Deaktivierung mit der dynamischen Einfügung von Zeitaktionen, um Informationslecks aktiv zu bekämpfung, insbesondere im Hinblick auf Timing-Seitenkanäle.
Formalisierung asymmetrischer Beobachtungsfunktionen:
Die Studie formalisiert Szenarien, in denen der Angreifer und der Supervisor über distinkte Beobachtungsfunktionen verfügen (z. B. statisch vs. dynamisch oder unterschiedliche Grade der Sichtbarkeit). Dies ermöglicht die Modellierung realistischer Sicherheitsszenarien, in denen keine der beiden Entitäten über die volle Sichtbarkeit verfügt und sich ihre Ansichten der Ausführungshistorie unterscheiden.
Abgrenzung der Entscheidbarkeitsgrenzen:
Die Arbeit etabliert eine umfassende Menge an Entscheidbarkeits- und Unentscheidbarkeitsresultaten bezüglich der Existenz solcher Supervisoren. Sie kartiert die Grenzen der Verifizierbarkeit über verschiedene Systemtypen (endliche Zustände vs. Turing-äquivalent), Beobachtungsgranularitäten sowie die Fähigkeiten sowohl der Angreifer als auch der Supervisoren hinweg.

Ergebnisse

Die theoretische Analyse liefert folgende zentrale Ergebnisse:

Unentscheidbarkeit in allgemeinen Fällen:
- Die Verifizierung, ob ein spezifischer Supervisor für einen gegebenen Prozess und Sprach-Opazität gültig ist, ist im Allgemeinen unentscheidbar (Proposition 3).
- Die Bestimmung, ob irgendein Supervisor existiert, der Sicherheit für einen gegebenen Prozess garantiert, ist ebenfalls unentscheidbar (Proposition 4). Dies resultiert aus der Unentscheidbarkeit der Sprach-Opazität selbst in Turing-äquivalenten Modellen.
Entscheidbarkeit in eingeschränkten Fällen:
- Wenn der Prozess $P$ $P$ endlich zustandsbasiert ist, die Beobachtungsfunktionen statisch sind und das Geheimnisprädikat $\phi$ $ϕ$ (und dessen Negation) endlich definierbar ist (modelliert durch endliche Zustands-Testprozesse), dann gilt:
  - Die Verifizierung, ob ein Supervisor gültig ist, ist entscheidbar.
  - Der Vergleich von Supervisoren und das Finden eines maximalen Supervisors (einer, der das Systemverhalten minimal einschränkt) ist entscheidbar.
  - Ein endlicher zustandsbasierter maximaler Supervisor ist garantiert existent (Propositionen 7 und 8).
Timing-Angriffe und deren Milderung:
- Die Arbeit definiert ein System als anfällig für Timing-Angriffe, wenn es unter einer "zeit-abstrakten" Beobachtung opak ist, aber nicht unter einer "zeit-sensitiven" Beobachtung.
- Es wird bewiesen, dass wenn ein Prädikat zeitabhängig ist (das heißt, ein geheimer Pfad durch das Einfügen von Zeitverzögerungen nicht mehr geheim gemacht werden kann) und der Supervisor mindestens so viel Beobachtungspräzision wie der Angreifer besitzt ( $O \preceq O_S$ ), ein Supervisor existiert, selbst wenn die Menge der kontrollierbaren Aktionen leer ist ( $C = \emptyset$ ). In diesem Fall wird Sicherheit allein durch das Einfügen von Zeitverzögerungen erreicht (Proposition 9).
Kontrollierbarkeitsbeschränkungen:
- Wenn die Menge der sicheren Pfade nicht kontrollierbar ist (d. h. es existiert ein sicherer Pfad, gefolgt von einer unkontrollierbaren Aktion, die zu einem unsicheren Pfad führt), existiert kein Supervisor (Proposition 2).

Bedeutung und Ansprüche

Die Arbeit beansprucht, eine rigorose theoretische Grundlage für die Analyse der Systemsicherheit innerhalb eines Prozessalgebra-Kontexts zu schaffen, wobei sie insbesondere die Grenzen der traditionellen supervisory Kontrolle gegenüber Timing-Angriffen adressiert.

Brückenschlag der Paradigmen: Sie schlägt die Brücke zwischen logischer Durchsetzung (Blockieren von Aktionen) und temporaler Manipulation (Einfügen von Verzögerungen) und bietet einen einheitlichen Kontrollmechanismus für sprachbasierte Opazität.
Realistische Modellierung von Adversaries: Durch die Modellierung sowohl von Angreifern als auch von Supervisoren mit leistungsstarken, asymmetrischen Beobachtungsfunktionen erfasst das Framework die realistische Dynamik moderner dezentraler Systeme, in denen Agenten unter Teil-Sichtbarkeit agieren.
Praktische Verifizierung: Die Autoren behaupten, dass für endliche Zustands-Systeme mit statischen Beobachtungen das vorgeschlagene Framework eine exakte Verifizierung und Synthese von Supervisoren unter Verwendung bestehender Werkzeuge wie CAAL (Concurrency Workbench Alternating-Time Logic) ermöglicht, sofern die Prädikate mittels $\mu$ -Kalkül ausgedrückt werden.
Zukünftige Richtungen: Die Arbeit skizziert bescheiden zukünftige Arbeiten, die auf die Synthese minimaler zeit-einfügender Supervisoren abzielen, um den temporalen Overhead zu reduzieren (Aufrechterhaltung der QoS), sowie die Erweiterung des algebraischen Frameworks auf räumliche Verteilung, Netzwerkarchitekturen und Leistungsverbrauchskennzahlen für die Multi-Domain-Sicherheitsverifizierung.

Die Arbeit schlägt keine neuen experimentellen Implementierungen vor, sondern etabliert die mathematischen Bedingungen, unter denen eine sichere, aktive Supervision theoretisch möglich oder unmöglich ist, um das Design robuster Architekturen für eingebettete und cyber-physische Systeme zu leiten.