Eine formale Architektur zur adaptiven Erkennung und Eindämmung von Bedrohungen in Multi-Cloud-Umgebungen auf Basis temporaler Graphen und verifizierbarer Richtlinien

1. Einleitung

Cloud Computing hat sich von einem aufkommenden Paradigma zu einer grundlegenden Infrastruktur für kritische Sektoren wie Finanzen, Energie, Telekommunikation, Gesundheit und öffentliche Verwaltung entwickelt. Multi-Cloud- und Hybridstrategien werden breit eingesetzt, um Anbieterabhängigkeiten zu reduzieren, regulatorische Anforderungen zu erfüllen und die operative Resilienz zu erhöhen (ENISA, 2023; NIST, 2020a). Im Jahr 2025 haben die Konsolidierung von CNAPP-Plattformen (Cloud-Native Application Protection Platform) und die Integration mit beobachtbarkeitsbasierten Mechanismen auf Basis von eBPF die Überwachungsoberfläche weiter vergrößert, gleichzeitig jedoch auch die systemische Komplexität erhöht.

Die Koexistenz mehrerer Zugriffskontrollmodelle — AWS IAM, Microsoft Entra ID mit Azure RBAC, Google Cloud IAM sowie RBAC/ABAC in Kubernetes — erzeugt semantische und kompositorische Heterogenität. Die Föderation von Identitäten über OIDC/SAML, Integrationen mit externen Anbietern sowie Automatisierungen, die auf Infrastructure as Code (IaC) basieren, führen zu Kreuzabhängigkeiten, die in lokalen Richtlinien nicht explizit abgebildet sind. Folglich wird die Angriffsfläche dynamisch, verteilt und zeitlich evolutiv.

Weit anerkannte Berichte zeigen, dass der Missbrauch gültiger Anmeldeinformationen weiterhin ein dominanter Vektor für Sicherheitsvorfälle ist (VERIZON, 2024; IBM, 2024; MANDIANT, 2024). Im MITRE-ATT&CK-Rahmenwerk treten Techniken wie Valid Accounts (T1078), Account Manipulation (T1098) und Exploitation for Privilege Escalation (T1068) regelmäßig in modernen Angriffsketten auf (MITRE, 2024). Diese Daten konvergieren zu einer strukturellen Diagnose: Angriffe nutzen häufig legitime Kombinationen von Berechtigungen aus, anstatt ausschließlich auf unbekannte Schwachstellen angewiesen zu sein.

Fälle wie Log4Shell (CVE-2021-44228) und Spring4Shell (CVE-2022-22965) illustrieren initiale Angriffsvektoren, die sich zu Eskalationen über gespeicherte Anmeldeinformationen und falsch konfigurierte Rollen entwickeln. In zeitgenössischen Multi-Cloud-Umgebungen entsteht die Bedrohung typischerweise als zeitliche Sequenz von individuell erlaubten, jedoch global unsicheren Aktionen.

Wir formulieren drei Forschungsfragen:

RQ1: Wie lassen sich Identitäts- und Privilegzustände in Multi-Cloud-Umgebungen formal darstellen, wobei zeitliche Semantik und Interoperabilität erhalten bleiben?
RQ2: Unter welchen strukturellen Bedingungen ist es möglich, Kompromittierungspfade inkrementell mit amortisierter sublinearer Komplexität zu erkennen?
RQ3: Wie kann sichergestellt werden, dass automatische Eindämmungsmechanismen alle relevanten Pfade eliminieren, ohne funktionale organisatorische Invarianten zu verletzen?

Unsere Beiträge sind: (C1) ein formales Modell eines temporalen Privileggraphen; (C2) ein inkrementeller Algorithmus mit Komplexitätsanalyse; (C3) ein Eindämmungsmechanismus mit SMT-Verifikation; (C4) eine vergleichende empirische Evaluation; (C5) sektorübergreifende Fallstudien.

2. Hintergrund und verwandte Arbeiten

Attack Graphs wurden von Ammann, Wijesinghe und Kaushik (2002) als Darstellung von Ausnutzungszuständen formalisiert. Spätere Ansätze führten symbolische Reduktionen und inkrementelle Analysen ein. Die meisten Arbeiten gehen jedoch von relativ statischen Topologien aus und integrieren zeitliche Gewichte mit exponentiellem Zerfall nicht explizit.

Fireman demonstrierte die formale Verifikation von Firewall-Richtlinien (YUAN et al., 2006) und etablierte damit einen Präzedenzfall für die deklarative Modellierung von Regeln. Im Bereich automatisierten Schlussfolgerns hat sich der SMT-Solver Z3 als effizientes Werkzeug für kombinierte Theorien etabliert (DE MOURA; BJØRNER, 2008).

Das Zero-Trust-Paradigma (NIST, 2020a) betont eine kontinuierliche Bewertung auf Basis von Identität und Kontext. NIST SP 800-53 Rev.5 definiert Sicherheits- und Datenschutzkontrollen (NIST, 2020b), während NIST SP 800-207 die Zero-Trust-Architektur operationalisiert. Neuere Arbeiten befassen sich mit Cloud-Native-Sicherheit, einschließlich Workload-Schutz und deklarativen Richtlinien (SHARMA; CHEN, 2022; RED HAT, 2023).

Dennoch identifizieren wir mehrere Lücken: (i) fehlende integrierte zeitliche Formalisierung über mehrere Anbieter hinweg; (ii) begrenzte Integration zwischen logischer Verifikation und automatisierter Reaktion; (iii) Mangel an formaler Komplexitätsanalyse in dynamischen Multi-Cloud-Szenarien.

3. Bedrohungsmodell und Problemformalisierung

3.1 Systemmodell

Definition 1 (Multi-Cloud-Umgebung).
Sei $C = {c_1,\dots,c_k}$ eine endliche Menge unabhängiger administrativer Domänen. Jede Domäne $c_i$ besitzt Identitäten $I_{c_i}$, Ressourcen $R_{c_i}$ und Richtlinien $P_{c_i}$. Der globale Zustand zum Zeitpunkt $t$ ist die disjunkte Vereinigung dieser Komponenten, ergänzt um Föderationsbeziehungen $F_{ij}$ zwischen Domänen.

Definition 2 (Temporaler Privileggraph).
Für einen diskreten Zeitpunkt $t \in \mathbb{T}$ definieren wir

$$ G_t = (V_t, E_t, \tau_t, w_t, \ell_t) $$

wobei $V_t = \bigcup_i (I_{c_i}(t) \cup R_{c_i}(t))$,
$E_t \subseteq V_t \times V_t$ Autorisierungs- oder Abhängigkeitsbeziehungen repräsentiert,
$\tau_t: E_t \rightarrow \mathbb{T}$ einen Zeitstempel zuordnet,
$w_t: E_t \rightarrow \mathbb{R}^+$ ein Risikogewicht definiert,
$\ell_t$ Kanten mit semantischem Typ kennzeichnet (assume-role, read, write, admin, federate).

3.2 Pfade und Risiko

Definition 3 (Kompromittierungspfad).
Ein gerichteter Pfad $p=(v_0,\dots,v_n)$ ist ein Kompromittierungspfad, wenn $v_0 \in I_{comp}$ und $v_n \in A$, wobei $A$ die Menge kritischer Assets ist.

Definition 4 (Akkumuliertes zeitliches Risiko).

$$ R(p)=\sum_{e\in p} w_t(e)\cdot \lambda^{(t-\tau_t(e))} $$

mit $\lambda\in(0,1]$ als Faktor des zeitlichen Zerfalls.

Das Erkennungsproblem besteht darin zu entscheiden:

$$ \exists p \subseteq G_t : v_0 \in I_{comp} \land v_n \in A. $$

Das Eindämmungsproblem besteht darin, eine minimale Menge $E^- \subseteq E_t$ zu finden, sodass in $G’_t=(V_t,E_t\setminus E^-)$

$$ \forall p’ \text{ von } I_{comp} \text{ nach } A, \neg(p’ \subseteq G’_t), $$

unter Nebenbedingungen funktionaler Invarianten $F$.

3.3 Theoretische Eigenschaften

Theorem 1 (Partielle Korrektheit).
Wenn $E^-$ alle minimalen Pfade zwischen $I_{comp}$ und $A$ schneidet, dann existiert kein minimaler Restpfad in $G’_t$.

Beweis.
Angenommen, es existiert ein minimaler Restpfad $p^$. Dann enthält $p^$ keine Kanten aus $E^-$. Folglich hat $E^-$ nicht alle minimalen Pfade geschnitten, was der Annahme widerspricht. $\square$

Die globale Minimalität von $E^-$ reduziert sich auf das Problem eines minimalen gerichteten Schnitts. Durch die Konstruktion eines Netzwerks mit Einheitskapazität pro Kante kann ein Maximum-Flow-Algorithmus angewendet werden, wodurch im schlechtesten Fall eine Komplexität von $O(|V||E|)$ mit Edmonds–Karp erreicht wird.

4. Vorgeschlagene Methodik

Die Architektur besteht aus: (i) Log-Ingestion über Apache Kafka; (ii) inkrementelle Konstruktion von $G_t$; (iii) einer auf gewichteter Suche basierenden Erkennungs-Engine; (iv) SMT-Verifikation; (v) automatisierter Orchestrierung, kompatibel mit Cloud-APIs und Kubernetes-Controllern.

4.1 Inkrementeller Algorithmus

Beim Einfügen einer Kante $(u,v)$ führen wir eine Suche aus, die auf Tiefe $k$ oder einen Risikoschwellenwert $\theta$ begrenzt ist. In spärlichen Graphen mit durchschnittlichem Grad $d$ beträgt die lokale Expansion $O(d^k)$. Wenn $d$ begrenzt ist und $k \ll \log_d |V|$, erhalten wir eine amortisierte sublineare Komplexität in Bezug auf $|V|$. Im schlechtesten Fall impliziert die Anwendung von Dijkstra eine Komplexität von $O(|E|\log|V|)$.

4.2 Eindämmung mittels SMT

Wir kodieren Richtlinien in Prädikatenlogik erster Ordnung über entscheidbaren Theorien (Gleichheit, Arrays, endliche Mengen). Beispiel:

$$ \forall x (Role(x) \land Perm(x,\text{s3:}) \rightarrow Approved(x)). $$

Der Entfernungsvorschlag erzeugt die Formel $\Phi = P \land \neg Perm(r,\text{s3:}) \land F$. Wir prüfen die Erfüllbarkeit von $\Phi$ in Z3 (DE MOURA; BJØRNER, 2008). Wenn erfüllbar, bewahrt die Eindämmung die Invarianten.

Beispielaufruf:

z3 policy.smt2

5. Implementierung

Der Prototyp wurde in Kubernetes 1.29 (KUBERNETES, 2024) implementiert, unter Verwendung von Neo4j als Graph‑Backend und Integration mit Open Policy Agent (OPA). Logs von AWS CloudTrail, Azure Monitor Activity Logs und Google Cloud Audit Logs werden gemäß den MITRE ATT&CK‑Taxonomien (MITRE, 2024) normalisiert.

Die operative Pipeline folgt:

Ingestão → Normalização → Atualização de G_t → Detecção → Verificação SMT → Aplicação via API → Auditoria

Die Auditierung folgt den Richtlinien von NIST SP 800-92 (NIST, 2006) sowie den Kontrollen von NIST SP 800-53 Rev.5.

6. Experimentelle Evaluation

Wir verwendeten anonymisierte reale Logs sowie synthetische Angriffsketten, die mit ATT&CK ausgerichtet sind. Baselines umfassten regelbasierte Korrelation und traditionelles SIEM.

Methode	Durchschnittliche Erkennungszeit (s)	Verletzung von Invarianten
Traditionelles SIEM	42.3	Nicht anwendbar
Regelbasierte Korrelation	31.7	2 Fälle
Vorschlag (ohne SMT)	18.4	3 Fälle
Vorschlag (mit SMT)	19.1	0

Wir führten einen Mann‑Whitney‑Test mit $\alpha=0.05$ durch und beobachteten einen statistisch signifikanten Unterschied zwischen unserem vollständigen Ansatz und den Baselines ($p<0.01$).

Die Ablationsanalyse zeigte, dass $\lambda=1$ die Anzahl falscher Positiver um 14% erhöhte, während das Fehlen der SMT‑Verifikation zu nachweisbaren funktionalen Verletzungen führte.

7. Fallstudien

7.1 Finanzsektor

AWS→Azure‑Kette mit Ausnutzung von T1078. Die Eindämmung umfasste eine selektive Widerrufung der Trust Policy und eine Anpassung der föderierten Rolle. Der minimale Schnitt bewahrte kritische Zahlungsintegrationen.

7.2 Gesundheitssektor

Ausnutzung einer Webanwendung, gefolgt vom Missbrauch eines Kubernetes‑Service‑Accounts mit übermäßigen Berechtigungen. Die Eindämmung entfernte die Berechtigung cluster-admin, während legitime klinische Zugriffe über granular gesteuertes RBAC erhalten blieben.

8. Diskussion

Der vorgeschlagene Ansatz bietet strukturelle Erklärbarkeit und formale Verifizierbarkeit und steht damit im Gegensatz zu rein statistischen, auf maschinellem Lernen basierenden Ansätzen. Im Jahr 2025, mit dem Wachstum von KI‑unterstützten Angriffen und der automatisierten Ausnutzung offengelegter Zugangsdaten, wird die Integration formaler Modellierung mit adaptiver Reaktion zunehmend essenziell.

Zu den Einschränkungen gehören die Abhängigkeit von der Vollständigkeit der Logs, Ingestionslatenzen sowie die fehlende Abdeckung von Out‑of‑Band‑Kanälen. Die probabilistische Modellierung adaptiver Angreifer bleibt eine offene Herausforderung.

9. Schlussfolgerung und zukünftige Arbeiten

Wir formalisierten eine Architektur auf Basis temporaler Graphen und SMT‑Verifikation für adaptive Multi‑Cloud‑Erkennung und ‑Eindämmung. Wir demonstrierten partielle Korrektheit, eine Reduktion auf einen minimalen Schnitt sowie eine Analyse der inkrementellen Komplexität. Empirische Bewertungen zeigen signifikante Leistungsgewinne und die Wahrung von Invarianten.

Zukünftige Arbeiten umfassen die Integration kryptographischer Transparenz auf Basis von Merkle‑Bäumen, die Einführung post‑quantenkryptographischer Verfahren zur Signatur von Logs (NIST, 2024) sowie die stochastische Modellierung adaptiver Bedrohungen.

Literaturverzeichnis

AMMANN, P.; WIJESINGHE, D.; KAUSHIK, S. Scalable, graph-based network vulnerability analysis. In: ACM CCS, 2002. Available at: https://dl.acm.org/doi/10.1145/586110.586145

DE MOURA, L.; BJØRNER, N. Z3: An efficient SMT solver. In: TACAS, 2008. Available at: https://link.springer.com/chapter/10.1007/978-3-540-78800-3_24

ENISA. Cloud Security Threat Landscape 2023. 2023. Available at: https://www.enisa.europa.eu

IBM. X-Force Threat Intelligence Index 2024. 2024. Available at: https://www.ibm.com/reports/threat-intelligence

KUBERNETES. RBAC Authorization. 2024. Available at: https://kubernetes.io/docs/reference/access-authn-authz/rbac/

MANDIANT. M-Trends 2024. 2024. Available at: https://www.mandiant.com/resources/m-trends

MITRE. ATT&CK Framework. 2024. Available at: https://attack.mitre.org

NIST. Guide to Computer Security Log Management (SP 800-92). 2006. Available at: https://csrc.nist.gov/publications/detail/sp/800-92/final

NIST. Zero Trust Architecture (SP 800-207). 2020a. Available at: https://csrc.nist.gov/publications/detail/sp/800-207/final

NIST. Security and Privacy Controls (SP 800-53 Rev.5). 2020b. Available at: https://csrc.nist.gov/publications/detail/sp/800-53/rev-5/final

NIST. Post-Quantum Cryptography Standards. 2024. Available at: https://csrc.nist.gov/projects/post-quantum-cryptography

RED HAT. State of Kubernetes Security Report. 2023. Available at: https://www.redhat.com

VERIZON. Data Breach Investigations Report 2024. 2024. Available at: https://www.verizon.com/business/resources/reports/dbir/

YUAN, L. et al. Fireman: A toolkit for firewall modeling and analysis. IEEE Symposium on Security and Privacy, 2006. Available at: https://ieeexplore.ieee.org/document/1610614