Yu-Fu Fu

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).

Publications

2026
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: 124 benchmarks, 82 OSS projects, 315 CPVs, and 2,000+ CPU campaigns that found 14 real 0-days.
2026
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
Co-analyzed all 7 AIxCC finalist CRSs, comparing architectures, vulnerability discovery strategies, patch generation, and competition lessons.
2026
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
Helped port AIxCC finalist CRSs into an OpenSSF sandbox framework with standardized targets and isolation; found 7 additional real 0-days.
2025
Agentic Specification Generator for Move Programs
Yu-Fu Fu, Meng Xu, Taesoo Kim
ASE 2025
First-author system for agentic Move specification generation; built the Rust/GPT pipeline over Aptos compiler and bytecode IR that produced verifiable specs for 84% of Aptos framework functions. Supported by a Sui research gift.
2023
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.
2023
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.
2023
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.
2021
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.
2019
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.

Publicly Reported / Disclosed Bugs

jq stack overflow in module loading on mutual include.
jq stack overflow in deep structural equality.
proc_rw flag behavior.
undefined behavior in array index handling for infinite.
Parquet DATA_PAGE_V2 truncated payload reaches delta decoding and triggers an uninitialized heap read.
DOMConfigurator stack overflow while loading crafted XML configuration.
Malformed dac4 config leaves the bitstream unaligned and triggers a later abort.
IllegalStateException in MultiFormatEncodeFuzzer.
Stack overflow in vCard parsing on deeply nested VCARD input.
Upstream fix for otherName handling in ConfirmNameConstraints.
NaCl bug report
Found and reported a NaCl bug while verifying production cryptographic code.

Software

Research

Team Atlanta CRS benchmark/discovery platform spanning 124 benchmarks, 82 OSS projects, and 315 CPVs
OpenSSF sandbox framework for running AIxCC CRSs on real OSS targets with isolation and standardized harnesses
Agentic Rust/GPT pipeline over Aptos Move IR for generating verifier-checkable formal specifications
Black-box runtime meta-fuzzer for composing existing fuzzers and reallocating resources from per-workload feedback
Coq-certified CryptoLine verifier for independently checkable cryptographic program proofs
Coq/SSReflect-certified QF_BV solver for machine-checkable bit-vector reasoning
GCC GIMPLE-to-CryptoLine translator used with SMT and Singular to verify optimized cryptographic C implementations

Tools

Run Codex under saved auth/provider profiles without touching config files
KeePass CLI in Rust with Emacs integration
Fastmail MaskedEmail CLI in Rust with Emacs integration
Sync Fastmail Sieve filter rules from a local file