Safe by construction
Proof-guided in-kernel verifiers that accept an extension only when it is accompanied by evidence the kernel itself can check: precise where today's verifiers are conservative, and sound where they are not.
Hao Sun
Ph.D. Candidate in Computer Science
Advanced Software Technologies Lab
Department of Computer Science,
ETH Zurich
CNB H 103.2, Universitätstrasse 6, 8092 Zürich, Switzerland
hao.sun@inf.ethz.ch
About
I am a Ph.D. candidate in the Advanced Software Technologies Lab at ETH Zurich, where I am advised by Prof. Zhendong Su. Before coming to ETH, I received an M.Sc. from Tsinghua University, where I was advised by Prof. Yu Jiang. In the summer of 2026 I was a research intern at Microsoft Research in Redmond, Washington.
My research is on making OS kernel components safe and correct by construction. Systems code demands the strongest guarantees of safety and correctness, and coding agents now produce it at ever greater scale; only reasoning that is equally automated, and no less rigorous, can keep pace in establishing those guarantees. I like problems that matter in practice, and I carry the solutions into real, working systems.
News
- 2026From Specification to Kernel Commit accepted at ASPLOS '27.
- 2026Research intern at Microsoft Research, Redmond, verifying kernel components in Rust/Verus.
- 2026Invited talk at the ETH Zurich Systems Group Seminar.
- 2025Prove It to the Kernel received the Best Paper Award at SOSP '25. 🏆
- 2024Invited talk at the Linux Plumbers Conference, eBPF track.
- 2024Awarded an eBPF Foundation Research Grant ($50,000) as co-PI.
I am on the academic job market in the 2026–2027 cycle, looking for faculty positions. Happy to talk, so please get in touch.
Research
An operating system kernel is the last place where a defect is acceptable, and the first place where one is hard to find. My work attacks this from three sides: admit only extensions that come with machine-checkable evidence, generate kernel code together with machine-checked proofs, and expose the defects that already exist at system scale.
Correct by construction
Verified code generation: coding agents and formal verification working together, so that real systems code arrives with a machine-checked proof of functional correctness against its specification.
Defect detection at scale
Relation-guided fuzzing, automatically generated interface specifications, and effective oracles that surface deep correctness and security defects in kernels that resist conventional testing.
Publications
Reverse chronological. See also my Google Scholar profile.
First-authored
-
From Specification to Kernel Commit: Verified Code Generation on Real-World Systems
-
Fast and Precise In-Kernel Extension Analysis via Proof-Guided Abstraction Refinement
-
Prove It to the Kernel: Precise Extension Analysis via Proof-Guided Abstraction Refinement
-
Approximation Enforced Execution of Untrusted Linux Kernel Extensions
-
Finding Correctness Bugs in eBPF Verifier with Structured and Sanitized Program
-
KSG: Augmenting Kernel Fuzzing with System Call Specification Generation
Co-authored
-
Kops: Safely Extending the eBPF Compilation Pipeline with Native Operations
-
Efficient Input Minimization for Kernel Fuzzing via Relation- and Type-Guided Optimization
-
Quantifying the Code-Size Overhead of eBPF JIT Compilation
-
Finding Metadata Inconsistencies in Distributed File Systems via Cross-Node Operation Modeling
-
SnapCC: Effective File System Consistency Testing Using Systematic State Exploration
-
Horus: Accelerating Kernel Fuzzing Through Efficient Host-VM Memory Access Procedures
-
Tardis: Coverage-Guided Embedded Operating System Fuzzing
Manuscripts
-
Stratified Testing: Divide the Input Space, Conquer Rare Paths
-
Synsema: Syntax-Guided Learning of Semantically Valid Programs
Software
-
BCF
An in-kernel proof checker (~5K lines of C) that admits an extension only when it carries evidence the kernel can check itself, 10× to 65× faster than checking the same proofs in user space.
-
Vero
A benchmark of 103 verified-code-generation tasks drawn from eBPF, LLVM, and seL4. Every task is a specification that production code has yet to meet, with a machine-checked proof obligation attached.
-
Healer
A relation-learning guided kernel fuzzer written in Rust. It has found 50+ kernel bugs and 10+ CVEs, and is used as a baseline by later fuzzing work.
Talks
- 2026Advancing In-Kernel Extension Verification: Towards a Highly Extensible and Reliable OS KernelInvited talk, ETH Zurich Systems Group Seminar
- 2025Prove It to the Kernel: Precise Extension Analysis via Proof-Guided Abstraction RefinementSOSP 2025, Seoul, Korea
- 2025Approximation Enforced Execution of Untrusted Linux Kernel ExtensionsUSENIX Security 2025, Seattle, WA
- 2024Lazy Abstraction Refinement with Proof for an Enhanced VerifierInvited talk, Linux Plumbers Conference (LPC '24), eBPF track
- 2024Validating the eBPF Verifier via State EmbeddingOSDI 2024, Santa Clara, CA
- 2022KSG: Augmenting Kernel Fuzzing with System Call Specification GenerationUSENIX ATC 2022, Carlsbad, CA
- 2021HEALER: Relation Learning Guided Kernel FuzzingSOSP 2021
Awards
- 2025Best Paper Award, SOSP 2025
- 2024eBPF Foundation Research Grant ($50,000), co-PI
- 2023Outstanding Master's Graduate, Tsinghua University
- 2022National Scholarship, Tsinghua University
Service
- 2026Program committee, 4th Workshop on eBPF and Kernel Extensions (SOSP '26)
- 2026Reviewer, ACM Transactions on Software Engineering and Methodology
- 2026Reviewer, IEEE/ACM Transactions on Networking
- 2026Reviewer, Computers & Security