spanwich/sel4-ics-gateway-demoDémonstration de sécurité défensive : passerelle seL4 microkernel protégeant les ICS vulnérables de CVE-2019-14462
Un projet de recherche défensive en cybersécurité comparant les architectures protocol-break et packet-forwarding pour la protection des systèmes de contrôle industriels contre les cyberattaques.
Documentation :
- Architecture réseau - Schémas réseau et flux de trafic
- Architecture des conteneurs - Relations entre les conteneurs Docker
- Explications des CVE - Détails des vulnérabilités et mécanismes d'attaque
Les systèmes ICS/SCADA modernes sont confrontés à des attaques sophistiquées comme FrostyGoop, qui a ciblé les systèmes de chauffage urbain ukrainiens via Modbus TCP en janvier 2024, privant plus de 600 foyers de chauffage par des températures négatives. Les solutions de sécurité traditionnelles (pare-feux, IDS) utilisent des architectures packet-forwarding qui inspectent le trafic en ligne mais maintiennent une seule connexion TCP de bout en bout.
Ce projet démontre une alternative : une passerelle protocol-break utilisant le micro-noyau formellement vérifié seL4. En terminant les connexions TCP et en validant la sémantique du protocole avant d'établir de nouvelles connexions vers les appareils protégés, cette architecture offre de meilleures garanties de sécurité.
| Aspect | Protocol-Break (seL4) | Packet-Forwarding (Snort) |
|---|---|---|
| CVE-2019-14462 | BLOQUÉ (validation de longueur) | DÉTECTÉ (règles Quickdraw) |
| CVE-2022-0367 | BLOQUÉ (validation d'adresse) | DÉTECTÉ (règles personnalisées) |
| CVE-2022-20685 | IMMUNISÉ (pas de préprocesseur) | VULNÉRABLE (DoS IDS) |
| CVE-2024-1086 | IMMUNISÉ (pas de noyau Linux) | VULNÉRABLE (partage le noyau hôte) |
| Variantes inconnues | BLOQUÉ (validation structurelle) | MANQUÉ (aucune signature) |
| Attaques d'état TCP | BLOQUÉ (connexion interrompue) | Possible |
| Surface d'attaque | ~1 000 LoC (micro-noyau) | ~500 000 LoC (Linux + Snort) |
┌─────────────────────────────────────────────────────────────────────────────┐
│ Docker Network: ics-untrusted (192.168.96.0/24) │
│ │
│ ┌───────────────────────┐ ┌───────────────────────┐ │
│ │ seL4 Gateway │ │ Snort IDS │ │
│ │ Port 502 │ │ Port 503 │ │
│ │ │ │ │ │
│ │ • Protocol-break │ │ • Packet-forwarding │ │
│ │ • TCP termination │ │ • Inline inspection │ │
│ │ • Length validation │ │ • Rule-based detection│ │
│ └───────────┬───────────┘ └───────────┬───────────┘ │
│ │ │ │
├───────────────┼───────────────────────────────┼─────────────────────────────┤
│ Docker Network: ics-protected (192.168.95.0/24) │
│ │ │ │
│ └───────────────┬───────────────┘ │
│ ▼ │
│ ┌───────────────────────────────┐ │
│ │ PLC (District Heating) │ │
│ │ Vulnerable libmodbus 3.1.2 │ │
│ │ Port 5020 (direct access) │ │
│ └───────────────────────────────┘ │
└─────────────────────────────────────────────────────────────────────────────┘
# Place your seL4 kernel image at:
gateway/sel4-image/capdl-loader-image-arm-qemu-arm-virt
# Build all containers
sudo docker compose build
# Start individual containers
sudo docker compose up plc # PLC only
sudo docker compose up gateway # seL4 gateway + PLC
sudo docker compose up snort # Snort IDS + PLC
# Start all
sudo docker compose up
# Through seL4 gateway (protected - protocol-break)
echo -ne '\x00\x01\x00\x00\x00\x06\x01\x03\x00\x00\x00\x01' | nc localhost 502 | xxd
# Through Snort IDS (protected - packet-forwarding)
echo -ne '\x00\x01\x00\x00\x00\x06\x01\x03\x00\x00\x00\x01' | nc localhost 503 | xxd
# Direct to PLC (unprotected - vulnerable)
echo -ne '\x00\x01\x00\x00\x00\x06\x01\x03\x00\x00\x00\x01' | nc localhost 5020 | xxd
| Port | Chemin | Architecture | Protection |
|---|---|---|---|
| 502 | Client → seL4 → PLC | Protocol-break | Valide la structure Modbus |
| 503 | Client → Snort → PLC | Packet-forwarding | IDS basé sur des règles |
| 5020 | Client → PLC (ASAN) | Direct | Mode CVE-2022-0367 |
| 5022 | Client → PLC | Direct | Mode CVE-2019-14462 (profil : cve14462) |
Remarque : Le PLC par défaut fonctionne maintenant en mode CVE-2022-0367 avec ASAN. Utilisez
--profile cve14462pour les tests CVE-2019-14462.
Le PLC utilise libmodbus 3.1.2 intentionnellement vulnérable. L'attaque exploite les champs de longueur MBAP fiables :
# Start PLC in CVE-2019-14462 mode
sudo docker compose --profile cve14462 up plc-14462
# Build attack tools
cd cve_tools && make
# Attack unprotected PLC (crashes)
./cve_14462_attack 127.0.0.1 5022
# Attack through seL4 (BLOCKED)
./cve_14462_attack 127.0.0.1 502
# Attack through Snort (DETECTED by Quickdraw rules)
./cve_14462_attack 127.0.0.1 503
Un bogue de vérification des limites dans modbus_mapping_new_start_address() permet un sous-débordement de tas via le code fonction 0x17 (Write and Read Registers) :
# Default PLC runs in CVE-2022-0367 mode with ASAN
sudo docker compose up plc
# Build attack tools
cd cve_tools && make
# Attack PLC - ASAN will detect heap-buffer-overflow
./cve_0367_attack 127.0.0.1 5020
# Attack with custom parameters
./cve_0367_attack 127.0.0.1 5020 88 0x4141 # Corrupt tab_registers pointer
./cve_0367_attack 127.0.0.1 5020 72 0xFFFF # Corrupt nb_registers
# Attack through seL4 (BLOCKED - address validation)
./cve_0367_attack 127.0.0.1 502
# Attack through Snort (DETECTED by custom rules)
./cve_0367_attack 127.0.0.1 503
Détails techniques :
start_registers=100, les adresses valides sont 100-109write_address < 100, provoquant un index de tableau négatifmb_mapping, y compris les pointeursSnort 2.9.18 présente un dépassement d'entier dans son préprocesseur Modbus qui provoque une boucle infinie, bloquant complètement tout le trafic à travers l'IDS :
# 1. Verify Snort is working (should return Modbus response)
echo -ne '\x00\x01\x00\x00\x00\x06\x01\x03\x00\x00\x00\x01' | nc -w 2 localhost 503 | xxd
# 2. Attack the Snort IDS
./cve_20685_attack 127.0.0.1 503