XcptProof: Formal Verification of CPU Exception Transient Execution Security via Leakage Contracts

Shixuan Zhang; Yujia Zhang; Kexin Gong; Hongpeng Wang; Haixia Wang; Dongsheng Wang

doi:10.1145/3787109.3815242

XcptProof: Formal Verification of CPU Exception Transient Execution Security via Leakage Contracts

Shixuan Zhang
, Yujia Zhang
, Kexin Gong
, Hongpeng Wang^*
, Haixia Wang^*
, Dongsheng Wang

^*Corresponding author for this work

Harbin Institute of Technology Shenzhen
Pengcheng Laboratory
Tsinghua University

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

Abstract

Transient execution attacks triggered by CPU exceptions, such as Meltdown and MDS-type attacks, have compromised system security. Unfortunately, no prior work has conducted a formalized analysis of the CPU exception transient execution security. To bridge this gap, we propose a framework, XcptProof, which primarily consists of two components: (1) defining exception-related hardware-software contracts to model the CPU's leakage capabilities, and (2) utilizing a formal verification methods to exhaustively analyze the CPU's satisfiability of given contracts. We introduce a miter-circuit based detection model and further incorporate a frontend-backend decoupling approach to optimize efficiency. XcptProof successfully verifies 49 contracts on the BOOM processor and confirms the effectiveness of the frontend-backend decoupling optimization.

Original language	English
Title of host publication	GLSVLSI 2026 - Proceedings of the Great Lakes Symposium on VLSI 2026
Editors	Fan Chen, Peipei Zhou, Jie Gu, Amit R. Trivedi, Xiaoxuan Yang
Publisher	Association for Computing Machinery, Inc
Pages	665-671
Number of pages	7
ISBN (Electronic)	9798400724312
DOIs	https://doi.org/10.1145/3787109.3815242
State	Published - 22 Jun 2026
Externally published	Yes
Event	36th Great Lakes Symposium on VLSI, GLSVLSI 2026 - Canandaigua, United States Duration: 22 Jun 2026 → 24 Jun 2026

Publication series

Name	GLSVLSI 2026 - Proceedings of the Great Lakes Symposium on VLSI 2026

Conference

Conference	36th Great Lakes Symposium on VLSI, GLSVLSI 2026
Country/Territory	United States
City	Canandaigua
Period	22/06/26 → 24/06/26

Keywords

CPU exception
Microarchitectural security
formal hardware verification
leakage contract
transient execution attack

Access to Document

10.1145/3787109.3815242

Cite this

Zhang, S., Zhang, Y., Gong, K., Wang, H., Wang, H., & Wang, D. (2026). XcptProof: Formal Verification of CPU Exception Transient Execution Security via Leakage Contracts. In F. Chen, P. Zhou, J. Gu, A. R. Trivedi, & X. Yang (Eds.), GLSVLSI 2026 - Proceedings of the Great Lakes Symposium on VLSI 2026 (pp. 665-671). (GLSVLSI 2026 - Proceedings of the Great Lakes Symposium on VLSI 2026). Association for Computing Machinery, Inc. https://doi.org/10.1145/3787109.3815242

Zhang, Shixuan ; Zhang, Yujia ; Gong, Kexin et al. / XcptProof : Formal Verification of CPU Exception Transient Execution Security via Leakage Contracts. GLSVLSI 2026 - Proceedings of the Great Lakes Symposium on VLSI 2026. editor / Fan Chen ; Peipei Zhou ; Jie Gu ; Amit R. Trivedi ; Xiaoxuan Yang. Association for Computing Machinery, Inc, 2026. pp. 665-671 (GLSVLSI 2026 - Proceedings of the Great Lakes Symposium on VLSI 2026).

@inproceedings{9746e59796fc4ac2bf2b173bf263e2ab,

title = "XcptProof: Formal Verification of CPU Exception Transient Execution Security via Leakage Contracts",

abstract = "Transient execution attacks triggered by CPU exceptions, such as Meltdown and MDS-type attacks, have compromised system security. Unfortunately, no prior work has conducted a formalized analysis of the CPU exception transient execution security. To bridge this gap, we propose a framework, XcptProof, which primarily consists of two components: (1) defining exception-related hardware-software contracts to model the CPU's leakage capabilities, and (2) utilizing a formal verification methods to exhaustively analyze the CPU's satisfiability of given contracts. We introduce a miter-circuit based detection model and further incorporate a frontend-backend decoupling approach to optimize efficiency. XcptProof successfully verifies 49 contracts on the BOOM processor and confirms the effectiveness of the frontend-backend decoupling optimization.",

keywords = "CPU exception, Microarchitectural security, formal hardware verification, leakage contract, transient execution attack",

author = "Shixuan Zhang and Yujia Zhang and Kexin Gong and Hongpeng Wang and Haixia Wang and Dongsheng Wang",

note = "Publisher Copyright: {\textcopyright} 2026 Copyright held by the owner/author(s).; 36th Great Lakes Symposium on VLSI, GLSVLSI 2026 ; Conference date: 22-06-2026 Through 24-06-2026",

year = "2026",

month = jun,

day = "22",

doi = "10.1145/3787109.3815242",

language = "英语",

series = "GLSVLSI 2026 - Proceedings of the Great Lakes Symposium on VLSI 2026",

publisher = "Association for Computing Machinery, Inc",

pages = "665--671",

editor = "Fan Chen and Peipei Zhou and Jie Gu and Trivedi, \{Amit R.\} and Xiaoxuan Yang",

booktitle = "GLSVLSI 2026 - Proceedings of the Great Lakes Symposium on VLSI 2026",

}

Zhang, S, Zhang, Y, Gong, K, Wang, H, Wang, H & Wang, D 2026, XcptProof: Formal Verification of CPU Exception Transient Execution Security via Leakage Contracts. in F Chen, P Zhou, J Gu, AR Trivedi & X Yang (eds), GLSVLSI 2026 - Proceedings of the Great Lakes Symposium on VLSI 2026. GLSVLSI 2026 - Proceedings of the Great Lakes Symposium on VLSI 2026, Association for Computing Machinery, Inc, pp. 665-671, 36th Great Lakes Symposium on VLSI, GLSVLSI 2026, Canandaigua, United States, 22/06/26. https://doi.org/10.1145/3787109.3815242

XcptProof: Formal Verification of CPU Exception Transient Execution Security via Leakage Contracts. / Zhang, Shixuan; Zhang, Yujia; Gong, Kexin et al.
GLSVLSI 2026 - Proceedings of the Great Lakes Symposium on VLSI 2026. ed. / Fan Chen; Peipei Zhou; Jie Gu; Amit R. Trivedi; Xiaoxuan Yang. Association for Computing Machinery, Inc, 2026. p. 665-671 (GLSVLSI 2026 - Proceedings of the Great Lakes Symposium on VLSI 2026).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - XcptProof

T2 - 36th Great Lakes Symposium on VLSI, GLSVLSI 2026

AU - Zhang, Shixuan

AU - Zhang, Yujia

AU - Gong, Kexin

AU - Wang, Hongpeng

AU - Wang, Haixia

AU - Wang, Dongsheng

PY - 2026/6/22

Y1 - 2026/6/22

N2 - Transient execution attacks triggered by CPU exceptions, such as Meltdown and MDS-type attacks, have compromised system security. Unfortunately, no prior work has conducted a formalized analysis of the CPU exception transient execution security. To bridge this gap, we propose a framework, XcptProof, which primarily consists of two components: (1) defining exception-related hardware-software contracts to model the CPU's leakage capabilities, and (2) utilizing a formal verification methods to exhaustively analyze the CPU's satisfiability of given contracts. We introduce a miter-circuit based detection model and further incorporate a frontend-backend decoupling approach to optimize efficiency. XcptProof successfully verifies 49 contracts on the BOOM processor and confirms the effectiveness of the frontend-backend decoupling optimization.

AB - Transient execution attacks triggered by CPU exceptions, such as Meltdown and MDS-type attacks, have compromised system security. Unfortunately, no prior work has conducted a formalized analysis of the CPU exception transient execution security. To bridge this gap, we propose a framework, XcptProof, which primarily consists of two components: (1) defining exception-related hardware-software contracts to model the CPU's leakage capabilities, and (2) utilizing a formal verification methods to exhaustively analyze the CPU's satisfiability of given contracts. We introduce a miter-circuit based detection model and further incorporate a frontend-backend decoupling approach to optimize efficiency. XcptProof successfully verifies 49 contracts on the BOOM processor and confirms the effectiveness of the frontend-backend decoupling optimization.

KW - CPU exception

KW - Microarchitectural security

KW - formal hardware verification

KW - leakage contract

KW - transient execution attack

UR - https://www.scopus.com/pages/publications/105045064149

U2 - 10.1145/3787109.3815242

DO - 10.1145/3787109.3815242

M3 - 会议稿件

AN - SCOPUS:105045064149

T3 - GLSVLSI 2026 - Proceedings of the Great Lakes Symposium on VLSI 2026

SP - 665

EP - 671

BT - GLSVLSI 2026 - Proceedings of the Great Lakes Symposium on VLSI 2026

A2 - Chen, Fan

A2 - Zhou, Peipei

A2 - Gu, Jie

A2 - Trivedi, Amit R.

A2 - Yang, Xiaoxuan

PB - Association for Computing Machinery, Inc

Y2 - 22 June 2026 through 24 June 2026

ER -

Zhang S, Zhang Y, Gong K, Wang H, Wang H, Wang D. XcptProof: Formal Verification of CPU Exception Transient Execution Security via Leakage Contracts. In Chen F, Zhou P, Gu J, Trivedi AR, Yang X, editors, GLSVLSI 2026 - Proceedings of the Great Lakes Symposium on VLSI 2026. Association for Computing Machinery, Inc. 2026. p. 665-671. (GLSVLSI 2026 - Proceedings of the Great Lakes Symposium on VLSI 2026). doi: 10.1145/3787109.3815242

XcptProof: Formal Verification of CPU Exception Transient Execution Security via Leakage Contracts

Abstract

Publication series

Conference

Keywords

Access to Document

Other files and links

Fingerprint

Cite this