PACE: Policy Adaptation for Cybersecurity Events Through Formal Verification of LLM-Generated Firewall Policies

The increasing integration of Artificial Intelligence (AI) into cybersecurity reduces manual efforts and improves adaptability, but the probabilistic nature of AI renders its output unreliable, especially when used in network firewall policies. This uncertainty prevents direct, real-time enforcement, leading to critical windows of latency due to necessary human oversight. This paper presents PACE, a formal framework designed to constrain and adapt LLM-generated firewall policies for safe enforcement via the extended Berkeley Packet Filter (eBPF). PACE integrates an LLM-based policy generator with a formal verifier that rigorously checks each candidate rule against a semantic bounding constraint (Φ) and a set of mathematically defined safety invariants (I). The policies that fail verification are used to provide iterative feedback to refine future LLM prompts, automatically improving policy generation over time. We formally model this verification, so that safety properties are preserved even under dynamic rule composition and updates, providing strong theoretical guarantees. A prototype implementation of the verifier demonstrates the feasibility and efficiency of the proposed approach. It achieves high verification success rates and near-linear scalability. By establishing a proof-backed interface between probabilistic AI predictions and deterministic system security, PACE aims to reduce the time-to-mitigation (TTM) while ensuring provable enforcement correctness.