spanwich/sel4-ics-gateway-demoDefensive security demo: seL4 microkernel gateway protecting vulnerable ICS from CVE-2019-14462
A defensive security research project comparing protocol-break vs packet-forwarding architectures for protecting industrial control systems from cyber attacks.
Documentation:
- Network Architecture - Network diagrams and traffic flow
- Container Architecture - Docker container relationships
- CVE Explanations - Vulnerability details and attack mechanisms
Modern ICS/SCADA systems face sophisticated attacks like FrostyGoop, which targeted Ukrainian district heating systems via Modbus TCP in January 2024, leaving 600+ households without heat during sub-zero temperatures. Traditional security solutions (firewalls, IDS) use packet-forwarding architectures that inspect traffic in-line but maintain a single TCP connection end-to-end.
This project demonstrates an alternative: a protocol-break gateway using the formally verified seL4 microkernel. By terminating TCP connections and validating protocol semantics before establishing new connections to protected devices, this architecture provides stronger security guarantees.
| Aspect | Protocol-Break (seL4) | Packet-Forwarding (Snort) |
|---|---|---|
| CVE-2019-14462 | BLOCKED (length validation) | DETECTED (Quickdraw rules) |
| CVE-2022-0367 | BLOCKED (address validation) | DETECTED (custom rules) |
| CVE-2022-20685 | IMMUNE (no preprocessor) | VULNERABLE (IDS DoS) |
| CVE-2024-1086 | IMMUNE (no Linux kernel) | VULNERABLE (shares host kernel) |
| Unknown variants | BLOCKED (structural validation) | MISSED (no signature) |
| TCP state attacks | BLOCKED (connection terminated) | Possible |
| Attack surface | ~1,000 LoC (microkernel) | ~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 | Path | Architecture | Protection |
|---|---|---|---|
| 502 | Client → seL4 → PLC | Protocol-break | Validates Modbus structure |
| 503 | Client → Snort → PLC | Packet-forwarding | Rule-based IDS |
| 5020 | Client → PLC (ASAN) | Direct | CVE-2022-0367 mode |
| 5022 | Client → PLC | Direct | CVE-2019-14462 mode (profile: cve14462) |
Note: The default PLC now runs in CVE-2022-0367 mode with ASAN. Use
--profile cve14462for CVE-2019-14462 testing.
The PLC uses intentionally vulnerable libmodbus 3.1.2. The attack exploits trusted MBAP length fields:
# 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
A bounds-checking bug in modbus_mapping_new_start_address() allows heap underflow via function code 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
Technical Details:
start_registers=100, valid addresses are 100-109write_address < 100, causing negative array indexmb_mapping struct fields including pointersSnort 2.9.18 has an integer overflow in its Modbus preprocessor that causes an infinite loop, completely blocking all traffic through the 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
# 3. Verify Snort is frozen (should timeout with NO response)
echo -ne '\x00\x01\x00\x00\x00\x06\x01\x03\x00\x00\x00\x01' | nc -w 5 localhost 503 | xxd
# 4. Check Snort CPU (should be 100%)
sudo docker exec ics-snort top -b -n 1 | grep snort
# 5. seL4 is IMMUNE (no Modbus preprocessor to exploit)
./cve_20685_attack 127.0.0.1 502 # No effect on seL4
# 6. Restart Snort after demo
sudo docker compose restart snort