在現今各種架構的處理器，例如：x86, ARM, RISC-V 處理器... 等等，都追求高效能且廣泛的運用在家用電腦、伺服器、智慧型手機等等。然而，處理器關於資訊安全上的疑慮也開始逐漸受到重視。在現今，大多數的處理器都有使用分支預測(branch prediction) 和推測執行(speculative execution)，藉以提高處理器的性能。Spectre 攻擊就是利用了猜測執行來執行會洩漏資料的程式片段，並利用了快取的特性將機密資料留在了快取的索引(cache index) 上，藉以獲取機密資料。本篇論文是透過模型驗證的驗證方法分辨出處理器是否會 Spectre 攻擊，而此攻擊是一種利用了分支預測、猜測執行和快取的側通道攻擊(cache-based side-channel attack)。我們致力於使用正規驗證的技術來偵測Spectre 攻擊，並且透過在硬體層級實作了緩解機制藉以證明所寫的正規模型驗證property 是可以幫我們分辨出處理器是否會被Spectre 攻擊所影響。
在本篇論文的實驗中，我們使用了兩個開源的out-of-order RISC-V CPU，分別是BOOM(Berkeley Out-of-Order Machine) 處理器、RSD (RISC-V Out-of-Order Superscalar Processor) 處理器，而這兩顆處理器在跑Spectre 的攻擊程式碼時機密資料都會被竊取成功，且跑模型驗證時也會因為違反我們針對 Spectre 攻擊所設計的property 而跑出可以成功竊取資料的反例。另一方面，我們在 RSD 處理器上做了緩解機制來阻擋 Spectre 攻擊，並且透過跑 Spectre 的攻擊程式碼來看到可以有效抵擋住 Spectre 攻擊，同時我們針對有緩解機制的RSD 處理器的狀態空間爆炸問題，做了一些 reduction 來做模型驗證。

Spectre attacks are revealed in early 2018. The attack exploits the speculative execu-tion and the side-channel such as cache to achieve leaking confidential data stored in the memory. In this work, we use RTL model checker to check if the processor is influ-enced by Spectre attack at hardware level. Moreover, we implement micro-architectural mitigation to block the Spectre attack. In the experimental results, we not only use the Spectre variant 1, variant 2, and 13 Spectre variants provided by Microsoft to compare the results between the mitigated and the non-mitigated out-of-order processor but also prove the proposed formal properties can distinguish the out-of-order processor with and without the micro-architectural mitigation.

[1] The berkeley out-of-order risc-v processor. https://github.com/riscv-boom/riscv-boom.
[2] Boom speculative attacks. https://github.com/riscv-boom/boom-attacks.
[3] Rsd risc-v out-of-order superscalar processor. https://github.com/rsd-devel/rsd.
[4] Jim Chow, Ben Pfaff, Tal Garfinkel, Kevin Christopher, and Mendel Rosenblum. Understanding data lifetime via whole system simulation. In 13th USENIX Security Symposium (USENIX Security 04), San Diego, CA, August 2004. USENIX Association.
[5] Edmund M Clarke Jr, Orna Grumberg, Daniel Kroening, Doron Peled, and Helmut Veith. Model checking. MIT press, 2018.
[6] 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.
[7] John L Hennessy and David A Patterson. Computer architecture: a quantitative approach. Elsevier, 2011.
[8] Vladimir Kiriansky, Ilia Lebedev, Saman Amarasinghe, Srinivas Devadas, and Joel Emer. Dawg: A defense against cache timing attacks in speculative execution processors. In 2018 51st Annual IEEE/ACM International Symposium on Microarchitecture (MICRO), pages 974–987, 2018.
[9] 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.
[10] Andrew Pardoe. Spectre mitigations in msvc. https://devblogs.microsoft.com/cppblog/spectre-mitigations-in-msvc/, 2018.
[11] 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. In Swarat Chaudhuri and Azadeh Farzan, editors, Computer Aided Verification, pages 42–58, Cham, 2016. Springer International Publishing.
[12] R. M. Tomasulo. An efficient algorithm for exploiting multiple arithmetic units. IBM Journal of Research and Development, 11(1):25–33, 1967.
[13] Guanhua Wang, Sudipta Chattopadhyay, Ivan Gotovchits, T. Mitra, and Abhik Roychoudhury. oo7: Low-overhead defense against spectre attacks via binary analysis. ArXiv, abs/1807.05843, 2018.
[14] 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.
[15] Yuval Yarom and Katrina Falkner. Flush+reload: A high resolution, low noise, l3 cache side-channel attack. In 23rd USENIX Security Symposium (USENIX Security 14), pages 719–732, San Diego, CA, August 2014. USENIX Association.
[16] Tse-Yu Yeh and Yale N. Patt. Alternative implementations of two-level adaptive branch prediction. In Proceedings of the 19th Annual International Symposium on Computer Architecture, ISCA ’92, page 124–134, New York, NY, USA, 1992. Association for Computing Machinery.