FORMAL VERIFICATION OF INTRUSION DETECTION SYSTEMS: A COMPUTATIONAL THEORY APPROACH

Abstract

This paper presents a computational theory-based formal verification of intrusion detection systems (IDS), employing a framework grounded in finite automata and temporal logic. The proposed methodology comprises four principal phases: system modelling, specification formalisation, verification procedure, and validation, enabling rigorous verification of signature-based, anomaly-based, and hybrid IDS architectures. Verification results show clear distinctions among architectures. The signature-based IDS exhibited strong soundness and timeliness, but failed completeness verification, unable to detect novel attacks outside its signature database. By contrast, the anomaly-based IDS achieved partial completeness catching some previously unknown attacks but failed to maintain soundness, breaching acceptable false positive thresholds. The hybrid IDS performed best, fully verifying five of seven key properties, though perfect completeness remained unattainable, highlighting inherent detection limitations. Counterexample analysis identified signature evasion (e.g., polymorphic attacks) as the root of 42.6% of detection failures attacks subtly altering known signatures. Meanwhile, anomaly-based systems suffered primarily from false positives due to benign but unusual traffic patterns (60.5% of failures). The signature-based IDS had the least state complexity and fastest verification due to its deterministic logic, while the hybrid and anomaly-based systems required far more computational resources owing to probabilistic modelling of traffic behaviour. Refinement iterations enhanced hybrid IDS performance, ultimately achieving satisfaction of all seven formal properties by combining weighted voting, temporal correlation analysis, and adaptive thresholds. Still, the signature-based model plateaued, and the anomaly-based approach could not simultaneously satisfy completeness and soundness due to conflicting error rates. Scalability analysis demonstrated that verification time increased polynomially with detection rules, becoming challenging for large-scale implementations. Overall, the formal verification framework uncovered 17 previously unknown vulnerabilities across the three IDSs all confirmed by manual inspection and subsequently patched. This demonstrates the practical value of formal verification in surfacing subtle, critical flaws, thus improving IDS robustness and reliability against evolving cyber threats.