OSVBench: Benchmarking LLMs on Specification Generation Tasks for Operating System Verification

TL;DR

OSVBench introduces a long-context, OS-kernel-focused benchmark for generating formal specifications needed for verification, using Hyperkernel as the verification engine. It reframes specification generation as a deterministic program-synthesis task with explicit verification assumptions, fixed declarative specs, and a restricted search space, then evaluates 12 LLMs across 245 syscall tasks with injected bugs. The findings reveal limited and highly variable performance across models, with larger or non-reasoning models not uniformly dominating, and demonstrate that demonstrations (few-shot) and self-repair can improve outcomes but whose gains vary by model. The work highlights substantial gaps in current LLM capabilities for complex, domain-specific verification and provides a dataset and methodology to drive future improvements in long-context, formal-spec generation for OS kernels.

Abstract

We introduce OSVBench, a new benchmark for evaluating Large Language Models (LLMs) on the task of generating complete formal specifications for verifying the functional correctness of operating system kernels. This benchmark is built upon a real-world operating system kernel, Hyperkernel, and consists of 245 complex specification generation tasks in total, each of which is a long-context task of about 20k-30k tokens. The benchmark formulates the specification generation task as a program synthesis problem confined to a domain for specifying states and transitions. This formulation is provided to LLMs through a programming model. The LLMs must be able to understand the programming model and verification assumptions before delineating the correct search space for syntax and semantics and generating formal specifications. Guided by the operating system's high-level functional description, the LLMs are asked to generate a specification that fully describes all correct states and transitions for a potentially buggy code implementation of the operating system. Experimental results with 12 state-of-the-art LLMs indicate limited performance of existing LLMs on the specification generation task for operating system verification. Significant disparities in their performance highlight differences in their ability to handle long-context code generation tasks. The code are available at https://github.com/lishangyu-hkust/OSVBench

Figures (18)

• Figure 1: The workflow of the OSVBench benchmark suite. The workflow consists of the generation stage and the specification quality evaluation stage. During the generation stage, the input to LLMs includes a system prompt, verification assumptions, a programming model, system call (syscall) examples, and a task question (see Sec. \ref{['sec:benchmark-task-construction']} for details). Based on this input, the LLMs are tasked with generating the correct state-machine specification for a given syscall. The evaluation stage checks the correctness of the generated state-machine specification by comparing the verification results it produces against those produced by a ground-truth oracle state-machine specification when both are fed into a kernel verifier. In particular, the kernel verifier takes as input a state-machine specification and a formal declarative specification of the kernel (see Sec. \ref{['sec:hyperkernel-preliminaries']}), then uses them to perform verification (see Sec. \ref{['sec:problem-formulation']}) on a potentially buggy kernel implementation (see Sec. \ref{['sec:benchmark-task-construction']}). If both state-machine specifications produce the same verification results for all kernel implementations, the generated one is considered correct. If the two results differ for any kernel implementation, the generated state-machine specification is considered incorrect.
• Figure 2: Abstract syntax for state-machine specifications. A specification is a kernel state. A kernel state may be an input parameter of the system call, a conditional state that branches to one of two existing states according to a condition, or a modified state that assigns new expressions to the attributes of an existing state. An expression may be an existing value, an arithmetic expression, or a conditional expression. A value may be an input parameter, a predefined constant literal, or an attribute of an existing state. A condition may be a logical expression, a conjunction, or a disjunction. Intuitively, a specification defines how to transition the OS kernel to a subsequent state. The specification defines state transition and field assignments, along with the conditions that must be satisfied.
• Figure 3: Performance comparison of Pass@1, Pass@3, and Pass@5 of various models. The average performance of the models exhibits consistent improvement as k increases in Pass@k.
• Figure 4: Performance of various models with different numbers of few-shot examples.
• Figure 5: Performance comparison (Pass@1 %) of 12 LLMs on specification generation tasks using syscall implementations injected with varying numbers of bugs.