Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts

Zilong Wang; Gideon Mohr; Klaus von Gleissenthall; Jan Reineke; Marco Guarnieri

doi:10.1145/3576915.3623192

Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts

Zilong Wang
, Gideon Mohr
, Klaus von Gleissenthall
, Jan Reineke
, Marco Guarnieri

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

Abstract

Leakage contracts have recently been proposed as a new security abstraction at the Instruction Set Architecture (ISA) level. Leakage contracts aim to capture the information that processors leak through their microarchitectural implementations. However, so far, we lack a methodology to verify that a processor actually satisfies a given leakage contract. In this paper, we address this challenge by developing LeaVe, the first tool for verifying register-transfer-level (RTL) processor designs against ISA-level leakage contracts. To this end, we show how to decouple security and functional correctness concerns. LeaVe leverages this decoupling to make verification of contract satisfaction practical. To scale to realistic processor designs, LeaVe further employs inductive reasoning on relational abstractions. Using LeaVe, we precisely characterize the side-channel security guarantees of three open-source RISC-V processors, thereby obtaining the first proofs of contract satisfaction for RTL processor designs.

Original language	English
Title of host publication	CCS 2023
Subtitle of host publication	Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security
Publisher	Association for Computing Machinery, Inc
Pages	2128-2142
Number of pages	15
ISBN (Electronic)	9798400700507
DOIs	https://doi.org/10.1145/3576915.3623192
Publication status	Published - 2023
Event	30th ACM SIGSAC Conference on Computer and Communications Security, CCS 2023 - Copenhagen, Denmark Duration: 26 Nov 2023 → 30 Nov 2023

Conference

Conference	30th ACM SIGSAC Conference on Computer and Communications Security, CCS 2023
Country/Territory	Denmark
City	Copenhagen
Period	26/11/23 → 30/11/23

Funding

We would like to thank Alastair Reid and Piotr Sapiecha for feedback and discussions. This project has received funding from the European Research Council under the European Union's Horizon 2020 research and innovation programme (grant agreement No. 101020415), from the Spanish Ministry of Science and Innovation under the project TED2021-132464B-I00 PRODIGY, from the Spanish Ministry of Science and Innovation under the Ramón y Cajal grant RYC2021-032614-I, from the Spanish Ministry of Science and Innovation under the project PID2022-142290OB-I00 ESPADA, and from a gift by Intel Corporation. We would like to thank Alastair Reid and Piotr Sapiecha for feedback and discussions. This project has received funding from the European Research Council under the European Union’s Horizon 2020 research and innovation programme (grant agreement No. 101020415), from the Spanish Ministry of Science and Innovation under the project TED2021-132464B-I00 PRODIGY, from the Spanish Ministry of Science and Innovation under the Ramón y Cajal grant RYC2021-032614-I, from the Spanish Ministry of Science and Innovation under the project PID2022-142290OB-I00 ESPADA, and from a gift by Intel Corporation.

Funders	Funder number
Intel Corporation
European Research Council
Horizon 2020
???publication-publication-funding-organisation-not-added???	101020415
Ministerio de Ciencia e Innovación	RYC2021-032614-I, PID2022-142290OB-I00 ESPADA, TED2021-132464B-I00

Access to Document

10.1145/3576915.3623192Licence: CC BY

Persistent URL (handle)

Persistent link

Cite this

Wang, Z., Mohr, G., von Gleissenthall, K., Reineke, J., & Guarnieri, M. (2023). Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts. In CCS 2023: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (pp. 2128-2142). Association for Computing Machinery, Inc. https://doi.org/10.1145/3576915.3623192

@inproceedings{2ac9d583d8974122a9d25ece1b004010,

title = "Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts",

abstract = "Leakage contracts have recently been proposed as a new security abstraction at the Instruction Set Architecture (ISA) level. Leakage contracts aim to capture the information that processors leak through their microarchitectural implementations. However, so far, we lack a methodology to verify that a processor actually satisfies a given leakage contract. In this paper, we address this challenge by developing LeaVe, the first tool for verifying register-transfer-level (RTL) processor designs against ISA-level leakage contracts. To this end, we show how to decouple security and functional correctness concerns. LeaVe leverages this decoupling to make verification of contract satisfaction practical. To scale to realistic processor designs, LeaVe further employs inductive reasoning on relational abstractions. Using LeaVe, we precisely characterize the side-channel security guarantees of three open-source RISC-V processors, thereby obtaining the first proofs of contract satisfaction for RTL processor designs.",

author = "Zilong Wang and Gideon Mohr and \{von Gleissenthall\}, Klaus and Jan Reineke and Marco Guarnieri",

year = "2023",

doi = "10.1145/3576915.3623192",

language = "English",

pages = "2128--2142",

booktitle = "CCS 2023",

publisher = "Association for Computing Machinery, Inc",

note = "30th ACM SIGSAC Conference on Computer and Communications Security, CCS 2023 ; Conference date: 26-11-2023 Through 30-11-2023",

}

Wang, Z, Mohr, G, von Gleissenthall, K, Reineke, J & Guarnieri, M 2023, Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts. in CCS 2023: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security. Association for Computing Machinery, Inc, pp. 2128-2142, 30th ACM SIGSAC Conference on Computer and Communications Security, CCS 2023, Copenhagen, Denmark, 26/11/23. https://doi.org/10.1145/3576915.3623192

Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts. / Wang, Zilong; Mohr, Gideon; von Gleissenthall, Klaus et al.
CCS 2023: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security. Association for Computing Machinery, Inc, 2023. p. 2128-2142.

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

TY - GEN

T1 - Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts

AU - Wang, Zilong

AU - Mohr, Gideon

AU - von Gleissenthall, Klaus

AU - Reineke, Jan

AU - Guarnieri, Marco

PY - 2023

Y1 - 2023

N2 - Leakage contracts have recently been proposed as a new security abstraction at the Instruction Set Architecture (ISA) level. Leakage contracts aim to capture the information that processors leak through their microarchitectural implementations. However, so far, we lack a methodology to verify that a processor actually satisfies a given leakage contract. In this paper, we address this challenge by developing LeaVe, the first tool for verifying register-transfer-level (RTL) processor designs against ISA-level leakage contracts. To this end, we show how to decouple security and functional correctness concerns. LeaVe leverages this decoupling to make verification of contract satisfaction practical. To scale to realistic processor designs, LeaVe further employs inductive reasoning on relational abstractions. Using LeaVe, we precisely characterize the side-channel security guarantees of three open-source RISC-V processors, thereby obtaining the first proofs of contract satisfaction for RTL processor designs.

AB - Leakage contracts have recently been proposed as a new security abstraction at the Instruction Set Architecture (ISA) level. Leakage contracts aim to capture the information that processors leak through their microarchitectural implementations. However, so far, we lack a methodology to verify that a processor actually satisfies a given leakage contract. In this paper, we address this challenge by developing LeaVe, the first tool for verifying register-transfer-level (RTL) processor designs against ISA-level leakage contracts. To this end, we show how to decouple security and functional correctness concerns. LeaVe leverages this decoupling to make verification of contract satisfaction practical. To scale to realistic processor designs, LeaVe further employs inductive reasoning on relational abstractions. Using LeaVe, we precisely characterize the side-channel security guarantees of three open-source RISC-V processors, thereby obtaining the first proofs of contract satisfaction for RTL processor designs.

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

UR - https://www.scopus.com/pages/publications/85179841369#tab=citedBy

U2 - 10.1145/3576915.3623192

DO - 10.1145/3576915.3623192

M3 - Conference contribution

SP - 2128

EP - 2142

BT - CCS 2023

PB - Association for Computing Machinery, Inc

T2 - 30th ACM SIGSAC Conference on Computer and Communications Security, CCS 2023

Y2 - 26 November 2023 through 30 November 2023

ER -

Wang Z, Mohr G, von Gleissenthall K, Reineke J, Guarnieri M. Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts. In CCS 2023: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security. Association for Computing Machinery, Inc. 2023. p. 2128-2142 Epub 2021 Nov 21. doi: 10.1145/3576915.3623192

Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts

Abstract

Conference

Funding

Access to Document

Persistent URL (handle)

Other files and links

Fingerprint

Cite this