Paper Files / Cloud
TITEL: Eine formale Architektur zur adaptiven Erkennung und Eindämmung von Bedrohungen in Multi-Cloud-Umgebungen auf Basis temporaler Graphen und verifizierbarer Richtlinien
TITEL: Eine formale Architektur zur adaptiven Erkennung und Eindämmung von Bedrohungen in Multi-Cloud-Umgebungen auf Basis temporaler Graphen und verifizierbarer Richtlinien ABSTRAKT: Die Einführung von Multi-Cloud- und Hybrid-Strategien hat sich in kritischen Sektoren als dominierende Praxis etabliert und erweitert die semantische und operative Komplexität von Zugriffssteuerungs- und Sicherheitsüberwachungsmechanismen. Die Heterogenität zwischen AWS IAM, Microsoft Entra ID/Azure RBAC, Google Cloud IAM und RBAC/ABAC-Modellen in Kubernetes, kombiniert mit Identitätsföderation, CI/CD-Pipelines und API-gesteuerten Integrationen, führt zu zeitlichen und transversalen Abhängigkeiten, die durch lokale Richtlinienanalysen nicht erfasst werden. Aktuelle Berichte zeigen, dass der Missbrauch gültiger Anmeldedaten weiterhin der vorherrschende Angriffsvektor bei Vorfällen ist und häufig legitime Kombinationen von Berechtigungen ausnutzt. Wir schlagen eine formale Architektur zur adaptiven Erkennung und Eindämmung von Bedrohungen vor, die auf temporalen Privileggraphen und automatischer Richtlinienverifikation mittels SMT basiert. Wir formalisieren die Multi-Cloud-Umgebung als dynamisches System G_t = (V_t, E_t, τ_t, w_t, ℓ_t), definieren Kompromittierungspfade, akkumuliertes zeitliches Risiko und das Dualproblem von Erkennung und Eindämmung als Instanzen von Erreichbarkeit und minimalem Schnitt unter funktionalen Nebenbedingungen. Wir zeigen partielle Korrektheitseigenschaften und eine Reduktion auf Max-Flow für minimale Eindämmung. Wir präsentieren einen inkrementellen Algorithmus mit amortisierter sublinearer Komplexitätsanalyse unter Annahmen von Dünnheit und zeitlicher Lokalität. Die Eindämmung wird durch die Kodierung organisatorischer Invarianten in entscheidender Prädikatenlogik erster Stufe validiert, gelöst mittels SMT. Wir implementierten einen Prototyp in Kubernetes 1.29 mit Graph-Backend und Integration mit OPA sowie MITRE-ATT&CK-Taxonomien. Empirische Auswertungen mit anonymisierten realen Logs und synthetischen Szenarien zeigen eine statistisch signifikante Reduktion der Erkennungszeit im Vergleich zu ausschließlich korrelationsbasierten Ansätzen. Fallstudien aus dem Finanz- und Gesundheitssektor veranschaulichen die Fähigkeit, Angriffsketten zu blockieren und dabei funktionale Anforderungen zu erhalten. Der Vorschlag trägt zur Konvergenz von identitätsbasierter Sicherheit, formaler Verifikation und automatisierter Reaktion in zeitgenössischen Multi-Cloud-Ökosystemen bei.
- Einleitung
Cloud Computing hat sich von einem aufkommenden Paradigma zu einer grundlegenden Infrastruktur kritischer Sektoren wie Finanzen, Energie, Telekommunikation, Gesundheitswesen und öffentlicher Verwaltung entwickelt. Multi-Cloud- und Hybrid-Strategien werden weithin eingesetzt, um Anbieterabhängigkeit zu verringern, regulatorische Anforderungen zu erfüllen und die operationale 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 auf eBPF basierenden Observability-Mechanismen die Überwachungsfläche weiter vergrößert, jedoch auch die systemische Komplexität.
Das Nebeneinander mehrerer Zugriffskontrollmodelle — AWS IAM, Microsoft Entra ID mit Azure RBAC, Google Cloud IAM sowie RBAC/ABAC in Kubernetes — erzeugt semantische und kompositionelle Heterogenität. Die Identitätsföderation via OIDC/SAML, Integrationen mit externen Providern und auf Infrastructure as Code (IaC) ausgerichtete Automatisierungen führen zu impliziten Querverbindungen, die in lokalen Richtlinien nicht explizit gemacht werden. Folglich wird die Angriffsfläche dynamisch, verteilt und zeitlich evolvierend.
Weit verbreitete Berichte weisen darauf hin, dass der Missbrauch gültiger Anmeldedaten weiterhin der dominierende Vektor von Vorfällen ist (VERIZON, 2024; IBM, 2024; MANDIANT, 2024). Im MITRE-ATT&CK-Rahmenwerk sind Techniken wie Valid Accounts (T1078), Account Manipulation (T1098) und Exploitation for Privilege Escalation (T1068) in modernen Angriffsketten wiederkehrend (MITRE, 2024). Diese Daten laufen auf eine strukturelle Diagnose hinaus: Angriffe nutzen häufig legitime Kombinationen von Berechtigungen aus, anstatt sich ausschließlich auf unbekannte Schwachstellen zu stützen.
Fälle wie Log4Shell (CVE-2021-44228) und Spring4Shell (CVE-2022-22965) veranschaulichen Initialvektoren, die sich zu Eskalationen über gespeicherte Anmeldedaten und fehlkonfigurierte Rollen entwickeln. In gegenwärtigen Multi-Cloud-Umgebungen tritt die Bedrohung typischerweise als zeitliche Sequenz einzelner erlaubter, global jedoch unsicherer Handlungen auf.
Wir formulieren drei Forschungsfragen:
RQ1: Wie lassen sich Zustände von Identität und Privilegien in Multi-Cloud-Umgebungen formal darstellen, während zeitliche Semantik und Interoperabilität erhalten bleiben?
RQ2: Unter welchen strukturellen Bedingungen ist es möglich, Kompromittierungspfade inkrementell mit sublinear amortisierter Komplexität zu erkennen?
RQ3: Wie kann sichergestellt werden, dass automatische Containment-Mechanismen alle relevanten Pfade eliminieren, ohne organisationale funktionale Invarianten zu verletzen?
Wir tragen bei mit: (C1) einem formalen Modell eines temporalen Privileggraphen; (C2) einem inkrementellen Algorithmus mit Komplexitätsanalyse; (C3) einem Containment-Mechanismus mit SMT-Verifikation; (C4) einer empirischen Vergleichsevaluation; (C5) sektorübergreifenden Fallstudien.
- Hintergrund und verwandte Arbeiten
Angriffsgraphen wurden von Ammann, Wijesinghe und Kaushik (2002) als Darstellung von Exploit-Zuständen formalisiert. Spätere Ansätze führten symbolische Reduktionen und inkrementelle Analysen ein. Die Mehrheit dieser Arbeiten nimmt jedoch relativ statische Topologien an und integriert explizit keine zeitlichen Gewichte mit exponentiellem Zerfall.
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 des automatisierten Schließens 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 die 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. Jüngere Arbeiten behandeln Cloud-native Sicherheit, einschließlich Workload-Schutz und deklarativer Richtlinien (SHARMA; CHEN, 2022; RED HAT, 2023).
Wir identifizieren jedoch Lücken: (i) das Fehlen einer integrierten zeitlichen Formalisierung über mehrere Provider hinweg; (ii) eine begrenzte Integration zwischen logischer Verifikation und automatisierter Reaktion; (iii) ein Mangel an formaler Komplexitätsanalyse in dynamischen Multi-Cloud-Szenarien.
- 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 $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 den 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 darstellt,
$\tau_t: E_t \rightarrow \mathbb{T}$ einen Zeitstempel zuordnet,
$w_t: E_t \rightarrow \mathbb{R}^+$ ein Risikogewicht definiert,
$\ell_t$ Kanten mit einer semantischen Typisierung versieht (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 (Kumuliertes zeitliches Risiko).
$$ R(p)=\sum_{e\in p} w_t(e)\cdot \lambda^{(t-\tau_t(e))} $$
mit $\lambda\in(0,1]$ als Zeitzerfallsfaktor.
Das Erkennungsproblem besteht darin zu entscheiden:
$$ \exists p \subseteq G_t : v_0 \in I_{comp} \land v_n \in A. $$
Das Containment-Problem besteht darin, eine minimale Menge $E^- \subseteq E_t$ zu finden, so dass in $G’_t=(V_t,E_t\setminus E^-)$ gilt:
$$ \forall p’ \text{ von } I_{comp} \text{ nach } A, \neg(p’ \subseteq G’_t), $$
unter den funktionalen Invarianten $F$.
3.3 Theoretische Eigenschaften
Satz 1 (Partielle Korrektheit).
Falls $E^-$ alle minimalen Pfade zwischen $I_{comp}$ und $A$ schneidet, dann existiert in $G’_t$ kein minimaler Restpfad.
Beweis.
Angenommen im Widerspruch, es existiere ein minimaler Restpfad $p^$. Dann enthält $p^$ keine Kanten aus $E^-$. Folglich hat $E^-$ nicht alle minimalen Pfade geschnitten, im Widerspruch zur Hypothese. $\square$
Die globale Minimalität von $E^-$ reduziert sich auf das Problem des gerichteten Minimum-Cuts. Durch die Konstruktion eines Netzwerks mit Einheitskapazität pro Kante können wir den Max-Flow-Algorithmus anwenden und erhalten im Worst Case eine Komplexität von $O(|V||E|)$ mit Edmonds–Karp.
- Vorgeschlagene Methodik
Die Architektur besteht aus: (i) Ingestion von Logs via Apache Kafka; (ii) inkrementeller Konstruktion von $G_t$; (iii) einem Erkennungsmodul auf Basis gewichteter Suche; (iv) SMT-Verifikation; (v) automatisierter Orchestrierung, kompatibel mit Cloud-APIs und Kubernetes-Controllern.
4.1 Inkrementeller Algorithmus
Beim Einfügen der Kante $(u,v)$ führen wir eine Suche aus, die auf Tiefe $k$ oder Risikoschwelle $\theta$ begrenzt ist. In dünn besetzten Graphen mit mittlerem Grad $d$ ist die lokale Expansion $O(d^k)$. Ist $d$ begrenzt und $k \ll \log_d |V|$, erhalten wir eine amortisierte sublineare Komplexität in $|V|$. Im Worst Case führt die Anwendung von Dijkstra zu $O(|E|\log|V|)$.
4.2 Containment via SMT
Wir kodieren Richtlinien in Prädikatenlogik erster Stufe über entscheidbaren Theorien (Gleichheit, Arrays, endliche Mengen). Beispiel:
$$ \forall x (Role(x) \land Perm(x,\text{s3:}) \rightarrow Approved(x)). $$
Der vorgeschlagene Entfernungsprozess erzeugt die Formel $\Phi = P \land \neg Perm(r,\text{s3:}) \land F$. Wir überprüfen die Erfüllbarkeit von $\Phi$ in Z3 (DE MOURA; BJØRNER, 2008). Ist $\Phi$ erfüllbar, bleibt durch das Containment die Invarianz erhalten.
Beispielaufruf:
z3 policy.smt2
- 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). AWS CloudTrail-, Azure Monitor Activity Logs- und Google Cloud Audit Logs werden gemäß MITRE-ATT&CK-Taxonomien normalisiert (MITRE, 2024).
Die operative Pipeline verläuft wie folgt:
Ingestion → Normalisierung → Aktualisierung von G_t → Erkennung → SMT-Verifikation → Anwendung via API → Audit
Das Audit folgt den Richtlinien des NIST SP 800-92 (NIST, 2006) sowie den Kontrollen des NIST SP 800-53 Rev.5.
- Experimentelle Evaluation
Wir verwendeten anonyme reale Logs und synthetische, an ATT&CK ausgerichtete Ketten. Zu den Baselines gehörten regelbasierte Korrelation und ein traditionelles SIEM.
| Methode | Mittlere 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 wendeten den Mann-Whitney-Test mit $\alpha=0.05$ an und beobachteten einen statistisch signifikanten Unterschied zwischen unserem vollständigen Ansatz und den Baselines ($p<0.01$).
Die Ablationsanalyse zeigte, dass $\lambda=1$ die Zahl der False Positives um 14 % erhöhte, während der Verzicht auf SMT-Verifikation zu nachweisbaren funktionalen Verletzungen führte.
- Fallstudien
7.1 Finanzsektor
AWS→Azure-Kette unter Ausnutzung von T1078. Das Containment umfasste die selektive Widerrufung einer Trust Policy und die Anpassung einer föderierten Rolle. Der minimale Schnitt bewahrte kritische Zahlungsintegrationen.
7.2 Gesundheitssektor
Ausnutzung einer Webanwendung gefolgt vom Missbrauch einer Kubernetes-Service-Account mit übermäßigen Berechtigungen. Das Containment entfernte die Berechtigung cluster-admin und bewahrte legitime klinische Zugriffe über granularen RBAC.
- Diskussion
Der Vorschlag bietet strukturelle Erklärbarkeit und formale Verifizierbarkeit und steht damit im Kontrast zu rein statistischen Ansätzen auf Basis von Machine Learning. Im Jahr 2025 wird angesichts wachsender KI-gestützter Angriffe und automatisierter Ausnutzung offengelegter Anmeldedaten die Integration von formaler Modellierung und adaptiver Reaktion essenziell.
Zu den Einschränkungen gehören die Abhängigkeit von der Vollständigkeit der Logs, die Ingestion-Latenz und die Nichtabdeckung von Out-of-Band-Kanälen. Die probabilistische Modellierung adaptiver Angreifer bleibt eine offene Herausforderung.
- Schlussfolgerung und zukünftige Arbeiten
Wir formalisierten eine auf temporalen Graphen und SMT-Verifikation basierende Architektur zur adaptiven Multi-Cloud-Erkennung und -Eindämmung. Wir demonstrierten partielle Korrektheit, Reduktion auf Minimum-Cut und inkrementelle Komplexitätsanalyse. Empirische Bewertungen zeigen signifikante Zugewinne bei Leistung und Invarianz-Erhaltung.
Zukünftige Arbeiten umfassen die Integration mit kryptographischer Transparenz auf Basis von Merkle-Bäumen, die Einführung post-quantischer Kryptographie zur Signierung von Logs (NIST, 2024) sowie die stochastische Modellierung adaptiver Bedrohungen.
Referenzen
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