BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//pretalx//pretalx.coscup.org//coscup-2026//talk//VQNU3N
BEGIN:VTIMEZONE
TZID:CST
BEGIN:STANDARD
DTSTART:20000101T000000
RRULE:FREQ=YEARLY;BYMONTH=1
TZNAME:CST
TZOFFSETFROM:+0800
TZOFFSETTO:+0800
END:STANDARD
END:VTIMEZONE
BEGIN:VEVENT
UID:pretalx-coscup-2026-VQNU3N@pretalx.coscup.org
DTSTART;TZID=CST:20260809T113000
DTEND;TZID=CST:20260809T120000
DESCRIPTION:Firmware underpins system security but remains challenging to v
 erify due to hardware dependency\, specialized coding idioms\, and limited
  open-source examples. Manual verification approaches\, while common in in
 dustry\, 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 (T
 DX)\, known as TDX Module. In this study\, we employ six state-of-the-art 
 C-program analyzers on the production TDX Module firmware\, leveraging tec
 hniques ranging from bounded model checking and symbolic execution to abst
 ract 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 sli
 cing for more scalable verification. Although the case study focuses on TD
 X 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 verific
 ation tasks and proof harnesses are publicly released to foster reproducib
 le research and future tool development.
DTSTAMP:20260713T142756Z
LOCATION:TR515
SUMMARY:A Case Study in Firmware Verification: Applying Formal Methods to I
 ntel® TDX Module - Nian-Ze Lee
URL:https://pretalx.coscup.org/coscup-2026/talk/VQNU3N/
END:VEVENT
END:VCALENDAR