Yu-Fu Fu

PhD Candidate — Georgia Institute of Technology · SSLab

I build vulnerability discovery and formal verification systems, with and without LLMs. My work includes CRSBench, a large-scale AI Cyber Reasoning System evaluation platform running 2,000+ CPU campaigns on GCP that found 14 real 0-days (3 acknowledged upstream); OSS-CRS, an OpenSSF sandbox project that found 7 additional 0-days using the AIxCC-winning CRS; and autofz, my first-author USENIX Security 2023 meta-fuzzer that composes existing fuzzers at runtime from per-workload feedback, beating collaborative fuzzing on 19 of 20 benchmarks and finding 152% more bugs than individual fuzzers. I also work on formal verification: CryptoLine-based verification of Curve25519 ladder-step and crypto field/group code (CCS); Coq-certified verification infrastructure for CryptoLine and SMT bit-vectors (CAV); and LLM-based specification generation for Move smart contracts (ASE 2025). I am advised by Prof. Taesoo Kim at SSLab.

Contributed security benchmark creation to Team Atlanta, DARPA AIxCC winner ($4M prize). 3× DEFCON CTF finalist (2nd, 4th, 12th).

News

Jul 2026

Wrote The Control Plane Was the Point: Revisiting autofz in the LLM Era, a retrospective on fuzzer orchestration and agentic security systems.

Publications

CRSBench benchmark construction, distributed execution, and verification pipeline

CRSBench: Realistic End-to-End Evaluation of Cyber Reasoning Systems

Yu-Fu Fu*, Youngjoon Kim*, Dongkwan Kim*, et al., Taesoo Kim (* co-first)

Under Review

Co-led the Team Atlanta benchmark/discovery platform and led its integration with OSS-CRS's standardized execution interface; distributed campaigns across 2,000+ GCP CPUs covered 124 benchmarks, 82 OSS projects, and 315 CPVs, finding 14 real 0-days.

Site Code

SoK: DARPA's AI Cyber Challenge (AIxCC): Competition Design, Architectures, and Lessons Learned

Cen Zhang, Younggi Park, Fabian Fleischer, Yu-Fu Fu, et al., Taesoo Kim

USENIX Security 2026

Led the paper's patch-generation section and co-analyzed all 7 finalist CRSs across architectures, vulnerability discovery, patching, and competition lessons.

PDF arXiv

OSS-CRS architecture and standardized execution interface

OSS-CRS: Liberating AIxCC Cyber Reasoning Systems for Real-World Open-Source Security

Andrew Chin, Dongkwan Kim, Yu-Fu Fu, et al., Taesoo Kim

WOOT 2026

Led the CRSBench–OSS-CRS integration boundary, connecting realistic evaluation and discovery campaigns to standardized, isolated AIxCC CRS execution; found 7 additional real 0-days.

Site PDF Code

MSG static analysis and agentic specification generation workflow

Agentic Specification Generator for Move Programs

Yu-Fu Fu, Meng Xu, Taesoo Kim

ASE 2025

Built the first automated specification generator for Move, a 7.3k-LoC Rust/GPT system published at ASE 2025. Independently reverse-engineered under-documented Aptos compiler internals, traced source-to-bytecode lowering, and built cross-module dependency analysis with compile-validated selective inlining. Added ClauseGen agents, ensembling, and Move Prover-checked AST mutation to generate verifiable specs for 84% of evaluated Aptos Move functions. Supported by a Sui research gift.

PDF Slides Code

autofz preparation and focus phase architecture

autofz: Automated Fuzzer Composition at Runtime

Yu-Fu Fu, Jaehyuk Lee, Taesoo Kim

USENIX Security 2023

First-author runtime meta-fuzzer for black-box fuzzer composition and resource scheduling; beat collaborative fuzzing on 19 of 20 benchmarks and found +152% bugs over individual fuzzers. Supported by a Cisco Research grant.

Retrospective: The Control Plane Was the Point: Revisiting autofz in the LLM Era.

PDF Slides Code HN

CoqCryptoLine certified verification architecture

CoqCryptoLine: A Verified Model Checker with Certified Results

Ming-Hsien Tsai, Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Bow-Yaw Wang, Bo-Yin Yang

CAV 2023

Co-developed a Coq-certified CryptoLine verifier so low-level cryptographic program proofs can be checked independently of the verifier implementation.

PDF Code

Algebraic abstraction from low-level instructions to polynomial equations

Certified Verification for Algebraic Abstraction

Ming-Hsien Tsai, Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Bow-Yaw Wang, Bo-Yin Yang

CAV 2023

Co-developed certified algebraic abstraction for bit-vector verification, reducing trusted reasoning in scalable cryptographic program proofs.

PDF

Certified SMT bit-vector solver workflow

CoqQFBV: A Scalable Certified SMT Quantifier-Free Bit-Vector Solver

Xiaomu Shi, Yu-Fu Fu, Jiaxiang Liu, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang

CAV 2021

Co-developed a scalable Coq/SSReflect-certified QF_BV solver, providing machine-checkable SMT bit-vector reasoning for low-level verification.

PDF Code

GCC plugin workflow for generating and verifying CryptoLine programs

Signed Cryptographic Program Verification with Typed CryptoLine

Yu-Fu Fu, Jiaxiang Liu, Xiaomu Shi, Ming-Hsien Tsai, Bow-Yaw Wang, Bo-Yin Yang

ACM CCS 2019

First-author work extending CryptoLine with signed arithmetic and GCC GIMPLE translation; verified Curve25519 ladder-step C in OpenSSL/BoringSSL plus field/group routines using SMT, Singular, and CryptoLine; found a NaCl bug.

PDF Slides Code

Publicly Reported / Disclosed Bugs

CVE-2026-44777

jq stack overflow in module loading on mutual include.

CVE-2026-47770

jq stack overflow in deep structural equality.

nsjail issue #247

proc_rw flag behavior.

jq issue #3533

undefined behavior in array index handling for infinite.

DuckDB issue #22325

Parquet DATA_PAGE_V2 truncated payload reaches delta decoding and triggers an uninitialized heap read.

log4cxx issue #639

DOMConfigurator stack overflow while loading crafted XML configuration.

GPAC issue #3548

Malformed dac4 config leaves the bitstream unaligned and triggers a later abort.

ZXing issue #2065

IllegalStateException in MultiFormatEncodeFuzzer.

libical issue #1311

Stack overflow in vCard parsing on deeply nested VCARD input.

wolfSSL PR #10339

Upstream fix for otherName handling in ConfirmNameConstraints.

NaCl bug report

Found and reported a NaCl bug while verifying production cryptographic code.

Software

Research

CRSBench

Team Atlanta CRS benchmark/discovery platform spanning 124 benchmarks, 82 OSS projects, and 315 CPVs

OSS-CRS

OpenSSF sandbox framework for running AIxCC CRSs on real OSS targets with isolation and standardized harnesses

MSG

Agentic Rust/GPT pipeline over Aptos Move IR with mutation-based coverage for verifier-checkable formal specifications

autofz

Black-box runtime meta-fuzzer for composing existing fuzzers and reallocating resources from per-workload feedback

coq-cryptoline

Coq-certified CryptoLine verifier for independently checkable cryptographic program proofs

coq-qfbv

Coq/SSReflect-certified QF_BV solver for machine-checkable bit-vector reasoning

gcc2cryptoline

GCC GIMPLE-to-CryptoLine translator used with SMT and Singular to verify optimized cryptographic C implementations

Tools

I develop open-source tools under Axiweave, my umbrella organization for intelligent developer tooling.

claude-code-ide.el

Project-aware Emacs IDE integration for Claude Code, Codex, OpenCode, Pi, and Oh My Pi

codex-as

Run Codex under saved auth/provider profiles without touching config files

keepass-cli-rs

KeePass CLI in Rust with Emacs integration

maskedemail-rs

Fastmail MaskedEmail CLI in Rust with Emacs integration

Fastmail-Sieve-Sync

Sync Fastmail Sieve filter rules from a local file