Spectre attack 在2018 年由Google Project Zero 團隊所發現，大多數支援亂序執行(out-of-order execution) 及分支預測(branch prediction) 的處理器皆會受其影響，包含常見於個人電腦的x86 架構處理器、手機晶片所採用的ARM 架構處理器，以及本篇所探討的RISC-V 架構處理器。Spectre 是一個基於快取的旁路攻擊(cache-based side-channel attack)，在攻擊過程中Spectre 會利用推測執行(speculative execution) 來執行惡意程式，藉此更改快取的狀態來洩漏資料。我們觀察其在攻擊過程中針對CPU 硬體層面所造成的影響設計了兩條正規驗證property 來偵測此惡意行為，此外，為了讓我們所設計的property 可以應用到其他也有此安全疑慮的CPU 上做檢查，我們設計了一個驗證接口(interface) 讓CPU 與我們的驗證property 對接來進行正規驗證。
在本篇論文中，我們在兩顆開源的out-of-order RISC-V CPU，BOOM 及RSD 進行實驗，透過模擬與驗證結果證實Spectre 可以成功的竊取機密資料。另外，我們也在RSD 上實做了硬體的防禦機制來阻擋Spectre 攻擊，透過模擬的結果發現其可以有效抵擋目前已經提出的多種Spectre 攻擊，同時，使用我們所提出的驗證property 也證實Spectre 所利用的硬體漏洞已被我們所修復。

Spectre attack was discovered by Google Project Zero team in 2018. Most processors that suport out-of-order execution and speculative execution will be affected by it, including x86, ARM, and RISC-V which discussed in this paper. Spectre is a cache-based side-channel sttack, it execute malicious code snippet speculatively and leave a footprint in the cache to leak the secret data. We observed the impact of the attack at the hardware level and design two formal verification properties to detect the malicious behavior. Furthermore, in order to apply our proposed property to other CPUs that also have this security concern, we design a verification interface that allow the CPU to bind with our verification property for formal verification.
In this paper, we experiment with two open-sourced out-of-order RISC-V processors, BOOM and RSD. The simulation and verification result shows that Spectre can steal confidential data on these two processors. In addition, we implement a hardware mitigation mechanism on RSD to block Spectre attack. Through simulation results, we found that it can effectively resist most currently proposed Spectre variants. At the same time, our proposed verification property confirmed that the hardware vulnerabilities used by Spectre have been fixed by us.

Alastair Reid, Rick Chen, Anastasios Deligiannis, David Gilday, David Hoyes, Will Keen, Ashan Pathirane, Owen Shepherd, Peter Vrabel, and Ali Zaidi. End-to-end verification of processors with isa-formal. volume 9780, pages 42–58, 07 2016.

Paul Kocher, Jann Horn, Anders Fogh, Daniel Genkin, Daniel Gruss, Werner Haas, Mike Hamburg, Moritz Lipp, Stefan Mangard, Thomas Prescher, Michael Schwarz, and Yuval Yarom. Spectre attacks: Exploiting speculative execution. In 2019 IEEE Symposium on Security and Privacy (SP), pages 1–19, 2019.

Intel analysis of speculative execution side channels. www.intel.com/design/literature.htm., 2018.

Managing-speculation-on-amd-processors. https://developer.amd.com/wpcontent/resources/Managing-Speculation-on-AMD-Processors.pdf, 2018.

Microsoft. Spectre mitigations in msvc. https://devblogs.microsoft.com/cppblog/spectremitigations-in-msvc/, 2018.

Jacob Fustos, Farzad Farshchi, and Heechul Yun. Spectreguard: An efficient datacentric defense mechanism against spectre attacks. In 2019 56th ACM/IEEE Design Automation Conference (DAC), pages 1–6, 2019.

Mengjia Yan, Jiho Choi, Dimitrios Skarlatos, Adam Morrison, Christopher Fletcher, and Josep Torrellas. Invisispec: Making speculative execution invisible in the cache hierarchy. In 2018 51st Annual IEEE/ACM International Symposium on Microarchitecture (MICRO), pages 428–441, 2018.

Guanhua Wang, Sudipta Chattopadhyay, Ivan Gotovchits, Tulika Mitra, and Abhik Roychoudhury. oo7: Low-overhead defense against spectre attacks via program analysis. IEEE Transactions on Software Engineering, pages 1–1, 2019.

Yuval Yarom and Katrina Falkner. Flush+reload: A high resolution, low noise, l3 cache side-channel attack. USA, 2014. USENIX Association.

Moritz Lipp, Michael Schwarz, Daniel Gruss, Thomas Prescher, Werner Haas, Jann Horn, Stefan Mangard, Paul Kocher, Daniel Genkin, Yuval Yarom, Mike Hamburg, and Raoul Strackx. Meltdown: Reading kernel memory from user space. Commun. ACM, 63(6):46–56, 2020.

Kevin Cheang, Cameron Rasmussen, Sanjit Seshia, and Pramod Subramanyan. A formal approach to secure speculation. In 2019 IEEE 32nd Computer Security Foundations Symposium (CSF), pages 288–28815, 2019.

Yunjie Zhang and Yiorgos Makris. Hardware-based detection of spectre attacks: A machine learning approach. In 2020 Asian Hardware Oriented Security and Trust Symposium (AsianHOST), pages 1–6, 2020.

Marco Guarnieri, Boris Köpf, José F. Morales, Jan Reineke, and Andrés Sánchez. Spectector: Principled detection of speculative information flows. In 2020 IEEE Symposium on Security and Privacy (SP), pages 1–19, 2020.

Gianpiero Cabodi, Paolo Camurati, Fabrizio Finocchiaro, and Danilo Vendraminetto. Model-checking speculation-dependent security properties: Abstracting and reducing processor models for sound and complete verification. Electronics, 2019.

Mohammad Rahmani Fadiheh, Johannes Müller, Raik Brinkmann, Subhasish Mitra, Dominik Stoffel, and Wolfgang Kunz. A formal approach for detecting vulnerabilities to transient execution attacks in out-of-order processors. In 2020 57th ACM/IEEE Design Automation Conference (DAC), pages 1–6, 2020.

Microsoft. Spectre Mitigations in Microsoft’s C/C++ Compiler.
https://www.paulkocher.com/doc/MicrosoftCompilerSpectreMitigation.html.

Physical Memory Protection in RISC-V. https://github.com/riscv/riscv-isamanual/releases/download/Ratified-IMFDQC-and-Priv-v1.11/riscv-privileged-20190608.pdf.

Paul Kocher, Joshua Jaffe, and Benjamin Jun. Differential power analysis. In Annual international cryptology conference, pages 388–397. Springer, 1999.

Alireza Nazari, Nader Sehatbakhsh, Monjur Alam, Alenka Zajic, and Milos Prvulovic. Eddie: Em-based detection of deviations in program execution. In 2017 ACM/IEEE 44th Annual International Symposium on Computer Architecture (ISCA), pages 333– 346, 2017.

Michael Schwarz, Martin Schwarzl, Moritz Lipp, and Daniel Gruss. Netspectre: Read arbitrary memory over network, 2018.

Marc Andrysco, David Kohlbrenner, Keaton Mowery, Ranjit Jhala, Sorin Lerner, and Hovav Shacham. On subnormal floating point and abnormal timing. In 2015 IEEE Symposium on Security and Privacy, pages 623–639, 2015.

Abraham Gonzalez, Ben Korpan, Jerry Zhao, Ed Younis, and K Asanovic. Replicating and mitigating spectre attacks on an open source risc-v microarchitecture. In Workshop on Computer Architecture Research with RISC-V (CARRV), 2019.

Christopher Celio, David A. Patterson, and Krste Asanović. The berkeley out-of-order machine (boom): An industry-competitive, synthesizable, parameterized risc-v processor. Technical Report UCB/EECS-2015-167, EECS Department, University of California, Berkeley, Jun 2015.

Susumu Mashimo, Akifumi Fujita, Reoma Matsuo, Seiya Akaki, Akifumi Fukuda, Toru Koizumi, Junichiro Kadomoto, Hidetsugu Irie, Masahiro Goshima, Koji Inoue, and Ryota Shioya. An open source fpga-optimized out-of-order risc-v soft processor. In 2019 International Conference on Field-Programmable Technology (ICFPT), pages 63–71, 2019.

riscv-tests github repository. https://github.com/riscv/riscv-tests.

RISC-V Specifications. https://github.com/riscv/riscv-isamanual/releases/download/Ratified-IMFDQC-and-Priv-v1.11/riscv-spec-20190608.pdf.

Edmund M Clarke, William Klieber, Miloš Nováček, and Paolo Zuliani. LNCS 7682 - Model Checking and the State Explosion Problem.

Alon Amid, David Biancolin, Abraham Gonzalez, Daniel Grubb, Sagar Karandikar, Harrison Liew, Albert Magyar, Howard Mao, Albert Ou, Nathan Pemberton, Paul Rigge, Colin Schmidt, John Wright, Jerry Zhao, Yakun Sophia Shao, Krste Asanović, and Borivoje Nikolić. Chipyard: Integrated design, simulation, and implementation framework for custom socs. IEEE Micro, 40(4):10–21, 2020.

boom-attack github repository. https://github.com/riscv-boom/boom-attacks.