SyzSpec

Specification Generation for Linux Kernel Fuzzing via Under-Constrained Symbolic Execution

Overview

SyzSpec addresses the critical bottleneck of manually writing syscall descriptions for Linux kernel fuzzing. It uses under-constrained symbolic execution to automatically generate precise specification templates, significantly reducing the human effort required to fuzz kernel drivers. SyzSpec has discovered over thousands of specification entries covering hundreds of drivers, leading to the discovery of numerous unique kernel bugs.

Key Features

• Under-constrained symbolic execution for specification inference

• Automatic identification of device opening sequences and ioctl dependencies

• Cross-driver dependency tracking for real-world device interactions

• Seamless integration with Syzkaller for downstream fuzzing

Technologies

• Symbolic Execution

• LLVM / Bitcode Analysis

• Syzkaller Integration

🏆 CCS 2025 Distinguished Paper Award