Zimmer, V. (2026). Machine-Checked Linear Temporal Logic for the UEFI Capsule Update Process: A Foundational Proof of Authenticity, Anti-Rollback, and Responsiveness. Zenodo. IEEE Cyber Awareness & Research Symposium 2026 (CARS 2026)
Accepted Paper - permanent record
Machine-Checked Linear Temporal Logic for the UEFI Capsule Update Process
This repository contains the formal verification source code and Lean proofs associated with the research paper: **"Machine-Checked Linear Temporal Logic for the UEFI Capsule Update Process: A Foundational Proof of Authenticity, Anti-Rollback, and Responsiveness"** presented at the 2026 IEEE Cyber Awareness and Research Symposium (CARS 2026).
Abstract
The Unified Extensible Firmware Interface (UEFI) Capsule Update process serves as the foundational mechanism for updating system firmware securely. However, verification gaps in implementation can lead to severe system vulnerabilities, including firmware rollbacks or permanent device bricking. In this work, we present a mathematically rigorous, machine-checked verification of the capsule update protocol using Linear Temporal Logic (LTL). We formally model and verify three foundational properties of the update lifecycle: Authenticity (ensuring untrusted payloads are never flashed), Anti-Rollback (guaranteeing monotonic version progression), and Responsiveness (proving eventual termination and liveness under recovery scenarios). The complete proof is mechanized, establishing an architectural blueprint for safety-critical hardware platforms.
Full Text PDF: Download Accepted Manuscript via Google Drive
Persistent Record: Zenodo Repository
If you use this work or the associated proofs in an academic context, please use the following citation format:
@inproceedings{zimmer2026machine,
title={Machine-Checked Linear Temporal Logic for the UEFI Capsule Update Process: A Foundational Proof of Authenticity, Anti-Rollback, and Responsiveness},
author={Zimmer, Vincent and et al.},
booktitle={Proceedings of the 2026 IEEE Cyber Awareness and Research Symposium (CARS)},
year={2026},
publisher={IEEE}
}
IEEE Copyright Notice
Accepted for publication at the 2026 IEEE Cyber Awareness and Research Symposium (CARS).
© 2026 IEEE. Personal use of this material is permitted. Permission from IEEE must be obtained for all other uses, in any current or future media, including reprinting/republishing this material for advertising or promotional purposes, creating new collective works, for resale or redistribution to servers or lists, or reuse of any copyrighted component of this work in other works.