💻 computer science

Language-based Security and Time-inserting Supervisor

Dit artikel maakt gebruik van algebraïsche methoden om taalgebaseerde beveiligingseigenschappen te definiëren en stelt een tijd-invoegende supervisor voor die, onder condities van partiële informatie voor zowel de supervisor als de aanvaller, procesbeveiliging waarborgt door ongewenste acties uit te schakelen of getimede gebeurtenissen in te voegen, terwijl het ook het bestaan en de beperkingen van een dergelijke supervisor analyseert.

Oorspronkelijke auteurs: Damas P. Gruska

Gepubliceerd 2026-07-01

📖 5 min leestijd🧠 Diepgaand

CC BY 4.0

Oorspronkelijke auteurs: Damas P. Gruska

Oorspronkelijk artikel gelicentieerd onder CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Dit is een AI-gegenereerde uitleg van het onderstaande artikel. Het is niet geschreven of goedgekeurd door de auteurs. Raadpleeg het oorspronkelijke artikel voor technische nauwkeurigheid. Lees de volledige disclaimer

Stel je voor dat je een beveiligde bankkluis beheert. Je hebt een strikte regel: Niemand mag ooit kunnen raden welke specifieke combinatie van knoppen is ingedrukt om de kluis te openen. Dit is het concept van opacity (ondoorzichtigheid): het geheim (het specifieke pad dat is genomen) verborgen houden voor een waarnemer.

Normaal gesproken, als een systeem onveilig is, heb je twee keuzes:

De kluis herbouwen: Het hele systeem opnieuw ontwerpen zodat het vanaf het begin veilig is. (Dit is duur, moeilijk en vaak onmogelijk als de machine al gebouwd is).
Een bewaker inhuren (Supervisor): Een bewaker buiten zetten die naar de knoppen kijkt. Als de bewaker ziet dat iemand een "slechte" knop wil indrukken, stopt de bewaker hen.

Het probleem met traditionele bewakers:
Het artikel wijst op een gebrek in de "bewaker"-aanpak. Sommige aanvallen gaan niet over welke knoppen worden ingedrukt, maar over hoe snel ze worden ingedrukt. Dit wordt een Timing Attack genoemd.

Voorbeeld: Als de kluis 2 seconden nodig heeft om te openen bij de code "1-2-3" maar slechts 1 seconde bij de code "1-2-4", dan heeft een hacker de knoppen niet eens nodig om te kijken. Ze hebben alleen een stopwatch nodig. De snelheid zelf lekt het geheim.
Een traditionele bewaker die alleen "Stop!" of "Doorgaan!" zegt, kan dit niet oplossen. Als de bewaker het proces stopt, gaat de kluis niet open. Als de bewaker het laat doorgaan, geeft de snelheid het geheim nog steeds weg.

De oplossing van het papier: De "Actieve" Bewaker
De auteur, Damas P. Gruska, stelt een nieuw soort bewaker voor: een Actieve Supervisor. Deze bewaker heeft een superkracht: Tijdmanipulatie.

Zie deze bewaker niet alleen als een uitsmijter, maar als een DJ of een Verkeersregelaar die twee dingen kan doen:

De auto blokkeren: Een specifieke actie stoppen als deze gevaarlijk is (zoals een traditionele bewaker).
Een rood licht toevoegen: Als de auto veilig is om te rijden maar te snel beweegt (waardoor een geheim wordt onthuld), kan de bewaker een kunstmatige "pauze" of "vertraging" invoegen om alles af te remmen.

Door deze kunstmatige pauzes toe te voegen, zorgt de bewaker ervoor dat het "snelle" geheime pad net zo langzaam lijkt als het "langzame" publieke pad. Voor de hacker met de stopwatch zien beide paden er identiek uit. Het geheim blijft behouden.

De adder onder het gras: De bewaker is blind
Dit is het lastige deel dat het papier onderzoekt: De bewaker ziet niet alles.

De Hacker heeft een bril waarmee ze sommige dingen kunnen zien, maar niet andere.
De Bewaker heeft een andere bril. Misschien ziet de bewaker minder dan de hacker, of zien ze misschien andere dingen.
De bewaker moet beslissingen nemen op basis van dit wazige, onvolledige beeld.

Het papier stelt de vraag: Kunnen we altijd een bewaker vinden die het beveiligingsprobleem kan oplossen, gegeven deze beperkingen?

De bevindingen (De "Ja, Nee en Misschien" lijst)
De auteur gebruikt complexe wiskunde (zoals een zeer geavanceerde regelset voor hoe machines denken) om te bepalen wanneer dit mogelijk is:

De "Onmogelijke" Zone: Soms is het antwoord Nee. Als de bewaker te blind is (kan de gevaarlijke acties niet aankomen) en het systeem te complex is (zoals een Turingmachine, die even slim is als een computer), is er geen manier om te garanderen dat het geheim veilig blijft. Het is wiskundig bewezen dat geen enkel algoritme dit voor elk mogelijk scenario kan oplossen.
De "Haalbare" Zone: Als het systeem eenvoudiger is (zoals een eindige verzameling staten, vergelijkbaar met een basis verkeerslicht) en de regels duidelijk zijn, kunnen we wiskundig bewijzen dat er een bewaker bestaat en deze zelfs bouwen.
De "Perfecte" Bewaker: Het papier probeert de "beste" bewaker te vinden—één die het systeem zo min mogelijk hindert. We willen dat de kluis zo snel mogelijk opent, en alleen vertragingen toevoegt wanneer dat absoluut noodzakelijk is. Het papier laat zien hoe we zo'n "maximale" bewaker kunnen vinden in eenvoudigere systemen.

De Grote Beeld Metafoor
Stel je een spelletje "Fluisterspel" voor waarbij een geheim bericht wordt doorgegeven.

De Aanvaller luistert naar de fluisteringen.
Het Systeem is de rij mensen die het bericht doorgeven.
De Timing Attack is wanneer de aanvaller merkt dat de mensen sneller fluisteren wanneer het bericht "Geheim" is dan wanneer het "Openbaar" is.
De Actieve Supervisor is een scheidsrechter die in de rij staat. De scheidsrechter kan niet alles perfect horen, maar kan mensen op de schouder tikken om ze een seconde te laten pauzeren.
Het Doel: De scheidsrechter laat de "snelle" fluisteraars net genoeg wachten, zodat iedereen precies evenveel tijd nodig heeft om het bericht door te geven. De aanvaller, die naar de timing luistert, kan niet langer onderscheiden of het bericht "Geheim" of "Openbaar" was.

Samenvatting
Dit papier introduceert een nieuwe manier om computersystemen te beschermen tegen "timing attacks" (waarbij snelheid een geheim onthult). In plaats van alleen slechte acties te blokkeren, stelt het een slimme controller voor die ook kunstmatige vertragingen kan invoegen om de timing te verbergen. Het papier gebruikt zware wiskunde om precies te bepalen wanneer dit mogelijk is en wanneer het onmogelijk is, afhankelijk van hoeveel de controller kan zien en hoe complex het systeem is.

Technische Samenvatting: Actieve Toezichthoudende Controle voor het Behoud van Opaciteit

Probleemstelling

Moderne systeemtechniek vertrouwt steeds vaker op formele methoden om veiligheid te verifiëren, maar wanneer een systeem onveilig wordt bevonden, is een fundamentele herontwerp vaak even kostbaar als onhaalbaar, met name voor legacy- of ingebedde systemen. Traditionele theorieën voor toezichthoudende controle pakken dit aan door de uitvoering van systeempaden dynamisch te beperken, waarbij controleerbare acties worden ingeschakeld of uitgeschakeld om veiligheids- of beveiligingsbeleid af te dwingen. Dit klassieke paradigma van actiebeperking is echter onvoldoende tegen timing-aanvallen, een krachtige klasse van zijkanaalaanvallen waarbij aanvallers gevoelige interne gegevens afleiden door variaties in de uitvoering en responstijd te meten.

In dergelijke scenario's faalt het louter blokkeren van acties omdat de pacing (het ritme) van gebeurtenissen zelf kritieke informatie lekt. Om deze kwetsbaarheden te mitigeren, moeten systemen het temporele gedrag manipuleren, vaak door kunstmatige tijdsvertragingen in te voegen om temporele varianties te egaliseren. Bovendien heeft bestaand onderzoek naar opaciteit (een taalgebaseerde beveiligingseigenschap die ervoor zorgt dat geheimen verborgen blijven voor waarnemers) zich grotendeels gericht op eindige automaten of toestandsgebaseerde modellen. Dit artikel adresseert de kloof in het afhandelen van taalgebaseerde opaciteit binnen een Timed Process Algebra (TPA) kader, specifiek voor systemen die equivalent zijn aan Turingmachines, waarbij noch de toezichthouder, noch de aanvaller volledige informatie bezit over het gedrag van het systeem.

Methodologie

Het artikel maakt gebruik van een Timed Process Algebra (TPA) kader, een uitbreiding van Milner's Calculus of Communicating Systems (CCS). TPA introduceert een discrete tijdactie ( $t$ ) om het verstrijken van tijd te modelleren, waardoor de formele representatie van timing-aanvallen en informatielekken mogelijk wordt.

Kernconcepten

Opaciteit en Observatiefuncties:
- Opaciteit wordt gedefinieerd als de eigenschap waarbij, voor elke trace die voldoet aan een geheim predicaat $\phi$ , er een andere trace bestaat die niet voldoet aan $\phi$ en die ononderscheidbaar is voor een waarnemer onder een specifieke observatiefunctie $O$ .
- Het artikel formaliseert diverse observatiefuncties ( $O$ $O$ ) om de capaciteiten van aanvallers te modelleren:
  - Statisch: Acties worden onafhankelijk van de context waargenomen.
  - Dynamisch: De observatie van een actie hangt af van de geschiedenis van voorafgaande acties.
  - Orwelliaans/m-Orwelliaans: Observatie hangt af van de volledige geschiedenis of een venster van $m$ voorgaande acties.
- Het kader gaat uit van asymmetrische informatie: de aanvaller ( $O$ ) en de toezichthouder ( $O_S$ ) kunnen verschillende observatiefuncties en gedeeltelijke zichtbaarheid hebben.
Actieve Toezichthouder:
- In tegenstelling tot traditionele toezichthouders die alleen acties uitschakelen, beschikt de voorgestelde Actieve Tozichthouder over een dubbele capaciteit:
  1. Actie-uitschakeling: Het kan specifieke controleerbare acties uit een verzameling $C$ verbieden.
  2. Tijdsinjectie: Het kan dynamisch sequenties van tijdacties ( $t$ ) in de executiestroom injecteren.
- De toezichthouder opereert onder gedeeltelijke observeerbaarheid ( $O_S$ ) en streeft ernaar te waarborgen dat de resulterende gesuperviseerde trace behoort tot een verzameling van Veilige Traces ( $K_{P,\phi,O}$ ), waarbij het geheime predicaat $\phi$ niet door de aanvaller kan worden afgeleid.
Formele Modellering:
- Observatiefuncties, predicaten en toezichthouders worden gemodelleerd als processen binnen het TPA-kader. Dit maakt het gebruik van standaard verificatietechnieken (trace-equivalentie, bisimulatie) mogelijk om de interacties tussen het systeem, de toezichthouder en de aanvaller te analyseren.
- Het systeem wordt gemodelleerd als een context $C(P, O_S, Sup)$ , waarbij de toezichthouder het proces $P$ onderschept en de uitvoering ervan wijzigt op basis van zijn observaties.

Belangrijkste Bijdragen

Het artikel levert drie primaire bijdragen:

Nieuw Actief Toezichthouder-kader onder Partiële Zichtbaarheid:
De auteurs introduceren een toezichthouder-model dat opereert onder asymmetrische en onvolledige informatie. Dit model combineert uniek de capaciteiten van actie-uitschakeling met de dynamische injectie van tijdacties om informatielekken actief te mitigeren, specifiek gericht op timing-zijkanalen.
Formalisering van Asymmetrische Observatiefuncties:
De studie formaliseert scenario's waarin de aanvaller en de toezichthouder over verschillende observatiefuncties beschikken (bijv. statisch versus dynamisch, of verschillende niveaus van zichtbaarheid). Dit maakt het modelleren mogelijk van realistische beveiligingsinstellingen waarbij geen van beide entiteiten over volledige zichtbaarheid beschikt en hun visies op de executiegeschiedenis uiteenlopen.
Afbakening van Beslisbaarheidsgrenzen:
Het artikel stelt een uitgebreide set van beslisbaarheids- en onbeslisbaarheidsresultaten vast met betrekking tot de existentie van dergelijke toezichthouders. Het brengt de grenzen in kaart van de verificatie haalbaarheid over diverse systemtypen (eindige toestanden versus Turing-equivalent), observatiegranulariteiten en de capaciteiten van zowel aanvallers als toezichthouders.

Resultaten

De theoretische analyse levert de volgende belangrijke resultaten op:

Onbeslisbaarheid in Algemene Gevallen:
- Het verifiëren of een specifieke toezichthouder geldig is voor een gegeven proces en taal-opaciteit is in het algemeen onbeslisbaar (Propositie 3).
- Het vaststellen of er welke toezichthouder dan ook bestaat die veiligheid garandeert voor een gegeven proces is ook onbeslisbaar (Propositie 4). Dit vloeit voort uit de onbeslisbaarheid van taal-opaciteit zelf in Turing-equivalente modellen.
Beslisbaarheid in Beperkte Gevallen:
- Als het proces $P$ $P$ een eindige toestand is, de observatiefuncties statisch zijn en het geheime predicaat $\phi$ $ϕ$ (en de negatie daarvan) eindig definieerbaar is (gemodelleerd door eindige toestand test-processen), dan:
  - Is het verifiëren of een toezichthouder geldig is beslisbaar.
  - Is het vergelijken van toezichthouders en het vinden van een maximale toezichthouder (één die de systeemgedragingen minimaal beperkt) beslisbaar.
  - Een eindige toestand maximale toezichthouder is gegarandeerd aanwezig (Proposities 7 en 8).
Timing-aanvallen en Mitigatie:
- Het artikel definieert een systeem als vatbaar voor timing-aanvallen als het opaak is onder een "tijd-abstracte" observatie, maar niet onder een "tijd-sensitieve" observatie.
- Het bewijst dat als een predicaat tijd-afhankelijk is (wat betekent dat een geheime trace niet-geheim gemaakt kan worden door tijdvertragingen in te voegen) en de toezichthouder ten minste evenveel observationele precisie heeft als de aanvaller ( $O \preceq O_S$ ), er een toezichthouder bestaat zelfs met een lege verzameling controleerbare acties ( $C = \emptyset$ ). In dit geval wordt veiligheid uitsluitend bereikt door het invoegen van tijdvertragingen (Proposition 9).
Controleerbaarheidsrestricties:
- Als de verzameling veilige traces niet controleerbaar is (dat wil zeggen: er bestaat een veilige trace gevolgd door een oncontroleerbare actie die leidt tot een onveilige trace), dan bestaat er geen toezichthouder (Proposition 2).

Betekenis en Claims

Het artikel claimt een rigoureus theoretisch fundament te bieden voor het analyseren van systeembeveiliging binnen een proces-algebraïsche context, waarbij specifiek wordt ingegaan op de beperkingen van traditionele toezichthoudende controle tegen timing-aanvallen.

Bruggen Slaan tussen Paradigma's: Het overbrugt de kloof tussen logische handhaving (blokkeren van acties) en temporele manipulatie (invoegen van vertragingen), wat leidt tot een verenigd controlesysteem voor taalgebaseerde opaciteit.
Realistische Adversarial Modellering: Door zowel aanvallers als toezichthouders te modelleren met krachtige, asymmetrische observatiefuncties, vangt het kader de realistische dynamiek van moderne gedecentraliseerde systemen waar agenten opereren onder partiële zichtbaarheid.
Praktische Verificatie: De auteurs stellen dat voor eindige toestandssystemen met statische observaties, het voorgestelde kader exacte verificatie en synthese van toezichthouders mogelijk maakt met bestaande tools zoals CAAL (Concurrency Workbench Alternating-Time Logic), mits predicaten worden uitgedrukt via $\mu$ -calculus.
Toekomstige Richtingen: Het artikel schetst bescheiden toekomstig werk gericht op het synthetiseren van minimale tijd-invoegende toezichthouders om de temporele overhead te verminderen (behoud van QoS) en het uitbreiden van het algebraïsche kader om ruimtelijke distributie, netwerkarchitecturen en stroomverbruik-metrieken voor multi-domein beveiligingsverificatie te omvatten.

Het werk stelt geen nieuwe experimentele implementaties voor, maar stelt de wiskundige condities vast waaronder actieve, toezichthoudende controle theoretisch wel of niet mogelijk is, ter ondersteuning van het ontwerp van robuuste architecturen voor embedded en cyber-fysieke systemen.