Md (Muhammad) Shafiuzzaman Ph.D. Candidate · Computer Science · UCSB
Google Scholar GitHub LinkedIn
Email

Bio. I am currently a Ph.D. candidate in Computer Science at the University of California, Santa Barbara (UCSB), advised by Prof. Tevfik Bultan. I work as a Graduate Student Researcher in the Verification Lab (VLab), supported by DARPA’s HARDEN and INGOTS programs. Before starting my Ph.D., I worked as a software engineer building large-scale software systems in industry.

Research. My research lies at the intersection of AI-assisted software engineering, software security, program analysis, and formal methods. I develop hybrid static–symbolic techniques and LLM-assisted workflows that make it practical to detect, confirm, and characterize vulnerabilities including exploit chains in large, real-world systems.

My framework STASE (Static Analysis–Guided Symbolic Execution) has uncovered previously unknown UEFI and Linux kernel vulnerabilities, confirmed multiple CVEs, and is being transitioned into U.S. Army adversarial-testing workflows. My current work extends these ideas with LLM- and agentic systems that synthesize harnesses, environment models, and machine-checkable vulnerability signatures.

My dissertation builds toward a single pipeline that can find, confirm, and repair memory-safety bugs in real code. Its centerpiece, SAILOR, pairs rule-based static analysis with LLM-orchestrated symbolic execution and a concrete, sanitizer-backed validation gate. Run against widely used C and C++ projects, it has uncovered 30+ previously unknown memory-safety vulnerabilities, several now patched upstream.

Program analysis & formal methods Symbolic execution Software & firmware security CodeQL / Static Analysis LLM-Driven Program Reasoning

Research

Focus & Vision

Research Interests

  • Building trust in AI-assisted systems. Precision–scalability trade-offs among static analysis, symbolic execution, fuzzing, and dynamic verification for secure-by-construction code and patches in human–LLM co-authored software.
  • Scaling formal methods with AI. Automating contracts, harnesses, invariants, and machine-checkable evidence so verification scales to large, safety- and mission-critical software and systems.
  • LLMs and agentic systems for software engineering. Symbolic-reasoning models and collaborative agents that generate harnesses, triage findings, and explain security guarantees.
  • Cyber defense automation. AI- and formal-methods-driven workflows for automated security assessment, end-to-end exploit discovery, triage, and mitigation.

Current Projects

  • SAILOR
    Static-analysis-guided, LLM-orchestrated symbolic execution with sanitizer-backed validation: finds, reproduces, and confirms memory-safety vulnerabilities in real-world C and C++ codebases.
  • STASE
    Static analysis guided symbolic execution for firmware and software: automatic harness generation, environment modeling, and vulnerability signature extraction.
  • CHAINER
    Memory-aware symbolic analysis to discover exploit chains that combine multiple low-level bugs into high-impact attacks.
  • Verified Patching
    Proving an automated or LLM-generated patch removes the whole bug class and changes nothing else, via self-differential equivalence over symbolic execution. Early prototype, evaluated on real CVE cases.

News

Updates
  • Sep 2026
    Credited as an independent reporter on the maintainers' published security advisory for a heap out-of-bounds read I found in liboqs (post-quantum cryptography). GHSA-wh5q-mpc8-67wf
  • Sep 2026
    Reported stack-buffer overflow fix merged upstream in encodec.cpp (Meta's EnCodec audio model, PABannier's C/C++ port). Pull request #57
  • Aug 2026
    DARPA's four-year HARDEN program is completing. Our UCSB Verification Lab team was the only bug-discovery (TA1) performer to advance through to the program's final phase, on the strength of STASE. Building on those results, our lab has transitioned into DARPA's new INGOTS program on automated exploit-chain discovery and analysis.
  • Aug 2026
    SAILOR, my LLM-orchestrated symbolic execution framework, is under submission. Its coordinated disclosures now span 30+ previously unknown memory-safety vulnerabilities across widely used C and C++ projects, several patched upstream. See Findings.
  • Jun 2026
    Advanced to Ph.D. candidacy and presented my dissertation proposal, Scalable Symbolic Execution for Vulnerability Detection and Patch Verification.
  • Oct 2025
    Demoed STASE at the DARPA HARDEN PI meeting. Watch the demo
  • Sep 2025
    VLab received a new DARPA HARDEN Phase 3 contract with approximately 3× increased funding, under which the STASE tool will be transitioned into U.S. Army adversarial testing workflows.
  • Jul 2025
    After Evaluation 3 at the end of Phase 2 of the DARPA HARDEN program, STASE was recognized as having the highest usability, with the greatest range of outputs and a high degree of automation among participating tools.

I periodically update this section with new papers, talks, and tool releases.

Security Findings

Responsible Disclosure

Vulnerabilities my research has found and disclosed in widely used, real-world C and C++ software. Every finding is confirmed by a concrete sanitizer crash on a synthesized input before it is reported, then disclosed responsibly upstream. This list grows as coordination completes; specifics stay withheld until each report is public.

30+
Zero-days disclosed
18
Real-world codebases
9
Upstream fix or advisory
100%
Sanitizer-confirmed
mruby Patched upstream
Integer overflow to out-of-bounds write in class_add_range.
CWE-190 to CWE-787
Issue #6937, fixed by Matz
SELinux (checkpolicy) Merged upstream
Double free in define_genfs_context_helper.
CWE-415
Merged fix, Acked-by S. Smalley
whisper.cpp Fix PR
Out-of-bounds read in log_mel_spectrogram on crafted audio.
CWE-125
Pull request #3956
whisper.cpp Fix PR
Stack-buffer overflow write via unchecked n_dims in the model loader.
CWE-787
Pull request #3957
bark.cpp Fix PR
Stack-buffer overflow write in the model loader and offline quantizer.
CWE-787
Pull request #220
encodec.cpp Merged upstream
Stack-buffer overflow write in encodec_load_model_weights.
CWE-787
Pull request #57, merged
liboqs Published advisory
Heap out-of-bounds read in LMS/HSS signature verification via unvalidated signature length.
CWE-125
Advisory GHSA-wh5q-mpc8-67wf
biogpt.cpp Fix accepted
Stack-buffer overflow write via unchecked n_dims in biogpt_model_load.
CWE-787
Pull request #27
koboldcpp Published advisory, High
Stack-buffer overflow write via unbounded n_dims across 6 legacy model loaders.
CWE-787
Advisory GHSA-qhvp-gj7g-rw26
Under coordinated disclosure. Additional confirmed findings are in maintainer hands and not yet public, including memory-safety bugs in tinyexr, hnswlib, usearch, Annoy, stable-diffusion.cpp, minja, OpenFHE, CTranslate2, and the llama.cpp / ggml stack. Each will be listed here in detail once its report is public.

Reproductions of already-known issues are excluded and not counted.

Research Outputs

Publications & Artifacts

Selected Publications

  1. SAILOR: Guiding Symbolic Execution for Memory Safety Vulnerability Detection. Under submission to USENIX Security, 2027.
  2. PAGENT: Program Analysis Guided LLM Agent for Proof-of-Concept Generation. ISSTA 2026. Artifacts Available & Functional
  3. Bug Composition: Triggering Multiple Bugs with Agentic Driver Generation. AgenticDev 2026 Workshop.
  4. Stateful Behavior Inference and Runtime Enforcement for Vehicle Network Security. USENIX VehicleSec 2025.
    Conference page
  5. STASE: Static Analysis Guided Symbolic Execution for UEFI Vulnerability Signature Generation. ASE 2024. A*
    DOI: 10.1145/3691620.3695543
  6. Rare Path Guided Fuzzing. ISSTA 2023.
    DOI: 10.1145/3597926.3598136
  7. CHAINER: Under submission.
  8. Verified Patching: In preparation, targeting FSE.

Full list on Google Scholar.

Artifacts & Tools

  • STASE 2.0 — Static Analysis–Guided Symbolic Execution.
    Hybrid static–symbolic framework for firmware and software, including automatic harness generation, environment modeling, and vulnerability signature extraction. In DARPA HARDEN it produced precise, zero-false-positive signatures, including 5 of the 9 PixieFail vulnerabilities and 13 new EDK2 firmware bugs.
    github.com/shafiuzzaman-md/stase-2.0
  • ChainBench — Vulnerability Chain Dataset.
    Curated dataset and harness suite for exploit-chain analysis and evaluation of chain discovery techniques.
    github.com/shafiuzzaman-md/chainbench
  • klee_harness — Educational KLEE Harness Examples.
    A small open-source repository demonstrating KLEE harness patterns used in mentoring ERSP students on symbolic execution.
    github.com/shafiuzzaman-md/klee_harness

Industry & Skills

Practice & Tooling

Industry Experience

  • Software Engineer Intern, Office of Research, UC Santa Barbara (Summer 2022)
    Integrated CAS single sign-on for enterprise apps and added role-based access control. (C#/.NET)
  • Software Engineer, Mobil Jamuna Lubricants, Bangladesh (2016–2018)
    Re-engineered data pipelines and authentication layers in the Lube Enterprise System, strengthening data integrity and security across inventory, billing, and reporting. (C#/.NET, JavaScript, MySQL)
  • Junior Software Engineer / Intern, Wolters Kluwer, Bangladesh (offshore, 2014–2016)
    Modernized financial compliance modules handling sensitive U.S. mortgage data with stronger input validation and expanded test coverage; introduced CI-friendly tests and migration scripts, reducing regression defects across releases. (C#/.NET, Angular/TypeScript, WebAPI, MS SQL)

Technical Skills

  • AI & LLMs. Prompt/agent design for code analysis, retrieval-augmented triage, and evidence-bearing spec/claim loops.
  • Formal Methods & Program Analysis. SMT solvers (Z3, Boolector), symbolic execution (KLEE), abstract interpretation, slicing, Datalog.
  • Security & Testing. Fuzzing (AFL++, libFuzzer), sanitizers (ASan/UBSan/MSan), exploit-chain modeling.
  • Systems & Toolchains. LLVM/Clang, GCC, Linux kernel build environments, UEFI EDK2.
  • DevOps & Scale. Docker, GitHub Actions (CI/CD).
  • Programming Languages. Python, C, C#, Java, JavaScript/TypeScript, Go, Racket/Rosette, SMT-LIB.

Teaching

Courses & Mentoring

Teaching Experience

  • Instructor, UCSB, Summer 2022 — CMPSC 130A: Data Structures & Algorithms I.
    Materials: github.com/shafiuzzaman-md/CS130A_Summer2022
  • Teaching Assistant, UCSB, 2021–2022 — Databases, Data Structures & Algorithms I/II.
  • Lecturer, Jashore University of Science & Technology, 2018–2021 — Software Engineering; Structured Programming; Algorithm Analysis & Design; Software Testing & Operations.
  • Pedagogy Training, UCSB STIA Program .
    Participated in teaching-development modules on learning objectives, lesson planning, assessment, and inclusive teaching practices.

Academic Leadership & Student Mentoring

  • Graduate Student Mentor, Graduate Scholars Program (GSP), UCSB Graduate Division (2025–2026).
  • Undergraduate Research Mentor, ERSP, UCSB Computer Science (2023–2024; 2025–2026).
    Cohort projects on vulnerability signature generation and LLM-assisted harness generation for fuzzing and symbolic execution. A mentored cohort's work was published at the AgenticDev 2026 workshop (Bug Composition, with three ERSP undergraduate authors).

Grants & Service

Community & Outreach

Grants & Proposals (Contributor / Co-Author)

  • DARPA ASEMA (2025): Assessing Security of Encrypted Messaging Applications.
  • Sony Research Award Program (2025): LLM-enhanced formal methods for embedded Linux security.
  • NSF Future CoRe/SHF (2025): Secure and verifiable code generation via specialized agents.
  • NSF SaTC Medium (2024): Side-channels — proofs, attacks, and defenses.
  • DARPA TRACTOR (2024): Translating C to Rust.
  • Amazon Trusted Crypto (2024): Detecting and quantifying information leakages in crypto libraries.
  • U.S. Army TARDEC (2023): Validating vehicle communications between trusted and untrusted control systems.

Professional Service

  • Program Committees & Reviewing. Sub-reviewer for premier software engineering venues, including ICSE, ASE, FSE, and ISSTA; Artifact Evaluation participation.
  • Open Science & Community. Maintainer of open-source research artifacts (STASE, ChainBench); contributor to reproducible containerized evaluation pipelines; frequent lab demos and internal tutorials on symbolic execution, CodeQL, and LLM-assisted program analysis.

Honors & Talks

Recognition & Presentations

Honors & Awards

  • UCSB Chancellor's Scholarship, University of California, Santa Barbara (2024).
  • Academic Excellence Fellowship, University of California, Santa Barbara (2021).
  • National Merit Scholarship, Government of Bangladesh (top 0.25% of cohort).

Selected Talks & Demos

  • STASE conference presentation, IEEE/ACM ASE 2024.
  • STASE live demo, DARPA HARDEN PI meeting (Oct 2025). Watch

Contact

Get in Touch

I am happy to discuss faculty positions, industry research and applied-science roles, and collaborative research in software security, formal methods, and AI-assisted program analysis.

The best way to reach me is by email: mdshafiuzzaman@ucsb.edu. Please include a brief description of your interests or the position you are contacting me about.

Profiles: Google Scholar · DBLP · GitHub · LinkedIn.