spanwich/sel4-ics-gateway-demoDemonstração de segurança defensiva: gateway de microkernel seL4 protegendo ICS vulneráveis contra CVE-2019-14462
Um projeto de pesquisa defensiva em segurança que compara arquiteturas protocol-break vs packet-forwarding para proteger sistemas de controle industrial contra ataques cibernéticos.
Documentação:
- Arquitetura de Rede - Diagramas de rede e fluxo de tráfego
- Arquitetura de Contêineres - Relações entre contêineres Docker
- Explicações de CVE - Detalhes de vulnerabilidades e mecanismos de ataque
Os sistemas modernos de ICS/SCADA enfrentam ataques sofisticados como o FrostyGoop, que teve como alvo sistemas ucranianos de aquecimento distrital via Modbus TCP em janeiro de 2024, deixando mais de 600 residências sem aquecimento durante temperaturas abaixo de zero. As soluções de segurança tradicionais (firewalls, IDS) usam arquiteturas packet-forwarding que inspecionam o tráfego em linha, mas mantêm uma única conexão TCP de ponta a ponta.
Este projeto demonstra uma alternativa: um gateway protocol-break usando o microkernel seL4 formalmente verificado. Ao encerrar conexões TCP e validar a semântica do protocolo antes de estabelecer novas conexões com os dispositivos protegidos, essa arquitetura oferece garantias de segurança mais fortes.
| Aspecto | Protocol-Break (seL4) | Packet-Forwarding (Snort) |
|---|---|---|
| CVE-2019-14462 | BLOQUEADO (validação de comprimento) | DETECTADO (regras Quickdraw) |
| CVE-2022-0367 | BLOQUEADO (validação de endereço) | DETECTADO (regras personalizadas) |
| CVE-2022-20685 | IMUNE (sem preprocessador) | VULNERÁVEL (DoS no IDS) |
| CVE-2024-1086 | IMUNE (sem kernel Linux) | VULNERÁVEL (compartilha o kernel do host) |
| Variantes desconhecidas | BLOQUEADO (validação estrutural) | NÃO DETECTADO (sem assinatura) |
| Ataques de estado TCP | BLOQUEADO (conexão encerrada) | Possível |
| Superfície de ataque | ~1.000 linhas de código (microkernel) | ~500.000 linhas de código (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
| Porta | Caminho | Arquitetura | Proteção |
|---|---|---|---|
| 502 | Cliente → seL4 → PLC | Protocol-break | Valida a estrutura Modbus |
| 503 | Cliente → Snort → PLC | Packet-forwarding | IDS baseado em regras |
| 5020 | Cliente → PLC (ASAN) | Direto | Modo CVE-2022-0367 |
| 5022 | Cliente → PLC | Direto | Modo CVE-2019-14462 (perfil: cve14462) |
Nota: O PLC padrão agora executa no modo CVE-2022-0367 com ASAN. Use
--profile cve14462para testes do CVE-2019-14462.
O PLC usa a libmodbus 3.1.2 intencionalmente vulnerável. O ataque explora campos de comprimento MBAP confiáveis:
# 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
Um bug de verificação de limites em modbus_mapping_new_start_address() permite subfluxo de heap por meio do código de função 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
Detalhes Técnicos:
start_registers=100; os endereços válidos são 100-109write_address < 100, causando um índice de array negativomb_mapping, incluindo ponteirosO Snort 2.9.18 tem um estouro de inteiro em seu preprocessador Modbus que causa um loop infinito, bloqueando completamente todo o tráfego que passa pelo 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