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 program. 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.
Research
Research Interests
- Building trust in AI-assisted systems. Precision–scalability trade-offs among static analysis, symbolic execution, 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
-
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. -
CEGIR-Harness
Static-analysis-driven, LLM-assisted counterexample-guided iterative refinement of symbolic execution harnesses.
News
-
Nov 2025Collaborating with ASU, Kudu Dynamics, and Galois within DARPA’s HARDEN program on a language of triggers for automating vulnerability signatures and exploit-chain discovery.
-
Sep 2025VLab 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.
-
Aug 2025Our paper “Stateful Behavior Inference and Runtime Enforcement for Vehicle Network Security” was accepted to USENIX VehicleSec 2025.
-
Jul 2025After 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.
Research Outputs
Selected Publications
-
Stateful Behavior Inference and Runtime Enforcement for Vehicle Network Security.
USENIX VehicleSec 2025.
Conference page -
STASE: Static Analysis Guided Symbolic Execution for UEFI Vulnerability Signature Generation.
ASE 2024. A*
DOI: 10.1145/3691620.3695543 -
Rare Path Guided Fuzzing. ISSTA 2023.
DOI: 10.1145/3597926.3598136 - CHAINER: Under submission.
- CEGIR-Harness: Under submission.
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.
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
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, USA (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
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.
Grants & Service
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.
Contact
I am happy to discuss opportunities related to faculty positions, collaborative research, and student supervision 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.