← Retour aux articles

Paper Files / Cloud

Une architecture formelle pour la détection et la contention adaptative des menaces dans des environnements multi-cloud basée sur des graphes temporels et des politiques vérifiables

CloudFR

TITLE: Une architecture formelle pour la détection et la contention adaptative des menaces dans des environnements multi-cloud basée sur des graphes temporels et des politiques vérifiables ABSTRACT: L’adoption de stratégies multi-cloud et hybrides s’est consolidée comme pratique dominante dans les secteurs critiques, accroissant la complexité sémantique et opérationnelle des mécanismes de contrôle d’accès et de surveillance de la sécurité. L’hétérogénéité entre AWS IAM, Microsoft Entra ID/Azure RBAC, Google Cloud IAM et les modèles RBAC/ABAC dans Kubernetes, combinée à la fédération d’identités, aux pipelines CI/CD et aux intégrations orientées API, introduit des dépendances temporelles et transversales qui ne sont pas capturées par des analyses locales de politiques. Des rapports récents indiquent que l’usage abusif de crédentiels valides demeure le vecteur prédominant d’incidents, exploitant fréquemment des compositions légitimes de permissions. Nous proposons une architecture formelle pour la détection et la contention adaptative des menaces basée sur des graphes temporels de privilèges et la vérification automatique de politiques via SMT. Nous formalisons l’environnement multi-cloud comme un système dynamique $G_t = (V_t, E_t, \tau_t, w_t, \ell_t)$, en définissant les chemins de compromission, le risque temporel accumulé et le problème dual de détection et de contention comme des instances d’atteignabilité et de coupe minimale sous contraintes fonctionnelles. Nous démontrons des propriétés de correction partielle et une réduction au flot maximum pour une contention minimale. Nous présentons un algorithme incrémental avec une analyse de complexité amortie sous-linéaire sous des hypothèses de parcimonie et de localité temporelle. La contention est validée par l’encodage d’invariants organisationnels en logique du premier ordre décidable, résolue par SMT. Nous implémentons un prototype sous Kubernetes 1.29 avec un backend de graphe et une intégration avec OPA et les taxonomies MITRE ATT&CK. Des évaluations empiriques avec des journaux réels anonymisés et des scénarios synthétiques montrent une réduction statistiquement significative du temps de détection par rapport aux approches basées exclusivement sur la corrélation. Des études de cas dans les secteurs financier et de la santé illustrent la capacité à bloquer des chaînes d’attaque tout en préservant les exigences fonctionnelles. La proposition contribue à la convergence entre la sécurité basée sur l’identité, la vérification formelle et la réponse automatisée dans les écosystèmes multi-cloud contemporains.

  1. Introduction

L’informatique en nuage a évolué d’un paradigme émergent vers une infrastructure fondamentale pour des secteurs critiques tels que la finance, l’énergie, les télécommunications, la santé et l’administration publique. Les stratégies multi‑cloud et hybrides sont largement adoptées afin de réduire la dépendance à un fournisseur, satisfaire aux exigences réglementaires et accroître la résilience opérationnelle (ENISA, 2023; NIST, 2020a). En 2025, la consolidation des plateformes CNAPP (Cloud-Native Application Protection Platform) et leur intégration avec des mécanismes d’observabilité fondés sur eBPF ont encore étendu la surface de surveillance, mais également la complexité systémique.

La coexistence de multiples modèles de contrôle d’accès — AWS IAM, Microsoft Entra ID avec Azure RBAC, Google Cloud IAM et RBAC/ABAC dans Kubernetes — produit une hétérogénéité sémantique et compositionnelle. La fédération d’identités via OIDC/SAML, les intégrations avec des fournisseurs externes et les automatisations orientées infrastructure en tant que code (IaC) introduisent des dépendances croisées non explicitées dans les politiques locales. Par conséquent, la surface d’attaque devient dynamique, distribuée et évolutive dans le temps.

Des rapports largement reconnus indiquent que l’usage abusif d’identifiants valides demeure un vecteur prédominant d’incidents (VERIZON, 2024; IBM, 2024; MANDIANT, 2024). Dans le cadre MITRE ATT&CK, des techniques telles que Valid Accounts (T1078), Account Manipulation (T1098) et Exploitation for Privilege Escalation (T1068) apparaissent fréquemment dans les chaînes d’attaque modernes (MITRE, 2024). Ces données convergent vers un diagnostic structurel : les attaques exploitent souvent des compositions légitimes de permissions plutôt que de dépendre exclusivement de vulnérabilités inconnues.

Des cas tels que Log4Shell (CVE-2021-44228) et Spring4Shell (CVE-2022-22965) illustrent des vecteurs initiaux qui évoluent vers des escalades de privilèges via des identifiants stockés et des rôles mal configurés. Dans les environnements multi‑cloud contemporains, la menace émerge typiquement comme une séquence temporelle d’actions individuellement autorisées, mais globalement non sûres.

Nous formulons trois questions de recherche :

RQ1: Comment représenter formellement les états d’identité et de privilège multi‑cloud tout en préservant la sémantique temporelle et l’interopérabilité ?
RQ2: Sous quelles conditions structurelles est‑il possible de détecter de manière incrémentale des chemins de compromission avec une complexité amortie sous‑linéaire ?
RQ3: Comment garantir que les mécanismes automatiques de confinement éliminent tous les chemins pertinents sans violer les invariants fonctionnels organisationnels ?

Nous contribuons avec : (C1) un modèle formel de graphe temporel de privilèges ; (C2) un algorithme incrémental avec analyse de complexité ; (C3) un mécanisme de confinement avec vérification SMT ; (C4) une évaluation empirique comparative ; (C5) des études de cas intersectorielles.

  1. Contexte et travaux connexes

Les graphes d’attaque ont été formalisés par Ammann, Wijesinghe et Kaushik (2002) comme une représentation des états d’exploitation. Des approches ultérieures ont introduit des réductions symboliques et des analyses incrémentales. Toutefois, la plupart supposent des topologies relativement statiques et n’incorporent pas explicitement des poids temporels avec décroissance exponentielle.

Fireman a démontré la vérification formelle des politiques de pare‑feu (YUAN et al., 2006), établissant un précédent pour la modélisation déclarative des règles. Dans le domaine du raisonnement automatique, le solveur SMT Z3 s’est consolidé comme un outil efficace pour les théories combinées (DE MOURA; BJØRNER, 2008).

Le paradigme Zero Trust (NIST, 2020a) met l’accent sur une évaluation continue fondée sur l’identité et le contexte. NIST SP 800-53 Rev.5 définit des contrôles de sécurité et de confidentialité (NIST, 2020b), tandis que NIST SP 800-207 opérationnalise l’architecture Zero Trust. Des travaux récents abordent la sécurité cloud-native, y compris la protection des workloads et les politiques déclaratives (SHARMA; CHEN, 2022; RED HAT, 2023).

Cependant, nous identifions plusieurs lacunes : (i) absence de formalisation temporelle intégrée entre multiples fournisseurs ; (ii) intégration limitée entre vérification logique et réponse automatisée ; (iii) rareté d’analyses formelles de complexité dans des scénarios multi‑cloud dynamiques.

  1. Threat Model and Problem Formalization

3.1 Modèle de Système

Définition 1 (Environnement Multi‑Cloud).
Soit $C = {c_1,\dots,c_k}$ un ensemble fini de domaines administratifs indépendants. Chaque $c_i$ possède des identités $I_{c_i}$, des ressources $R_{c_i}$ et des politiques $P_{c_i}$. L’état global au temps $t$ est l’union disjointe de ces composants, à laquelle s’ajoutent des relations de fédération $F_{ij}$ entre domaines.

Définition 2 (Graphe Temporel de Privilège).
Pour un instant discret $t \in \mathbb{T}$, nous définissons

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

où $V_t = \bigcup_i (I_{c_i}(t) \cup R_{c_i}(t))$,
$E_t \subseteq V_t \times V_t$ représente des relations d’autorisation ou de dépendance,
$\tau_t: E_t \rightarrow \mathbb{T}$ associe un timestamp,
$w_t: E_t \rightarrow \mathbb{R}^+$ définit un poids de risque,
$\ell_t$ étiquette les arêtes avec un type sémantique (assume-role, read, write, admin, federate).

3.2 Chemins et Risque

Définition 3 (Chemin de Compromission).
Un chemin dirigé $p=(v_0,\dots,v_n)$ est un chemin de compromission si $v_0 \in I_{comp}$ et $v_n \in A$, où $A$ est l’ensemble des actifs critiques.

Définition 4 (Risque Temporel Accumulé).

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

avec $\lambda\in(0,1]$ représentant le facteur de décroissance temporelle.

Le problème de détection consiste à décider :

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

Le problème de confinement consiste à trouver un ensemble minimal $E^- \subseteq E_t$ tel que, dans $G’_t=(V_t,E_t\setminus E^-)$,

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

sous réserve des invariants fonctionnels $F$.

3.3 Propriétés Théoriques

Théorème 1 (Correction Partielle).
Si $E^-$ intercepte tous les chemins minimaux entre $I_{comp}$ et $A$, alors il n’existe aucun chemin minimal résiduel dans $G’_t$.

Preuve.
Supposons par contradiction qu’il existe un chemin minimal résiduel $p^$. Alors $p^$ ne contient aucune arête de $E^-$. Donc $E^-$ n’interceptait pas tous les chemins minimaux, ce qui contredit l’hypothèse. $\square$

La minimalité globale de $E^-$ se réduit au problème de coupe minimale dirigée. Par la construction d’un réseau avec capacité unitaire par arête, nous pouvons appliquer un algorithme de flot maximal, obtenant une complexité $O(|V||E|)$ dans le pire cas en utilisant Edmonds–Karp.

  1. Proposed Methodology

L’architecture est composée de : (i) ingestion de logs via Apache Kafka ; (ii) construction incrémentale de $G_t$ ; (iii) moteur de détection fondé sur une recherche pondérée ; (iv) vérification SMT ; (v) orchestration automatisée compatible avec les API cloud et les contrôleurs Kubernetes.

4.1 Algorithme Incrémental

Lors de l’insertion d’une arête $(u,v)$, nous exécutons une recherche limitée à une profondeur $k$ ou à un seuil de risque $\theta$. Dans des graphes clairsemés avec un degré moyen $d$, l’expansion locale est $O(d^k)$. Si $d$ est borné et $k \ll \log_d |V|$, nous obtenons une complexité amortie sous‑linéaire en $|V|$. Dans le pire cas, l’application de Dijkstra implique $O(|E|\log|V|)$.

4.2 Confinement via SMT

Nous encodons les politiques en logique du premier ordre sur des théories décidables (égalité, tableaux, ensembles finis). Exemple :

$$ \forall x (Role(x) \land Perm(x,\text{s3:})) $$5. Implémentation

Le prototype a été implémenté sur Kubernetes 1.29 (KUBERNETES, 2024), en utilisant Neo4j comme backend de graphe et une intégration avec Open Policy Agent (OPA). Les logs AWS CloudTrail, Azure Monitor Activity Logs et Google Cloud Audit Logs sont normalisés selon les taxonomies MITRE ATT&CK (MITRE, 2024).

Le pipeline opérationnel suit :

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

L’audit suit les directives du NIST SP 800-92 (NIST, 2006) et les contrôles du NIST SP 800-53 Rev.5.

  1. Évaluation expérimentale

Nous avons utilisé des logs réels anonymisés et des chaînes synthétiques alignées sur ATT&CK. Les baselines incluaient une corrélation basée sur des règles et un SIEM traditionnel.

Méthode Temps moyen de détection (s) Violation d’invariants
SIEM traditionnel 42.3 Non applicable
Corrélation par règles 31.7 2 cas
Proposition (sans SMT) 18.4 3 cas
Proposition (avec SMT) 19.1 0

Nous avons appliqué le test de Mann‑Whitney avec $\alpha=0.05$, observant une différence statistiquement significative entre notre approche complète et les baselines ($p<0.01$).

L’analyse d’ablation a indiqué que $\lambda=1$ a augmenté les faux positifs de 14 %, tandis que l’absence de vérification SMT a entraîné des violations fonctionnelles détectables.

  1. Études de cas

7.1 Secteur financier

Chaîne AWS→Azure exploitant T1078. La contention a impliqué la révocation sélective d’une trust policy et l’ajustement d’un rôle fédéré. La coupe minimale a préservé les intégrations de paiement critiques.

7.2 Secteur de la santé

Exploitation d’une application web suivie d’un abus d’un service account Kubernetes avec des permissions excessives. La contention a supprimé la permission cluster-admin tout en préservant les accès cliniques légitimes via un RBAC granulaire.

  1. Discussion

La proposition offre une explicabilité structurelle et une vérifiabilité formelle, contrastant avec des approches purement statistiques basées sur l’apprentissage automatique. En 2025, avec la croissance des attaques assistées par l’IA et l’exploitation automatisée d’identifiants exposés, l’intégration entre modélisation formelle et réponse adaptative devient essentielle.

Les limitations incluent la dépendance à la complétude des logs, la latence d’ingestion et l’absence de couverture des canaux hors bande. La modélisation probabiliste d’adversaires adaptatifs demeure un défi ouvert.

  1. Conclusion et travaux futurs

Nous avons formalisé une architecture basée sur des graphes temporels et la vérification SMT pour la détection et la contention adaptative multi‑cloud. Nous avons démontré une correction partielle, une réduction à une coupe minimale et une analyse de complexité incrémentale. Les évaluations empiriques indiquent des gains significatifs de performance et la préservation des invariants.

Les travaux futurs incluent l’intégration avec une transparence cryptographique basée sur des arbres de Merkle, l’adoption de la cryptographie post‑quantique pour la signature des logs (NIST, 2024) et la modélisation stochastique des menaces adaptatives.

References

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

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

ENISA. Cloud Security Threat Landscape 2023. 2023. Disponible à : https://www.enisa.europa.eu

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

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

MANDIANT. M-Trends 2024. 2024. Disponible à : https://www.mandiant.com/resources/m-trends

MITRE. ATT&CK Framework. 2024. Disponible à : https://attack.mitre.org

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

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

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

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

RED HAT. State of Kubernetes Security Report. 2023. Disponible à : https://www.redhat.com

VERIZON. Data Breach Investigations Report 2024. 2024. Disponible à : 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. Disponible à : https://ieeexplore.ieee.org/document/1610614