Nov 2026· Information and Software Technology· Vol 199, pp. 108285· 0 citations· 14 references
TL;DR
Pretty Verifier significantly improves the developer’s experience and facilitates the resolution of critical security issues by improving the readability of eBPF verifier messages and strengthening their connection to the original C source code.
Abstract
Context: eBPF is an emerging technology in cloud computing, allowing user-defined programs to run in kernel space for observability, networking, and security. To ensure system integrity, the kernel relies on the eBPF verifier, a static analyzer that rejects potentially unsafe code. However, the verifier’s error messages are notoriously difficult to understand, generally referencing low-level bytecode rather than the original C source and making debugging a difficult and time-consuming task. Objective: The goal of this work is to improve the eBPF verifier error messages and make debugging easier by mapping verification errors back to the original C source code and by providing more understandable feedback to developers. Methods: This paper presents Pretty Verifier, a tool designed to improve the eBPF verifier error messages. By analyzing the verifier log and the compiler debug information, the tool maps verification errors back to the specific lines of C code, providing human-readable explanations and actionable fix suggestions. To rigorously validate the tool despite the scarcity of faulty eBPF datasets, we developed a fuzzing framework based on the BRF semantic fuzzer, capable of generating a balanced dataset of broken programs. Results: Experimental results on over 400 test cases demonstrate that the tool successfully localizes errors in 84% of cases and provides precise, context-aware explanations. Conclusion: Pretty Verifier significantly improves the developer’s experience and facilitates the resolution of critical security issues by improving the readability of eBPF verifier messages and strengthening their connection to the original C source code.
An approach to verifying the results of static code analysis using large language models (LLMs), which filters warnings to eliminate false positives, which was implemented in SharpChecker, an industrial static analyzer for C#.
D. D. Panov, N. V. Shimchik, D. A. Chibisov et al.· Programming and computer sof...· 0 citations
eBPF allows user-defined programs to safely extend Linux kernel functionality at runtime, but its final machine code comes from a compilation pipeline that differs from native targets, and how efficient that pipeline is has no clear reference point. Our work constructs one: using the standard LLVM x86 backend as an app...
Hoang Duong, Hao Sun, Zhen-Dong Su· Proceedings of the 4th Works...· 0 citations
This paper investigates automated fault localization for verification-aware languages by comparing two paradigms: state-based and counterexample-based localization, and shows that counterexample-based approaches substantially outperform state-based localization in this setting.
Álvaro F. Silva, Isabel Amaral, João Pascoal Faria et al.· 1 citation· ⚡1
FlowCheck, a constraint language to specify user-visible information flows directly through the application interface, where constraints can also be displayed and inspected without reading code, and are structured enough for reliable LLM generation.
Reya Vir, Lydia B. Chilton, Zhuo Zhang et al.· 1 citation
Statically typed languages offer many advantages in software engineering, including bug prevention, enhanced code quality, and reduced maintenance costs. However, these benefits come at the expense of a steep learning curve and a slower development pace. Although known for its expressive and strong type system, Haskell...
Shuai Fu, Tim Dwyer, Peter James Stuckey et al.· International Conference on...· 0 citations
A debugging workflow that combines dynamic analysis with directed unit tests is introduced, and ACF, an infrastructure for automating this workflow is presented, indicating that ACF can help developers to isolate specific inputs causing an error, thus simplifying the process of locating faulty statements.
Roman Vašut, P. Parízek· Proceedings of the 14th Work...· 0 citations
We use cookies to run the site and, with your consent, for analytics and to show ads.
See our Cookie Policy.