Hierarchical Security Monitoring for Edge-IoT: A Formal Methods Approach

Cyber resiliency in edge-IoT deployments is fundamentally an economic problem: detection must keep critical processes operating under attack, but defender resources (compute, bandwidth, operator attention) are bounded. Centralised cloud monitoring offers expressive cross-device detection at prohibitive bandwidth cost; purely edge-local monitoring is cheap but blind to coordinated multi-device attacks where the asymmetric balance favours the attacker. We propose a lightweight hierarchical security-monitoring framework, built on formal runtime-verification methods, that occupies the practical middle ground at quantified cost. Each edge device runs a lightweight TeSSLa stream specification (size, payload validity, rate, and timestamp-drift predicates) that emits a four-valued verdict per aggregation window at sub-microsecond per-event cost; the gateway runs a parametric first-order MonPoly monitor over the per-device verdict streams at microsecond-scale per-verdict cost. The edge-to-gateway uplink carries roughly one Boolean per aggregation window per node, orders of magnitude smaller than the raw packet stream. The gateway tier detects coordinated attack patterns that no single-node monitor can see, shifting the asymmetric cost balance toward the defender. Every alert carries a witness set naming the device, the monitor tier, and the predicate that fired, providing an auditable record of the decision. We evaluate the framework on a container-host testbed spanning nominal and attacker nodes across four attack classes (buffer overflow, time spoofing, denial-of-service, and mixed advanced-persistent-threat patterns), and describe the edge- and gateway-tier specifications together with the cost-versus-coverage trade-off as monitor levels are added.