Reasoning Under Threat: Symbolic and Neural Techniques for Cybersecurity Verification
It addresses the need for rigorous and scalable verification methods in cybersecurity for system designers and researchers, but it is incremental as a survey paper.
This survey tackles the problem of ensuring cybersecurity through automated reasoning by providing a comprehensive overview of how formal logic and symbolic techniques are used to verify security properties, analyzing state-of-the-art tools and highlighting research gaps in scalability and integration with AI.
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.