用形式化方法验证网络安全，结合逻辑与AI提升系统可信度。
Reasoning Under Threat: Symbolic and Neural Techniques for Cybersecurity Verification
- 用时序、道义等逻辑语言建模安全规则
- 整合符号与神经网络实现更高效推理
- 适合安全系统开发者和形式化验证研究者
网络安全需要严谨且可扩展的技术来保障系统正确性、鲁棒性和对持续演进威胁的韧性。自动化推理，包括形式逻辑、定理证明、模型检测和符号分析，为访问控制、协议设计、漏洞检测及对抗建模等领域的安全属性验证提供了基础框架。本文综述了自动化推理在网络安全中的作用，分析了时序、道义和认知逻辑等逻辑系统如何用于形式化和验证安全保证。我们考察了当前最先进工具与框架，探索了与人工智能结合的神经符号推理集成，并指出了在可扩展性、组合性及多层安全建模方面的关键研究空白。文章最后提出一系列基于实证的未来研究方向，旨在通过形式化、自动化和可解释的推理技术推动安全系统的构建。
原文摘要 · Abstract (English)
Cybersecurity demands rigorous and scalable techniques to ensure system correctness, robustness, and resilience against evolving threats. Automated reasoning, encompassing formal logic, theorem proving, model checking, and symbolic analysis, provides a foundational framework for verifying security properties across diverse domains such as access control, protocol design, vulnerability detection, and adversarial modeling. This survey presents a comprehensive overview of the role of automated reasoning in cybersecurity, analyzing how logical systems, including temporal, deontic, and epistemic logics are employed to formalize and verify security guarantees. We examine SOTA tools and frameworks, explore integrations with AI for neural-symbolic reasoning, and highlight critical research gaps, particularly in scalability, compositionality, and multi-layered security modeling. The paper concludes with a set of well-grounded future research directions, aiming to foster the development of secure systems through formal, automated, and explainable reasoning techniques.
Thank you to arXiv for use of its open access interoperability. PaperDance 不是 arXiv 官方产品；中文卡片由大模型生成，请以原文为准。