Sep 2026· Proceedings of the 4th Workshop on eBPF and Kernel Extensions· 0 citations· 31 references
TL;DR
A userspace version of the kernel verifier is developed and appended to the BPF backend to increase the class of programs accepted by the Linux eBPF verifier without increasing its complexity.
Abstract
This paper proposes proof-carrying-BPF programs as a mechanism to increase the class of programs accepted by the Linux eBPF verifier without increasing its complexity. To accomplish this vision, we develop a userspace version of the kernel verifier and append it to the BPF backend. The BPF backend generates proofs with symbolic evaluation where the kernel verifier is not able to prove safety. The kernel verifier checks proofs with an in-kernel proof checker and accepts the program when the proof is valid. This coupling of the userspace BPF verifier to the BPF backend addresses the limitations of the recent BCF framework, such as latency due to multiple kernel-to-userspace transitions and the dormant verifier state during userspace verification. Our prototype successfully verifies all 360 objects of the BCF suite — drawn from the Calico and Cilium datapaths, BCC, and Inspektor Gadget — that the kernel verifier previously rejected.
Large language models (LLMs) have shown strong potential for assisting software and security analysis tasks, yet their effectiveness in cryptographic symbolic protocol verification remains insufficiently understood. In this paper, we conduct the first systematic evaluation of the capability of state-of-the-art LLMs in...
Tian-Jian Liu, Shi-Cheng Feng, Jin'ao Shang et al.· 0 citations
This pearl shows how a clean separation can be achieved within the two-layer method by combining two simple ideas: expressing implementation correctness as a relational Hoare quadruple, and introducing assertion annotations into the abstract program to capture key invariants.
Shu-Shu Wu, Cheng-Xi Yang, Xi-Wei Wu et al.· Proc. ACM Program. Lang.· 0 citations
Specifying contracts as program behavior using Hoare triples is an established practice in software engineering. Compared to traditional testing approaches, formal verification of these contracts provides stronger guarantees of functional correctness. However, its practical adoption has remained limited since significa...
Aryan Kumar, Alex Toppo, Sandip Ghosal· Proceedings of the 2nd Works...· 0 citations
A proof checker called Nörgler is introduced that builds upon and extends the established approach pioneered by GDV and supports checking propositional, (untyped and typed) first-order, and higher-order refutations represented in TSTP.
Melanie Taprogge, H. Sariyanto, Alexander Steen· 1 citation
This work develops a new methodology for verifying cryptographic software and extends SymCrypt with experimental optimizations and implementations of algorithms such as FrodoKEM, ML-DSA, and HPKE to explore the scalability of writing, adapting, and verifying cryptographic code.
Ho Son, C. Fournet, Jonathan Protzenko et al.· 0 citations
SymCert is presented, a framework implemented in Lean for building verified SMT-based analyses of Cedar policies that provide a verified symbolic compiler and authorizer for reducing policies to SMT formulas, a hierarchy enforcer for ensuring well-formedness of counterexamples, and a counterex-ample extractor for provi...
Emina Torlak· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.
