Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts. Wang, Z., Mohr, G., von Gleissenthall, K., Reineke, J., & Guarnieri, M. In CCS, 2023. Distinguished Paper Award![Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts [pdf]](https://bibbase.org/img/filetypes/pdf.svg "pdf")
Paper abstract bibtex 8 downloads Leakage contracts have recently been proposed as a new security abstraction at the Instruction Set Architecture (ISA) level. Such contracts aim to faithfully capture the information processors may leak through side effects of their microarchitectural implementations. However, so far, we lack a verification methodology to check that a processor actually satisfies a given leakage contract. In this paper, we address this problem by developing LeaVe, the first tool for verifying register-transfer-level (RTL) processor designs against ISA-level leakage contracts. To this end, we introduce a decoupling theorem that separates security and functional correctness concerns when verifying contract satisfaction. 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 provided by three open-source RISC-V processors, thereby obtaining the first contract satisfaction proofs for RTL processor designs.
@inproceedings{wang_specification_2023,
title = {Specification and {Verification} of {Side}-channel {Security} for {Open}-source {Processors} via {Leakage} {Contracts}},
url = {https://gleissen.github.io/papers/ccs2023.pdf},
abstract = {Leakage contracts have recently been proposed as a new security abstraction at the Instruction Set Architecture (ISA) level. Such contracts aim to faithfully capture the information processors may leak through side effects of their microarchitectural implementations. However, so far, we lack a verification methodology to check that a processor actually satisfies a given leakage contract. In this paper, we address this problem by developing LeaVe, the first tool for verifying register-transfer-level (RTL) processor designs against ISA-level leakage contracts. To this end, we introduce a decoupling theorem that separates security and functional correctness concerns when verifying contract satisfaction. 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 provided by three open-source RISC-V processors, thereby obtaining the first contract satisfaction proofs for RTL processor designs.},
urldate = {2023-07-27},
booktitle = {{CCS}},
author = {Wang, Zilong and Mohr, Gideon and von Gleissenthall, Klaus and Reineke, Jan and Guarnieri, Marco},
year = {2023},
note = {Distinguished Paper Award},
keywords = {Computer Science - Cryptography and Security, type\_award, type\_conf, type\_paper, type\_tier1, type\_top},
}
Downloads: 8
{"_id":"qDEjnoH6Ecbrp3Q4D","bibbaseid":"wang-mohr-vongleissenthall-reineke-guarnieri-specificationandverificationofsidechannelsecurityforopensourceprocessorsvialeakagecontracts-2023","author_short":["Wang, Z.","Mohr, G.","von Gleissenthall, K.","Reineke, J.","Guarnieri, M."],"bibdata":{"bibtype":"inproceedings","type":"inproceedings","title":"Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts","url":"https://gleissen.github.io/papers/ccs2023.pdf","abstract":"Leakage contracts have recently been proposed as a new security abstraction at the Instruction Set Architecture (ISA) level. Such contracts aim to faithfully capture the information processors may leak through side effects of their microarchitectural implementations. However, so far, we lack a verification methodology to check that a processor actually satisfies a given leakage contract. In this paper, we address this problem by developing LeaVe, the first tool for verifying register-transfer-level (RTL) processor designs against ISA-level leakage contracts. To this end, we introduce a decoupling theorem that separates security and functional correctness concerns when verifying contract satisfaction. 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 provided by three open-source RISC-V processors, thereby obtaining the first contract satisfaction proofs for RTL processor designs.","urldate":"2023-07-27","booktitle":"CCS","author":[{"propositions":[],"lastnames":["Wang"],"firstnames":["Zilong"],"suffixes":[]},{"propositions":[],"lastnames":["Mohr"],"firstnames":["Gideon"],"suffixes":[]},{"propositions":["von"],"lastnames":["Gleissenthall"],"firstnames":["Klaus"],"suffixes":[]},{"propositions":[],"lastnames":["Reineke"],"firstnames":["Jan"],"suffixes":[]},{"propositions":[],"lastnames":["Guarnieri"],"firstnames":["Marco"],"suffixes":[]}],"year":"2023","note":"Distinguished Paper Award","keywords":"Computer Science - Cryptography and Security, type_award, type_conf, type_paper, type_tier1, type_top","bibtex":"@inproceedings{wang_specification_2023,\n\ttitle = {Specification and {Verification} of {Side}-channel {Security} for {Open}-source {Processors} via {Leakage} {Contracts}},\n\turl = {https://gleissen.github.io/papers/ccs2023.pdf},\n\tabstract = {Leakage contracts have recently been proposed as a new security abstraction at the Instruction Set Architecture (ISA) level. Such contracts aim to faithfully capture the information processors may leak through side effects of their microarchitectural implementations. However, so far, we lack a verification methodology to check that a processor actually satisfies a given leakage contract. In this paper, we address this problem by developing LeaVe, the first tool for verifying register-transfer-level (RTL) processor designs against ISA-level leakage contracts. To this end, we introduce a decoupling theorem that separates security and functional correctness concerns when verifying contract satisfaction. 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 provided by three open-source RISC-V processors, thereby obtaining the first contract satisfaction proofs for RTL processor designs.},\n\turldate = {2023-07-27},\n\tbooktitle = {{CCS}},\n\tauthor = {Wang, Zilong and Mohr, Gideon and von Gleissenthall, Klaus and Reineke, Jan and Guarnieri, Marco},\n\tyear = {2023},\n\tnote = {Distinguished Paper Award},\n\tkeywords = {Computer Science - Cryptography and Security, type\\_award, type\\_conf, type\\_paper, type\\_tier1, type\\_top},\n}\n\n","author_short":["Wang, Z.","Mohr, G.","von Gleissenthall, K.","Reineke, J.","Guarnieri, M."],"key":"wang_specification_2023","id":"wang_specification_2023","bibbaseid":"wang-mohr-vongleissenthall-reineke-guarnieri-specificationandverificationofsidechannelsecurityforopensourceprocessorsvialeakagecontracts-2023","role":"author","urls":{"Paper":"https://gleissen.github.io/papers/ccs2023.pdf"},"keyword":["Computer Science - Cryptography and Security","type_award","type_conf","type_paper","type_tier1","type_top"],"metadata":{"authorlinks":{}},"downloads":8},"bibtype":"inproceedings","biburl":"https://download.vusec.net/papers/zotero.php?tag=&full=1&format=bibtex&sort=date","dataSources":["LY5xkJFgS2sBQ9umB","JWcaY4xDbjG3msjWc","DLugeJAYYvwYZmqse","iLMsrq6FJma6GoJv6"],"keywords":["computer science - cryptography and security","type_award","type_conf","type_paper","type_tier1","type_top"],"search_terms":["specification","verification","side","channel","security","open","source","processors","via","leakage","contracts","wang","mohr","von gleissenthall","reineke","guarnieri"],"title":"Specification and Verification of Side-channel Security for Open-source Processors via Leakage Contracts","year":2023,"downloads":8}