VeriLucid: A Verification-aware Data-plane Programming Language

Compilomorphic Fuzzing: Turning a Compiler Against Itself

Compilomorphic fuzzing is introduced, a new validation approach that turns a compiler into its own test oracle via structure-preserving transformations over programs and structured inputs, establishing a practical, model-free foundation for validating compilers in critical DSL domains.

Formally-Verified, Tight Timing Constraints for Machine Code

Chameleon: Toward Runtime-Pluggable Verification of Programmable Networks

Runtime verification is critical for detecting whether programmable networks behave as intended during operation. However, many existing runtime verification mechanisms instantiate executable verification logic around requirements specified before deployment, making it difficult to change checks at runtime. This paper presents Chameleon, a runtime-pluggable verification mechanism for programmable networks. Chameleon separates a stable verification substrate from concrete verification requirements: the verification substrate is embedded into the data plane before deployment, while requirements are represented as runtime-manageable VERIFY objects and translated into P4Runtime table entries, allowing the operator to add, modify, or delete supported verification types without recompiling the data-plane program. Experimental results show that Chameleon can augment P4 programs with small one-time preprocessing and compilation overheads, and supports millisecond-level runtime configuration operations for verification requirements.

T-LLM Compiler: Trusted LLM-based Code Optimization and Verification Framework

Recent advances in Large Language Models (LLMs) have opened opportunities to apply high-level code transformations to the field of code optimization, and it has since emerged as one of the most fundamental tasks for LLMs to perform; however, at present, LLMs struggle to apply wide-ranging code optimization tasks due to both the complexity of the code and the inability to independently verify the correctness of the transformations. In this paper, we present the Trusted LLM (T-LLM) Compiler, which proposes an advancement in compiler technology through a collaborative effort involving high-level LLM code transformations, traditional compilers, and verification tools. Experimental results reveal that it can significantly improve code correctness when tested on a set of PolyBench/C benchmarks. Our approach facilitates iterative code optimization efforts with verification strategies that enable corrective actions. Through this approach, T-LLM Compiler achieves code optimization accuracy of up to 83.3% and a speedup of up to 16.1\% on the PolyBench/C benchmarks, with the transformed code reaching an average of 26.7% speedup wrt standard baselines. Additionally, we release the project's source code to the open-source community.

Improving error messages for eBPF programs

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.

Trace-Based Execution-Level Observability of VDM-SL Specifications

The recording and utilization of execution traces of assignments, operation calls, and return statements are proposed to make the internal behavior of operations persistent and analyzable as state-based models.