spanwich/sel4-ics-gateway-demoDemostración de seguridad defensiva: puerta de enlace del micronúcleo seL4 protegiendo ICS vulnerables de CVE-2019-14462
Un proyecto de investigación de seguridad defensiva que compara las arquitecturas de ruptura de protocolo vs reenvío de paquetes para proteger sistemas de control industrial de ciberataques.
Documentación:
- Arquitectura de red - Diagramas de red y flujo de tráfico
- Arquitectura de contenedores - Relaciones entre contenedores Docker
- Explicaciones de CVE - Detalles de vulnerabilidad y mecanismos de ataque
Los sistemas ICS/SCADA modernos enfrentan ataques sofisticados como FrostyGoop, que atacó sistemas de calefacción urbana ucranianos a través de Modbus TCP en enero de 2024, dejando a más de 600 hogares sin calefacción durante temperaturas bajo cero. Las soluciones de seguridad tradicionales (firewalls, IDS) utilizan arquitecturas de reenvío de paquetes que inspeccionan el tráfico en línea pero mantienen una única conexión TCP de extremo a extremo.
Este proyecto demuestra una alternativa: un gateway de ruptura de protocolo que utiliza el microkernel seL4 formalmente verificado. Al terminar las conexiones TCP y validar la semántica del protocolo antes de establecer nuevas conexiones a los dispositivos protegidos, esta arquitectura proporciona garantías de seguridad más sólidas.
| Aspecto | Ruptura de protocolo (seL4) | Reenvío de paquetes (Snort) |
|---|---|---|
| CVE-2019-14462 | BLOQUEADO (validación de longitud) | DETECTADO (reglas Quickdraw) |
| CVE-2022-0367 | BLOQUEADO (validación de dirección) | DETECTADO (reglas personalizadas) |
| CVE-2022-20685 | INMUNE (sin preprocesador) | VULNERABLE (DoS del IDS) |
| CVE-2024-1086 | INMUNE (sin kernel Linux) | VULNERABLE (comparte kernel del host) |
| Variantes desconocidas | BLOQUEADO (validación estructural) | NO DETECTADO (sin firma) |
| Ataques al estado TCP | BLOQUEADO (conexión terminada) | Posible |
| Superficie de ataque | ~1,000 LdC (microkernel) | ~500,000 LdC (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
| Puerto | Ruta | Arquitectura | Protección |
|---|---|---|---|
| 502 | Cliente → seL4 → PLC | Ruptura de protocolo | Valida estructura Modbus |
| 503 | Cliente → Snort → PLC | Reenvío de paquetes | IDS basado en reglas |
| 5020 | Cliente → PLC (ASAN) | Directo | Modo CVE-2022-0367 |
| 5022 | Cliente → PLC | Directo | Modo CVE-2019-14462 (perfil: cve14462) |
Nota: El PLC por defecto ahora se ejecuta en modo CVE-2022-0367 con ASAN. Use
--profile cve14462para pruebas de CVE-2019-14462.
El PLC usa libmodbus 3.1.2 intencionalmente vulnerable. El ataque explota campos de longitud MBAP confiados:
# 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 error de verificación de límites en modbus_mapping_new_start_address() permite un subdesbordamiento de heap a través del código de función 0x17 (Escribir y Leer Registros):
# 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
Detalles técnicos:
start_registers=100, las direcciones válidas son 100-109write_address < 100, causando un índice de array negativomb_mapping, incluidos punterosSnort 2.9.18 tiene un desbordamiento de enteros en su preprocesador Modbus que provoca un bucle infinito, bloqueando completamente todo el tráfico a través del 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