Reasoning Under Threat: Symbolic and Neural Techniques for Cybersecurity Verification

TL;DR

The paper tackles the challenge of achieving rigorous, scalable cybersecurity verification across protocols, software, networks, and adversarial settings. It surveys how logical formalisms (temporal, deontic, epistemic, higher-order) and automated reasoning tools (theorem proving, model checking, SMT solving) model, verify, and certify security properties. It covers vulnerability detection, threat analysis, and the integration of AI with formal methods to enable neural-symbolic verification and explainable reasoning. By identifying gaps in expressiveness, compositionality, and tooling, it proposes a roadmap toward unified, modular verification pipelines, AI-assisted reasoning, and end-to-end formal ecosystems for trustworthy cybersecurity.

Abstract

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.