Signal
No commercial platform formally verifies industrial control systems. Dragos detects. Claroty monitors. Signal proves. Signal applies Z3 formal verification to PLC ladder logic, SCADA control loops, and industrial protocol parsers — producing machine-verifiable safety certificates for the systems that keep reactors stable, pipelines flowing, and power grids online. When the CNSC requires a formal safety case, Signal generates it. When a pipeline operator needs proof that a pressure control loop cannot exceed design limits under any reachable input, Signal proves it. This is not a security scanner. It is an industrial certification engine — the first of its kind.
- PLC Ladder Logic / Structured Text / Function Block Diagram (IEC 61131-3)
- SCADA configuration + process variable definitions (pressure, flow, temperature bounds)
- Industrial protocol implementation source — Modbus, DNP3, IEC 61850, OPC-UA
- Control loop specification + safety invariants
- Optional: CODESYS runtime C source for deep static analysis
- Process variable bounds — pressure, temperature, flow cannot exceed design limits under any reachable PLC state
- Control loop termination — PERFORM UNTIL / scan cycle cannot diverge
- Ladder logic rung reachability — dead rungs and unreachable safety interlocks formally identified
- Protocol parser arithmetic — integer overflow in Modbus register parsing, DNP3 length fields
- Safety interlock reachability — emergency shutdown logic cannot be bypassed under adversarial input sequence
- State machine invariants — process cannot enter undefined or dangerous state under formal attacker model
- Z3 formal safety certificate per invariant (machine-verifiable)
- Control loop reachability proof — states that cannot be entered under any input
- Protocol parser overflow witness values (exact attacker-controlled bytes)
- CNSC-formatted formal safety case document
- Remediation path with re-verification of fix
Natural gas pipeline — Modbus register overflow bypasses pressure safety interlock
register_addr: uint16 = 0xFFFF + offset 1 → wraps to 0x0000 → reads safety interlock register as process data → emergency shutdown logic unreachable| # | Target | Vulnerability Class | Status |
|---|---|---|---|
| 01 | libmodbus 3.1.x Integer Overflow | Integer Overflow | CVE Filed |
| 02 | CANDU PLC Logic Safety Interlock | Safety Interlock | Formal Case |
| 03 | Hydro-Québec SCADA Control Loop | Control Loop | Target |
Formal engagement starts with a technical intake. We scope, configure, and deliver a proof artifact within the agreed SLA.