Hierarchical Security Monitoring for Edge-IoT: A Formal Methods Approach
Hierarchical TeSSLa and MonPoly monitors detect cross-device edge-IoT attacks while sending only compact verdicts upstream.
The paper presents a hierarchical runtime-verification monitor that keeps edge-IoT detection cheap while still seeing coordinated multi-device attacks. Each device runs a lightweight TeSSLa specification over size, payload validity, rate, and timestamp drift, emitting a four-valued verdict per window at sub-microsecond per-event cost. A gateway MonPoly monitor consumes those verdicts at microsecond scale, and the uplink carries roughly one Boolean per aggregation window per node rather than raw packets. A container testbed covered buffer overflow, time spoofing, denial of service, and mixed APT patterns, and every alert includes a witness naming the device, tier, and predicate.