TLA2eBPF: Real-Time Protection for Kernel Memory Out-of-Bounds Security

Memory out-of-bounds (OOB) vulnerabilities in the Linux kernel threaten system integrity by enabling privilege escalation, information leakage, and arbitrary code execution. Formal verification techniques such as TLA+ can mathematically guarantee memory-safety invariants but cannot enforce runtime monitoring, whereas eBPF provides real-time kernel instrumentation but relies on manually crafted heuristic rules. This work presents TLA2eBPF, the first semantics-preserving framework that automatically converts TLA+ security specifications into executable eBPF monitoring code. We design (1) bidirectional semantic-mapping rules between TLA+ state machines and eBPF runtime states; (2) a TLAPS-based bisimulation proof system ensuring behavioral equivalence; and (3) an optimized eBPF runtime including cache acceleration, batched event delivery, and probabilistic sampling. Experiments on real CVEs and Syzkaller cases demonstrate 100% detection coverage, 0% false positives, and <3.5% runtime overhead, achieving both formal completeness and practical real-time protection.