Hybrid Hierarchical Runtime Verification for Edge-IoT Security: Combining MonPoly and RTLola

• Per-node monitors cannot see coordinated attacks, while sending every event to the cloud restores fleet visibility at the cost of bandwidth and detection latency.An attacker who compromises a device, sends one malicious request, and goes quiet can leave an event-triggered monitor with nothing to evaluate.Source: §1 · p. 2
• The edge canonicalises events, the gateway aggregates short per-device windows, and the cloud pairs MonPoly correlation with RTLola time-triggered silent-node detection.MonPoly handles coordinated overflow and per-device APT, escalation, and persistent-campaign patterns; RTLola emits a verdict at a deadline even without input.Source: §1 · p. 2
• The evaluation spans eight attack profiles: single-node attacks are caught at the edge and gateway, while multi-vector APT, persistent campaigns, and silent bypass require the hybrid cloud tier.Source: §1 · p. 2
• Under the adopted single-device gateway abstraction, no per-device rule can decide a property that quantifies over two distinct devices.The paper identifies this as a formal necessity for coordinated cross-device detection below the cloud.Source: §1 · p. 3
• Mean monitoring cost is ∼57 µs per event at the edge and ∼710 µs at the gateway; gateway-to-cloud alerts are roughly 7× smaller than edge input, with cloud latency around 1.7 s.The silent-node detector adds a fixed five-second window.Source: §1 · p. 3
• The adversary may compromise edge monitors and know the framework’s thresholds and cloud property catalogue, while supply-chain compromise and gateway-timestamp tampering are out of scope.Source: §1 · p. 3
• The framework specifies thirteen properties across three tiers to cover eight attack classes plus a silent-bypass scenario, and is instantiated on a 15-actor Docker testbed.The cloud runs four MonPoly processes alongside one RTLola time-triggered process.Source: §1 · p. 3

• The eight profiles are emulated across 15 Docker containers, with five clean baselines and ten attackers; AS1 is a behaviour of existing attackers, not a separate node.Source: §2 · p. 4
• Single-event classes A2, A3, and A6 map to L1 per-event predicates; time-windowed A4, A5, and A7 map to L2 sliding counts.Source: §2 · p. 4
• The multi-vector class A8 maps to L3 parametric quantification, logically necessary for P3.2 under the single-device gateway abstraction; silent-bypass AS1 maps to time-triggered P3.5.Source: §2 · p. 4

3 Three-Layer Specification

• The framework formalizes per-event L1, per-window-per-device L2, and multi-device past-time L3 specifications, with outputs composed as a streaming pipeline.Each layer adds temporal or cross-device patterns unavailable at the preceding data granularity.Source: §3 · p. 4, §3.3 · p. 7

3.2 Per-layer property specifications

• L1 uses four memoryless predicates for buffer overflow, time spoofing, content fuzzing, and the residual safe-tx category.Fuzzing checks payload well-formedness, while oversized payloads belong to the separate overflow class.Source: §3.2 · p. 5

3.1 Event schema

• Each raw event becomes exactly one of four canonical events; safe-tx is the residual category, not a positive assertion that the transaction is verified safe.The schema maps canonical events into gateway alerts and cloud incidents; for example, three overflows within 30 seconds raise an overflow alert.Source: §3.2 · p. 5, §3.1 · p. 5

3.2 Per-layer property specifications

• L2 counts per-device events in short sliding windows: three overflows within 30 seconds, 30 spam events, or 15 pulsing events within 2 seconds trigger alerts.Time anomalies and fuzz events trigger immediate alerts.Source: §3.2 · pp. 5–6
• MonPoly runs four event-triggered cloud properties, while RTLola handles the time-triggered silent-node anomaly and emits its verdict at the 5-second window closure without input.Under total fleet silence, MonPoly’s event-triggered clock stalls; RTLola bounds detection natively at the window length.Source: §3.2 · p. 6, Table 2 · p. 7

3.3 Hierarchical composition

• Under the single-device gateway abstraction, P3.2’s distinct-device overflow correlation cannot be decided by any per-device rule, making cloud placement necessary for that property.A multi-device gateway could express P3.2 with O(N) state, but placement of P3.1, P3.3, and P3.4 at the cloud is an engineering choice, not a logical necessity.Source: §3.3 · p. 8

4 Runtime Architecture

• Of 6,861 L2 outputs, 941 were security alerts; forwarded safe-transaction events dominated measured inter-tier traffic.The alert subset alone was smaller than the L1 input.Source: §4 · p. 8
• L1 emits one canonical event per input, and L2 maintains per-device sliding-window deques for overflow, spam, and pulsing checks before JSON-serializing outputs to L3.L1 evaluates its four predicates in priority order.Source: §4 · p. 8
• The reference layout places L1 and L2 in a monitor container connected by a Unix pipe and L3 in a separate correlator container, mapping directly to edge, gateway, and cloud roles.L1 classifies each event in constant time; L2 aggregates 5–30-second windows and forwards alerts and safe-transaction events to L3.Source: §4 · p. 8, Figure 1 · p. 9
• L3 runs four persistent MonPoly processes for P3.1–P3.4 and one RTLola process for P3.5, deduplicating outputs before logging incidents with engine and severity tags.The orchestrator’s filtering, translation, subprocess management, and verdict aggregation can accommodate another RV engine given its predicate subset, encoding, and output regex.Source: §4 · p. 9

5.1 Dataset

• Fifteen emulated actors—five clean and ten attackers—cover eight profiles in 17 Docker containers on a single M1 host.The packaged testbed records traces for reproducible evaluation.Source: §5.1 · pp. 9–10, §5 · p. 9

5.2 Aggregate workload

• 72 of 6,872 raw events are lost before L1; L2 emits 941 alerts and 5,920 safe forwards, while L3 emits 137 incidents.L1 processes the 6,800 events it receives, and the 600 s run is summarized in Table 4.Source: §5.2 · p. 10, Table 4 · p. 11

5.3 L3 incident detection

• All 137 device-attributable incidents correspond to attacker-labelled devices, with 100% witness completeness.P3.1 fires on four mixed-APT nodes, P3.4 on six attackers, and P3.5 yields 30 incidents across five silent devices.Source: §5.3 · p. 11, Table 6 · p. 12

5.4 Ablation: contribution of each layer

• MonPoly adds 107 multi-event or multi-device incidents, and RTLola adds 30 silent-node detections that MonPoly alone cannot detect within a bounded delay.Removing the MonPoly tier loses P3.1–P3.4 detections; removing RTLola loses P3.5 detections.Source: §5.4 · p. 12

5.5 Computational cost

• Alert-to-incident latency averages 1.71 s across 118 incidents; L1 and L2 median per-event costs are 33 µs and 605 µs.All five properties accumulate steadily with run length, with P3.4 growing most slowly; the reported microsecond timings are hardware-dependent.Source: §5.5 · pp. 12–13, Figure 2 · p. 13

5.6 Coverage, evasion, and threats to validity

• Coverage spans mixed-APT nodes, six P3.4 attackers, and silent-node incidents; evasion requires throttling or meeting P3.2’s three-device breadth.IoT-23 replay tests compatibility, not detection accuracy; its labels do not align with the event-level catalogue.Source: §5.6 · pp. 13–14
• The attack set is synthetic and closed, and the single-host setup compresses real multi-gateway jitter and clock skew.Thresholds are testbed-tuned rather than claimed to generalize; benign-shaped pulsing trips P2.2, making deployment-time calibration a prerequisite.Source: §5.6 · pp. 14–15

Hierarchical CPS-RV and runtime assurance

• STREL and SaSTL formalise hierarchical spatio-temporal monitoring; this paper reuses that decomposition but uses parametric MFOTL for cross-node correlation.SOTER and safe-RL shielding pair monitors with controller fallback.Source: §6 · p. 15

Comparison of RV engines for L3

• MonPoly supports cross-device first-order quantification but is event-triggered; RTLola handles silent-node deadlines, making their pairing cover both capabilities.VeriMon also covers quantification but is event-triggered; TeSSLa scales poorly with runtime-varying fleet sizes, while Copilot targets single-device instrumentation.Source: §6 · p. 15

Runtime verification in digital twins

• Temperekidis et al. integrate runtime verification with digital-twin executions at design time; this framework applies formal monitoring at deployment time over edge-device fleets.The cited digital-twin work includes traffic-sign recognition and depth-of-anesthesia control.Source: §6 · p. 15
• Prior digital-twin work shares per-tier formal design but operates on design-time traces rather than deployment-time fleet traces.This is the paper’s stated distinction from the cited digital-twin architecture.Source: §6 · p. 15

IoT security monitoring and layered architectures

• Unlike IoT monitoring reference models surveyed by Cavalli et al., the framework formally specifies each tier, instantiates attacks on a 15-actor testbed, and tags cloud incidents with contributing sub-traces.The paper links the audit record to NIST SP 800-160 Vol. 2 and DORA.Source: §6 · p. 15

IDS, resiliency frameworks, and audit alignment

• Learned IDS could populate the edge canonical-event stream without changing gateway or cloud tiers, while the framework adds measured costs to resiliency techniques catalogues.The paper notes that edge CNN deployment carries performance trade-offs.Source: §6 · p. 15

Limitations

• The 15-actor dataset is synthetic and covers a closed set of eight attack classes; real traffic mixes may require additional L1 predicates or threshold tuning.Threshold drift is not modelled, and finer timestamps could remove some near-coincident-event false positives.Source: §7 · p. 16

Partial compromise of L1

• If an attacker bypasses L1 but emits raw events, L2 sliding counts and L3 properties still apply; dropping events entirely remains a residual risk.An L2 heartbeat requiring each device to emit at least one event within 30 seconds is a planned mitigation.Source: §7 · p. 16

Artefact and reproducibility

• The artefact bundles monitor programs, specifications, an emulator, and the Docker topology; one shell command rebuilds and runs the stack and emits metrics and analysis files.It includes four MonPoly specifications and the RTLola P3.5 specification.Source: §7 · p. 16

Future directions

• Planned work includes Raspberry-Pi-class hardware deployment, live closed-loop evaluation, multi-gateway aggregation, an acknowledged event bus, and automated property synthesis from manuals [4].The event bus is intended to address the synchronization limitations described in the discussion.Source: §7 · p. 16

8 Conclusion

• The hybrid cloud pairing addresses cross-device quantification and absence-of-event detection, while the framework assigns monitoring checks across three hierarchical layers.Cross-device quantification becomes necessary when the gateway is restricted to single-device state; absence detection matters when a compromised edge monitor goes quiet.Source: §8 · p. 16
• In the controlled labelled 15-actor Docker testbed, every device-attributable incident named an attacker-labelled device, and RTLola caught silent-bypass attempts the MFOTL tier could not detect within a bounded delay.Per-tier monitoring costs stayed well below typical real-time budgets.Source: §8 · p. 16