Nian-Ze Lee
Dr. Nian-Ze Lee is an Assistant Professor in the Department of Electrical Engineering at National Taiwan University (NTUEE), a position he has held since February 2025, and a Visiting Professor at the Institute of Informatics, LMU Munich, Germany. He earned his Ph.D. in Electronics Engineering from NTU in 2021, where he was selected as an honorary member of the Phi Tau Phi Scholastic Honor Society. His dissertation on stochastic Boolean satisfiability received the prestigious Lam Research Thesis Award. From 2021 to 2024, Dr. Lee was a Postdoctoral Researcher at LMU Munich, Germany, focusing on formal methods and their practical applications in software engineering and EDA. His work has been recognized at top-tier international conferences and earned several awards, including an ETAPS Distinguished Paper Award at TACAS 2026, an ACM SIGSOFT Distinguished Paper Award and a Best Artifact Award at FSE 2024, a Best Paper Award at SPIN 2024, and a Distinguished Artifact Award at TACAS 2024. As of 2026, he leads multiple research projects as a principal investigator, including a DFG-funded research project and an Intel-funded collaboration. From 2025 to 2028, he holds the Garmin Scholar Fellowship at NTU.
議程
Firmware underpins system security but remains challenging to verify due to hardware dependency, specialized coding idioms, and limited open-source examples. Manual verification approaches, while common in industry, are labor-intensive and difficult to scale. This paper presents a detailed case study on applying automatic formal methods for software to a security-critical firmware component in Intel Trust Domain Extensions (TDX), known as TDX Module. In this study, we employ six state-of-the-art C-program analyzers on the production TDX Module firmware, leveraging techniques ranging from bounded model checking and symbolic execution to abstract interpretation. Our empirical evaluation identifies obstacles unique to firmware, highlights harness-design decisions essential for verifying industry-scale code bases, and demonstrates opportunities in advanced slicing for more scalable verification. Although the case study focuses on TDX Module, the findings are broadly applicable to large-scale, low-level programs and have already influenced the software-verification community, such as standardizing nondeterministic object initialization. All verification tasks and proof harnesses are publicly released to foster reproducible research and future tool development.