Beyond Runtime Enforcement: Shield Synthesis as Defensibility Analysis for Adversarial Networks
English summary
The paper reframes shield synthesis in reinforcement learning from a runtime safety mechanism into a design-time analytical tool for assessing network defensibility. It instantiates this via a constrained two-player safety game for network defense, which yields a binary defensibility verdict, the winning region, a shield, and topology-level metrics derived from attractor computation. These formal measures are combined with post-convergence behavior from adversarial multi-agent reinforcement learning to form a defensibility fingerprint. A what-if analysis demonstrates that formal defensibility and operational effectiveness capture distinct aspects of security, with small architectural changes causing large shifts in operational outcomes while leaving formal safety margins nearly unchanged. The work concludes that shield synthesis is most valuable as a framework for answering architectural questions about whether, where, and how a system can be defended.
Chinese summary
该论文将强化学习中的盾牌合成从运行时安全机制重新阐述为一种用于评估网络防御性的设计时分析工具。它通过一个受约束的双玩家安全博弈来实例化网络防御，产出防御性判定（拓扑-规约对是否可防御）、获胜区域、盾牌以及从吸引子计算中导出的拓扑级指标。这些形式化度量与对抗多智能体强化学习收敛后的行为相结合，形成防御性指纹。假设分析表明，形式防御性和运行有效性捕捉了安全的不同方面：微小的体系结构变化会导致运行结果的巨大变化，而形式安全余量几乎不变。研究认为，盾牌合成的最大价值在于回答关于系统是否、何处以及如何能防御的体系结构问题，而非仅仅产出安全策略。
Key points
Repurposes shield synthesis from runtime enforcement to a design-time defensibility analysis for adversarial networks.
将盾牌合成从运行时执行的定位重新定义为针对对抗网络的设计时防御性分析。
Formalizes a constrained two-player safety game that outputs a defensibility verdict, winning region, shield, and topology-level metrics from attractor computation.
形式化了一个受约束的双玩家安全博弈，输出防御性判定、获胜区域、盾牌以及通过吸引子计算得到的拓扑级指标。
Combines formal safety metrics with post-convergence adversarial MARL behavior to create a defensibility fingerprint.
将形式安全指标与对抗多智能体强化学习收敛后的行为结合，构成防御性指纹。
What-if analysis reveals formal defensibility and operational effectiveness are distinct; architectural tweaks can dramatically alter operational outcomes with minimal impact on formal margins.
假设分析揭示形式防御性与运行有效性是分离的；体系结构微调可大幅改变运行结果，却对形式安全余量影响甚微。