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

I. INTRODUCTION

• Edge-only monitors are inexpensive and operate at line rate but cannot detect attacks coordinated across devices; cloud monitors incur bandwidth and latency costs and cannot enforce local properties at line rate.Single-trace edge monitors cannot express parametric correlation across independent device traces, while processing every raw packet at the gateway is bandwidth- and compute-prohibitive.Source: §I · pp. 1–2
• The framework composes lightweight single-property edge monitors with a parametric first-order gateway monitor using a formal four-valued algebra and witness sets.The realization uses TeSSLa at the edge and MonPoly at the gateway.Source: §I · pp. 1–2
• Three of four attack classes—overflow, time spoofing, and denial-of-service—are caught at the edge; mixed APT is only presumptively flagged per node and confirmed by gateway correlation.The evaluation uses a 12-actor dataset with five nominal nodes and seven attackers.Source: §I · p. 1
• The framework reduces the uplink to roughly one Boolean per node per aggregation window, far less than the raw stream required by a cloud correlator.The stated cost profile is microsecond-scale monitoring and O(1) witness sets per alert.Source: §I · p. 2
• The threat model allows compromise of up to K of N devices but assumes attestation or isolation handles binary compromise, gateway-timestamp tampering, and direct sidecar interference.The adversary may control outbound streams within physical-channel limits and coordinate intermittent behavior.Source: §I · p. 2
• Mixed-APT actors behave nominally about 60% of the time, so the gateway detects their pattern by correlating three independent ⊥p verdicts within a 60 s window.The gateway rule uses parametric quantification over nodes and a bounded-past ONCE condition.Source: §I · p. 2

II. SPECIFICATION AND COMPOSITION

• The engine-independent framework specification is a pair Φ = ⟨φL1, φL2⟩ in past-time first-order temporal logic, applied to typed packet events and per-window verdict events.The verdict domain is V4 = {⊤, ⊤p, ⊥p, ⊥}.Source: §II · p. 2

A. Two-level specification

• Each device evaluates four single-property predicates per event, with violations corresponding to overflow, fuzzing, time spoofing, or denial of service.The supplied predicate definitions specify size_ok as actual_sent ≤ buffer_limit, fuzz_ok as actual_sent > 0, and mono_ok as turn ≥ prev_turn − τjit.Source: A. Two-level specification · p. 2
• For each device and aggregation window, L1 counts events that violate any predicate and also counts near-rate-threshold events.The aggregation window is Wagg; sh counts events whose inter-arrival is within 50% of the rate threshold.Source: A. Two-level specification · pp. 2–3
• L1 maps window counts to four-valued verdicts: at least Nhard violations yield ⊥, one or more fewer violations yield ⊥p, and a sufficiently large near-rate burst without violations yields ⊤p.Otherwise, L1 emits ⊤; the listed testbed operating point sets Nhard to 3 and Wagg to 5 s.Source: A. Two-level specification · pp. 2–3
• The gateway baseline fires when three distinct devices each emit at least one presumptive-unsat verdict in the bounded past-time window Wp, detecting a cross-device pattern invisible to any single-device monitor.The robust variant requires each contributing actor to emit at least k presumptive-unsat verdicts in the past Wpast; k=3 on the 12-actor trace and k=2 on the 15-actor replay.Source: A. Two-level specification · p. 3

B. Composition algebra

• The composed verdict is the pointwise meet of the two tier verdicts, with ⊥ dominating and ⊤ confirming; composition unions level- and node-tagged witness sets.For example, ⊥p ⊗ ⊥ yields ⊥, while ⊥p ⊗ ⊥p yields ⊥p; the stated soundness lemma links a composed ⊥ to a joint-trace violation and witness sub-trace.Source: B. Composition algebra · p. 3
• Single-node attacks are caught at L1, while coordinated APT patterns rely on an L2 ⊥ verdict after predominantly ⊥p verdicts at individual devices.The passage identifies NODE-5/6/7 for single-node attacks and NODE-8/9/10 for coordinated APT.Source: B. Composition algebra · p. 3
• Each of N edge containers converts raw packets into a four-valued verdict per window, and the gateway hosts L2, the composer, and the shield.The uplink carries one Boolean per window per node.Source: Figure 1 · p. 3

III. RUNTIME ARCHITECTURE

• The implementation realizes the engine-agnostic L1 and L2 specifications with TeSSLa and MonPoly, respectively, using the parameters defined in Section II-A.The passage identifies the TeSSLa stream program as Listing 1 and the MonPoly MFOTL program as Listing 2.Source: §III · p. 3
• The evaluation implements both tiers as separate Docker containers on one host, while physical Raspberry Pi per-event latency is left for follow-up.The described deployment topology puts the gateway one network hop above the devices.Source: §III · p. 3
• Each device’s L1 TeSSLa process inspects its outbound packet stream alongside the network stack, and one gateway L2 process consumes aggregated per-node verdict streams.The gateway receives one Boolean per window per node.Source: §III · p. 3

A. Event canonicalisation

• A Python adapter parses JSONL into typed packet events, groups them by actor for L1, and translates verdicts into one-argument MonPoly events per actor-window pair.The declared signature includes actor-keyed sat, psat, punsat, and unsat predicates, plus edge_block and coordinated_apt_alert predicates.Source: A. Event canonicalisation · p. 3
• The gateway rule maps an unsat verdict to edge_block and defines a robust coordinated-APT alert using repeated punsat verdicts from three nodes within the bounded past window.The listing identifies ONCE[0,60s] as the bounded-past operator, with quantifiers ranging over observed nodes.Source: A. Event canonicalisation · p. 4

B. Concrete L1 and L2 specifications

• Four single-property L1 invariants run in parallel, with their per-event conjunction aggregated over a five-second window into a four-valued verdict sent to the gateway.The verdict is sampled before transmission.Source: B. Concrete L1 and L2 specifications · p. 4
• L2 consumes per-actor ⊥p verdict events and detects coordinated-APT correlation; its robust rule requires each contributing node to emit ⊥p at least k times within 60 seconds.The recommended k is 3 on the 12-actor trace; k=2 is shown in the specification.Source: B. Concrete L1 and L2 specifications · p. 4
• The composer applies the verdict lattice pointwise, unions witness sets, and emits verdict, witnesses, and evidence; the shield maps verdicts to block, confirm, or allow actions.Event-verdict pairs can be appended to a hash-chained audit log; that mechanism was described but not evaluated.Source: B. Concrete L1 and L2 specifications · p. 4

IV. EVALUATION AND METHODOLOGY

• The methodology is described in enough detail for independent reproduction on the 12-actor dataset.Source: §IV · p. 4

A. Dataset and testbed

• The Docker testbed emulates Raspberry-Pi-class edge devices communicating with a separate gateway, but runs uncapped containers on one workstation-class host.The reported L1 timings are host-relative; physical Raspberry Pi timing with the primary workload sharing the device is left for follow-up.Source: A. Dataset and testbed · p. 4
• Each JSON event records a gateway-observed timestamp, actor, tool, and payload size and bound, supporting checks for oversize payloads, non-monotone timestamps, and short inter-arrival times.Source: A. Dataset and testbed · p. 4
• The 12 actors include nominal nodes, overflow, time-spoofing, and denial-of-service attackers, plus three mixed-APT nodes that behave nominally about 60% of the time.Mixed-APT violations are sampled independently across the three nodes.Source: A. Dataset and testbed · p. 4
• Single-node attack classes cross L1 thresholds, while three mixed-APT nodes contribute only eleven sparse ⊥p verdicts and one ⊥ that jointly trigger L2.Source: A. Dataset and testbed · p. 4
• Three trace bundles, each run three times, validate L1, validate L2 on mixed-APT traces, and measure false positives on nominal traces.Source: A. Dataset and testbed · p. 4

C. Metrics and protocol

• Detection rate is the fraction of attack windows emitting a non-sat verdict; the protocol also measures clean-actor false-positive rate and per-event L1 and per-verdict L2 cost.Offline replay compares composed verdicts and witnesses with ground-truth labels.Source: C. Metrics and protocol · p. 5

D. Measured results

• L1+L2 detects 14/16 coordinated-APT windows, versus 12/16 for L1-only; only L1 covers all three single-node classes simultaneously.Table II summarizes detection and false-positive rates by configuration on the 12-actor trace and 15-actor replay.Source: D. Measured results · p. 5, Table II · p. 5

B. Baselines

• The single-signal baselines catch only selected attacks: token-bucket catches DoS (7/7) and partial time-spoofing (2/4), while size cap catches overflow (15/15).Naive AND matches L1 per window but is two-valued and cannot drive the gateway's four-valued rule.Source: D. Measured results · p. 5

D. Measured results

• False-positive rate stays invariant across ρmin values of 0.3, 0.5, and 0.7 seconds because all eight clean-node PUNSAT windows arise from coincident integer-second event pairs.Changing aggregation windows from 5 to 2 seconds reduces FPR from 24% to 14%; 10–30-second windows raise it to 32–50%. Time-spoof detection remains 50%.Source: D. Measured results · p. 5
• With k=3, all six L2 alerts contain three real attackers and no clean contributors on this trace; L1+L2 covers 14/16 attacker windows by recovering two L1 misses.L1 costs 0.52 µs per event (p95 0.67 µs) and L2 about 1 µs per verdict; L2 cost at N=1000 is unmeasured.Source: D. Measured results · p. 5

• Three additional classes—stealth overflow, fuzzing, and pulsing DoS—are detected by existing L1 primitives without architectural change.The size, fuzz_ok, and rate predicates detect the respective patterns.Source: E. Second-generation replay · p. 5
• The clean-actor false-positive rate falls to 1/23 (≈4%) on the fresh trace, where same-second-collision artifacts are absent.The passage attributes the original artifacts to the data-collection layer.Source: E. Second-generation replay · p. 5
• The robust L2 variant reaches all-true alerts at k=2 on the replay, versus k=3 on the 12-actor trace, making the recommended operating point data-dependent.At k=2 there are 6 alerts, all true; the comparison trace has 3 all-true alerts at k=3, against 15 baseline alerts (7 true / 8 mixed).Source: E. Second-generation replay · p. 5

V. RELATED WORK

• The related-work discussion replaces propositional spatial operators in hierarchical monitoring with parametric first-order MFOTL for cross-node correlation.It also presents learned classifiers as complementary to L1 and identifies the lack of numerical cost models in established resiliency frameworks.Source: §V · p. 6

VI. DISCUSSION

• The evaluation uses a synthetic 12-actor dataset and a closed set of four attack classes; heavier-tailed real-world mixes would need additional predicates or threshold tuning.Future directions include physical Raspberry-Pi timing, live closed-loop deployment, and hardening against adaptive adversaries.Source: §VI · p. 6

VII. CONCLUSION

• The composed monitor catches every single-node attack window caught by any baseline and detects coordinated mixed-APT patterns no single-tier baseline can express.On the 12-actor testbed, L1 costs sub-microsecond per event, L2 costs microseconds per verdict, and the uplink is four orders of magnitude smaller than the raw packet stream.Source: §VII · p. 6