发表机构
Bitdefender; Alexandru Ioan Cuza University（比特防御; 亚历山德鲁·约安·库扎大学）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
该研究针对分布式恶意软件检测系统的服务器故障处理问题，基于Bitdefender生产架构构建Promela形式化模型，用SPIN验证其优雅降级回退链的6项LTL属性，证明系统无误报、无死锁等，为生产安全系统故障处理逻辑提供形式化正确性保证。
AI 中文摘要
现代终端恶意软件检测是分布式的：每个终端上的轻量级代理从被扫描的文件或进程中收集特征，将其发送到远程服务器进行分析，随后通过拦截、隔离或清除在本地执行返回的判定结果。由于终端会依据判定结果采取行动，检测相关的分布式机制绝不能将暂时性的服务器故障转化为错误操作。我们提出了一个用Promela语言编写的此类系统终端决策流水线形式化模型，该模型提取自Bitdefender的生产架构。该模型刻画了系统的优雅降级回退链：当主分析服务器超时，终端会回退到较旧的传统协议服务器，若仍失败则回退到精简特征库的本地扫描，之后再执行判定结果。假设检测特征库是可靠的，我们用线性时序逻辑（LTL）定义了6项安全性和活性属性，并使用SPIN模型检测器对其进行了穷尽验证。我们证明了回退机制绝不会产生误报（对良性文件采取执行措施），即使超时响应延迟到达，每次扫描也只会得出一个判定结果，检测强度仅以明确且有序的方式减弱，且始终能终止于一个执行决策，因此该流水线无死锁。经检验，每项属性都非空成立，我们还报告了状态空间如何随并发扫描和终端数量增长。这项工作展示了模型检测如何为生产级安全系统的故障处理逻辑提供强正确性保证，而这一层面此前很少受到直接的形式化关注。
英文摘要
Modern endpoint malware detection is distributed: a lightweight agent on each endpoint collects features from a scanned file or process, sends them to a remote server for analysis, and then enforces the returned verdict locally by blocking, quarantining, or disinfecting. Because the endpoint acts on the verdict, the distributed machinery surrounding detection must never turn a transient server failure into a wrong action. We present a formal model, in Promela, of the endpoint decision pipeline of such a system, abstracted from a production architecture at Bitdefender. The model captures the system's graceful-degradation fallback chain: when the primary analysis server times out, the endpoint falls back to an older legacy-protocol server, and failing that to a reduced-signature local scan, before enforcing a verdict. Assuming detection signatures are sound, we specify six safety and liveness properties in linear temporal logic (LTL) and verify them exhaustively with the SPIN model checker. We prove that the fallback machinery never causes a false positive (an enforcement action against a benign file), commits to exactly one verdict per scan even when timed-out responses arrive late, weakens detection strength only in an explicit and ordered way, and always terminates in an enforcement decision, so the pipeline is deadlock-free. Each property is checked to hold non-vacuously, and we report how the state space grows with concurrent scans and endpoints. The work shows how model checking can give strong correctness guarantees for the failure-handling logic of a production security system, a layer that has received little direct formal attention.
CommentsIn Proceedings FROM 2026, arXiv:2609.30324
Journal refEPTCS 452, 2026, pp. 158-171
