发表机构
Clone Systems; International Hellenic University; Aristotle University of Thessaloniki; University of Thessaly（克隆系统; 国际希腊大学; 塞萨洛尼基亚里士多德大学; 色萨利大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
针对关键边缘物联网基础设施的运行时验证，提出弹性投递层RV-Fabric，通过双代理架构和五项连续性保证，使不完整数据流不能产生无条件的完全通过，故障注入实验证明其优于共享日志基线。
AI 中文摘要
保护关键基础设施日益依赖于在运行时对照正式安全规范持续验证大规模物联网设备群。然而，为此任务提出的运行时验证（RV）流水线通常是单主机原型，其监控器读取共享日志文件，对这种部署所遭遇的故障缺乏弹性：崩溃或过载会静默丢弃事件，时钟偏差破坏监控器所需的排序度量，当网络本身静默时，基于时间触发的“节点已静默”属性无法触发，且一个慢消费者会阻塞整个流水线。每种故障都是静默的：监控器持续在受损视图上发出判定。我们提出RV-Fabric，一个弹性投递层，通过两个代理（用于设备接入的MQTT和用于后端投递的持久流代理）承载层级结构，并重新建立五项连续性保证：崩溃下的持久投递、可信事件顺序、完全静默下的进展、有界过载下的消费者隔离与流量控制，每项保证均以代理持久性为条件的不变式。在传输层之上，RV-Fabric将证据完整性纳入运行时验证语义：每个判定携带由投递间隙、保留压力和活性导出的状态（可靠、降级、不完整或不可用），因此不完整的数据流不能产生无条件的完全通过。在容器化测试平台上进行受控故障注入，使用真实MonPoly引擎对照无故障基准衡量，共享日志基线漏掉七个注入事件中的六个，并将每个报告为无条件的完全通过，而RV-Fabric保留全部七个；移除投递机制会重新引入静默丢失，移除隔离仅损失及时性。两个已发布的关键基础设施数据集，水SCADA和IoT/IIoT，进行端到端重放。
英文摘要
Protecting critical infrastructure increasingly depends on continuously verifying large IoT fleets against formal security specifications at runtime. Yet the runtime-verification (RV) pipelines proposed for this task are typically single-host prototypes whose monitors read a shared log file, with no resilience to the failures such deployments incur: a crash or overload silently drops events, clock skew corrupts the ordering metric monitors require, a time-triggered "node has gone silent" property cannot fire when the network itself falls silent, and one slow consumer stalls the pipeline. Each failure is silent: the monitor keeps emitting verdicts over a corrupted view. We present RV-Fabric, a resilient delivery layer that carries the hierarchy over two brokers (MQTT for device ingest, a durable stream broker for backend delivery) and re-establishes five continuity guarantees: durable delivery under crashes, a trusted event order, progress under total silence, consumer isolation and flow control under bounded overload, each an invariant conditioned on broker durability. Above the transport, RV-Fabric makes evidence completeness part of runtime-verification semantics: every verdict carries a status (sound, degraded, incomplete or unavailable) derived from delivery gaps, retention pressure and liveness, so an incomplete stream cannot yield an unqualified all-clear. Under controlled fault injection on a containerised testbed, measured against a fault-free oracle using the real MonPoly engine, the shared-log baseline misses six of seven injected incidents, reporting each as an unqualified all-clear, whereas RV-Fabric preserves all seven; removing a delivery mechanism reintroduces silent loss, removing isolation costs only timeliness. Two published critical-infrastructure datasets, water-SCADA and IoT/IIoT, replay end-to-end.
Comments21 pages, 2 figures. Accepted at the 21st International Conference on Critical Information Infrastructures Security (CRITIS 2026)
