More Web Proxy on the site http://driver.im/

research-article

Towards a formally verified hardware root-of-trust for data-oblivious computing

Authors:

Lucas Deutschmann,

Johannes Müller,

Mohammad R. Fadiheh,

Dominik Stoffel,

Wolfgang KunzAuthors Info & Claims

DAC '22: Proceedings of the 59th ACM/IEEE Design Automation Conference

Pages 727 - 732

https://doi.org/10.1145/3489517.3530981

Published: 23 August 2022 Publication History

Abstract

The importance of preventing microarchitectural timing side channels in security-critical applications has surged immensely over the last several years. Constant-time programming has emerged as a best-practice technique to prevent leaking out secret information through timing. It builds on the assumption that certain basic machine instructions execute timing-independently w.r.t. their input data. However, whether an instruction fulfills this data-independent timing criterion varies strongly from architecture to architecture.

In this paper, we propose a novel methodology to formally verify data-oblivious behavior in hardware using standard property checking techniques. Each successfully verified instruction represents a trusted hardware primitive for developing data-oblivious algorithms. A counterexample, on the other hand, represents a restriction that must be communicated to the software developer. We evaluate the proposed methodology in multiple case studies, ranging from small arithmetic units to medium-sized processors. One case study uncovered a data-dependent timing violation in the extensively verified and highly secure Ibex RISC-V core.

References

[1]

2018. BearSSL. https://www.bearssl.org/. (2018).

[2]

2018. SHA cores. https://opencores.org/projects/sha_core. (2018).

[3]

2021. Arm Armv8-A Architecture Registers. https://developer.arm.com. (2021).

[4]

2021. Featherweight RISC-V. https://github.com/Featherweight-IP/fwrisc. (2021).

[5]

2021. Ibex RISC-V Core. https://github.com/lowRISC/ibex. (2021).

[6]

2021. RISC-V Crypto Extension. https://github.com/riscv/riscv-crypto. (2021).

[7]

2021. SCARV. https://github.com/scarv/scarv-cpu. (2021).

[8]

2021. Trust-Hub. https://trust-hub.org. (2021).

[9]

2021. Zip CPU. https://github.com/ZipCPU/zipcpu. (2021).

[10]

José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, and Michael Emmi. 2016. Verifying constant-time implementations. In 25th USENIX Security Symposium (USENIX Security 16). 53--70.

[11]

Marc Andrysco, Andres Nötzli, Fraser Brown, Ranjit Jhala, and Deian Stefan. 2018. Towards verified, constant-time floating point operations. In Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security. 1369--1382.

Digital Library

[12]

Sunjay Cauligi, Craig Disselkoen, Klaus v Gleissenthall, Dean Tullsen, Deian Stefan, Tamara Rezk, and Gilles Barthe. 2020. Constant-time foundations for the new spectre era. In Proceedings of the 41st ACM SIGPLAN Conference on Programming Language Design and Implementation. 913--926.

Digital Library

[13]

Sunjay Cauligi, Gary Soeller, Fraser Brown, Brian Johannesmeyer, Yunlu Huang, Ranjit Jhala, and Deian Stefan. 2017. Fact: A flexible, constant-time programming language. In 2017 IEEE Cybersecurity Development (SecDev). IEEE, 69--76.

[14]

Bart Coppens, Ingrid Verbauwhede, Koen De Bosschere, and Bjorn De Sutter. 2009. Practical mitigations for timing-based side-channel attacks on modern x86 processors. In 2009 30th IEEE symposium on security and privacy. IEEE, 45--60.

Digital Library

[15]

Mohammad Rahmani Fadiheh, Dominik Stoffel, Clark Barrett, Subhasish Mitra, and Wolfgang Kunz. 2019. Processor Hardware Security Vulnerabilities and their Detection by Unique Program Execution Checking. In Design, Automation & Test in Europe Conf. (DATE). 994--999.

[16]

Mohammad Rahmani Fadiheh, Alex Wezel, Johannes Mueller, Joerg Bormann, Sayak Ray, Jason M Fung, Subhasish Mitra, Dominik Stoffel, and Wolfgang Kunz. 2021. An Exhaustive Approach to Detecting Transient Execution Side Channels in RTL Designs of Processors. arXiv preprint arXiv:2108.01979 (2021).

[17]

Christopher W Fletcher, Ling Ren, Albert Kwon, Marten Van Dijk, Emil Stefanov, Dimitrios Serpanos, and Srinivas Devadas. 2015. A low-latency, low-area hardware oblivious RAM controller. In 2015 IEEE 23rd Annual International Symposium on Field-Programmable Custom Computing Machines. IEEE, 215--222.

Digital Library

[18]

Klaus v Gleissenthall, Rami Gökhan Kıcı, Deian Stefan, and Ranjit Jhala. 2019. IODINE: Verifying Constant-Time Execution of Hardware. In 28th USENIX Security Symposium (USENIX Security 19). 1411--1428.

[19]

Rami Gokhan Kici, Klaus v Gleissenthall, Deian Stefan, and Ranjit Jhala. 2021. Solver-Aided Constant-Time Circuit Verification. arXiv preprint arXiv:2104.00461 (2021).

[20]

Joakim Urdahl, Dominik Stoffel, and Wolfgang Kunz. 2014. Path Predicate Abstraction for Sound System-Level Models of RT-Level Circuit Designs. IEEE Trans. on Comp.-Aided Design of Integrated Circuits & Systems 33, 2 (Feb. 2014), 291--304.

[21]

Jose Rodrigo Sanchez Vicarte, Pradyumna Shome, Nandeeka Nayak, Caroline Trippel, Adam Morrison, David Kohlbrenner, and Christopher W. Fletcher. 2021. Opening Pandora's Box: A Systematic Study of New Ways Microarchitecture Can Leak Private Data. In ACM/IEEE 48th Annual International Symposium on Computer Architecture (ISCA).

[22]

Jiyong Yu, Lucas Hsiung, Mohamad El Hajj, and Christopher W Fletcher. 2019. Data Oblivious ISA Extensions for Side Channel-Resistant and High Performance Computing. In The Network and Distributed System Security Symposium (NDSS).

[23]

F. Zaruba and L. Benini. 2019. The Cost of Application-Class Processing: Energy and Performance Analysis of a Linux-Ready 1.7-GHz 64-Bit RISC-V Core in 22-nm FDSOI Technology. IEEE Transactions on Very Large Scale Integration (VLSI) Systems 27, 11 (Nov 2019), 2629--2640.

Digital Library

Cited By

Müller JDuque Antón ADeutschmann LMehmedagić DRodrigues COliveira DRahmani Fadiheh MDevarajegowda KPinto SStoffel DKunz WDe V(2024)MCU-Wide Timing Side Channels and Their DetectionProceedings of the 61st ACM/IEEE Design Automation Conference10.1145/3649329.3656541(1-6)Online publication date: 23-Jun-2024
https://dl.acm.org/doi/10.1145/3649329.3656541
Deutschmann LMüller JFadiheh MStoffel DKunz W(2024)A Scalable Formal Verification Methodology for Data-Oblivious HardwareIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2024.337424943:9(2551-2564)Online publication date: Sep-2024
https://doi.org/10.1109/TCAD.2024.3374249
Dinesh SParthasarathy MFletcher C(2024)ConjunCT: Learning Inductive Invariants to Prove Unbounded Instruction Safety Against Microarchitectural Timing Attacks2024 IEEE Symposium on Security and Privacy (SP)10.1109/SP54263.2024.00180(3735-3753)Online publication date: 19-May-2024
https://doi.org/10.1109/SP54263.2024.00180
Show More Cited By

Recommendations

Formally verified superblock scheduling
CPP 2022: Proceedings of the 11th ACM SIGPLAN International Conference on Certified Programs and Proofs

On in-order processors, without dynamic instruction scheduling, program running times may be significantly reduced by compile-time instruction scheduling. We present here the first effective certified instruction scheduler that operates over superblocks ...
Code optimizations using formally verified properties
OOPSLA '13: Proceedings of the 2013 ACM SIGPLAN international conference on Object oriented programming systems languages & applications

Formal program verification offers strong assurance of correctness, backed by the strength of mathematical proof. Constructing these proofs requires humans to identify program invariants, and show that they are always maintained. These invariants are ...
A formal model for proving hardware timing properties and identifying timing channels
Abstract
Timing channels are becoming a critical threat to hardware security. When exploited, secret information can be revealed by analyzing the execution time statistically. There are a variety of methods for detecting timing channels such as ...
Highlights
- Developing an IFT model with time label to detect hardware timing channels.
- ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

DAC '22: Proceedings of the 59th ACM/IEEE Design Automation Conference

July 2022

1462 pages

ISBN:9781450391429

DOI:10.1145/3489517

General Chair:
Rob Oshana
NXP

Copyright © 2022 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGDA: ACM Special Interest Group on Design Automation
IEEE CEDA

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 August 2022

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Best Paper

Author Tags

Qualifiers

Research-article

Funding Sources

Scalable Assurance (Intel)
DFG SPP NanoSecurity
BMBF ZuSE (Scale4Edge)

Conference

DAC '22

Sponsor:

SIGDA

DAC '22: 59th ACM/IEEE Design Automation Conference

July 10 - 14, 2022

California, San Francisco

Acceptance Rates

Overall Acceptance Rate 1,770 of 5,499 submissions, 32%

Upcoming Conference

DAC '25

Sponsor:
sigda

62nd ACM/IEEE Design Automation Conference

June 22 - 26, 2025

San Francisco , CA , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
641
Total Downloads

Downloads (Last 12 months)179
Downloads (Last 6 weeks)14

Reflects downloads up to 04 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Müller JDuque Antón ADeutschmann LMehmedagić DRodrigues COliveira DRahmani Fadiheh MDevarajegowda KPinto SStoffel DKunz WDe V(2024)MCU-Wide Timing Side Channels and Their DetectionProceedings of the 61st ACM/IEEE Design Automation Conference10.1145/3649329.3656541(1-6)Online publication date: 23-Jun-2024
https://dl.acm.org/doi/10.1145/3649329.3656541
Deutschmann LMüller JFadiheh MStoffel DKunz W(2024)A Scalable Formal Verification Methodology for Data-Oblivious HardwareIEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems10.1109/TCAD.2024.337424943:9(2551-2564)Online publication date: Sep-2024
https://doi.org/10.1109/TCAD.2024.3374249
Dinesh SParthasarathy MFletcher C(2024)ConjunCT: Learning Inductive Invariants to Prove Unbounded Instruction Safety Against Microarchitectural Timing Attacks2024 IEEE Symposium on Security and Privacy (SP)10.1109/SP54263.2024.00180(3735-3753)Online publication date: 19-May-2024
https://doi.org/10.1109/SP54263.2024.00180
Hsiao YNikoleris NKhyzha AMulligan DPetri GFletcher CTrippel C(2024)RTL2MμPATH: Multi-μPATH Synthesis with Applications to Hardware Security Verification2024 57th IEEE/ACM International Symposium on Microarchitecture (MICRO)10.1109/MICRO61859.2024.00045(507-524)Online publication date: 2-Nov-2024
https://doi.org/10.1109/MICRO61859.2024.00045
Deutschmann LKazhalawi YSeckinger JAntón AMüller JFadiheh MStoffel DKunz W(2024)Data-Oblivious and Performant: On Designing Security-Conscious Hardware2024 IEEE 25th Latin American Test Symposium (LATS)10.1109/LATS62223.2024.10534597(1-6)Online publication date: 9-Apr-2024
https://doi.org/10.1109/LATS62223.2024.10534597
Mehmedagić DFadiheh MMüller JAntón AStoffel DKunz WCalandrino JTroncoso C(2023)Design of access control mechanisms in systems-on-chip with formal integrity guaranteesProceedings of the 32nd USENIX Conference on Security Symposium10.5555/3620237.3620393(2779-2796)Online publication date: 9-Aug-2023
https://dl.acm.org/doi/10.5555/3620237.3620393
Jauch TWezel AFadiheh MSchmitz PRay SFung JFletcher CStoffel DKunz W(2023)Secure-by-Construction Design Methodology for CPUs: Implementing Secure Speculation on the RTL2023 IEEE/ACM International Conference on Computer Aided Design (ICCAD)10.1109/ICCAD57390.2023.10323843(1-9)Online publication date: 28-Oct-2023
https://doi.org/10.1109/ICCAD57390.2023.10323843

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents