Laser method improves detecting complex protocol dependencies accurately
LASER: Defeasible Certificate Search for Long-Range Protocol Dependencies
Software EngineeringArtificial Intelligence
Summary
Protocols that control how computers talk often spread their rules across many places, making it hard to understand what exactly should happen. The authors present LASER, a method that gathers pieces of evidence from far apart parts of a protocol and decides if a behavior is allowed, blocked, or unclear. Unlike other approaches that just look nearby or read the whole document blindly, LASER carefully tracks missing or conflicting information and flags uncertainty explicitly. Tests show LASER finds more correct protocol behaviors and avoids false positives better than previous tools.
What this means in practice
- •For network protocol developers: Improve validation tools to detect correct or uncertain behaviors by assembling and checking sparse protocol evidence across distant document parts.
- •For security analysts: Use LASER to reduce false alarms in protocol compliance audits by explicitly managing incomplete or corrected evidence in protocol rules.
Authors
Zihan Tang, Huibiao Zhu
Abstract
Protocol specifications rarely justify executable behavior in one place: a transition may inherit its source state from a remote control block, name its events only by number, and remain subject to a later correction. Recovering the nearby clause is therefore insufficient; the system must assemble a source-linked certificate and determine whether any stronger rule applies. We introduce LASER, a proof-carrying search method for sparse, defeasible protocol evidence. LASER represents missing support and unresolved corrections as explicit obligations, searches typed evidence routes, and lets an occurrence-aware symbolic checker alone decide whether a certificate warrants, refutes, or leaves a behavior unresolved. On 91 BehaviorCheck families under a matched 2K budget, LASER improves Joint Edge+Proof over the strongest local reader on two model families ($Δ=+.132$, $p=.017$; $Δ=+.198$, $p<.001$) while cutting false discoveries by 2--3$\times$. Controlled replays attribute the gain and its limits: neither reference routing nor deterministic citation expansion alone exceeds the local baseline; whole-document reading (29--65K tokens), two-round iterative retrieval, and even oracle minimal-certificate evidence all fail to reach LASER, localizing the bottleneck in typed obligation closure rather than evidence access. An authority-corruption replay shows source-link errors only cause abstention, while the only unsafe-warrant mechanism is mis-recording a Held erratum as Verified, confined to that erratum's family. LASER thus improves long-range dependency recovery while converting incomplete evidence and uncertain authority into explicit residual obligations rather than unsupported behavior.