Though modern microprocessors embed several hardware security mechanisms, aimed at guaranteeing confidentiality and integrity of sensible data, recently disclosed attacks such as Spectre and Meltdown witness weaknesses with potentially great impact on CPU security. Both vulnerabilities exploit speculative execution of modern high-performance micro-architectures, allowing the attacker to observe data leaked via a memory side channel, during speculated and mispredicted instructions. In this paper we present a methodology to formally verify, by means of a model checker, speculative vulnerabilities, such as the class of Spectre/Meltdown attacks, in microprocessors based on speculative execution. In detail, we discuss the problem of formally verifying confidentiality violations, since we deem it will help preventing new vulnerabilities of the same typology. We describe our methodology on a pipelined CPU inspired by the DLX RISC processor architecture. Due to scalability issues, and following related approaches in formal verification of correctness, our approach simplifies the model under verification by proper abstraction and reduction steps. The approach is based on flushing the pipeline, abstracting data and most of the speculative execution logic, keeping a subset of control data, plus speculated data state and tainting logic. Illegal propagation (data leakage) is encoded in terms of taint propagation, from a protected/invalid memory address to the address bus on a subsequent memory read, affecting the cache. We introduce the theoretical flow, relying on known theoretical results combined and exploited to prove soundness and completeness. Finally, using a state-of-the-art model checking tool, we present preliminary data on formal verification based on Bounded Model Checking, that to support our claims and highlight the feasibility of the approach.

Model Checking Speculation-Dependent Security Properties: Abstracting and Reducing Processor Models for Sound and Complete Verification / Cabodi, Gianpiero; Camurati, Paolo; Finocchiaro, Fabrizio; Vendraminetto, Danilo. - STAMPA. - 11445:(2019), pp. 462-479. (Intervento presentato al convegno Codes, Cryptology and Information Security tenutosi a Rabat, Morocco nel April 22-24, 2019) [10.1007/978-3-030-16458-4_27].

Model Checking Speculation-Dependent Security Properties: Abstracting and Reducing Processor Models for Sound and Complete Verification

Cabodi, Gianpiero;Camurati, Paolo;Finocchiaro, Fabrizio;Vendraminetto, Danilo
2019

Abstract

Though modern microprocessors embed several hardware security mechanisms, aimed at guaranteeing confidentiality and integrity of sensible data, recently disclosed attacks such as Spectre and Meltdown witness weaknesses with potentially great impact on CPU security. Both vulnerabilities exploit speculative execution of modern high-performance micro-architectures, allowing the attacker to observe data leaked via a memory side channel, during speculated and mispredicted instructions. In this paper we present a methodology to formally verify, by means of a model checker, speculative vulnerabilities, such as the class of Spectre/Meltdown attacks, in microprocessors based on speculative execution. In detail, we discuss the problem of formally verifying confidentiality violations, since we deem it will help preventing new vulnerabilities of the same typology. We describe our methodology on a pipelined CPU inspired by the DLX RISC processor architecture. Due to scalability issues, and following related approaches in formal verification of correctness, our approach simplifies the model under verification by proper abstraction and reduction steps. The approach is based on flushing the pipeline, abstracting data and most of the speculative execution logic, keeping a subset of control data, plus speculated data state and tainting logic. Illegal propagation (data leakage) is encoded in terms of taint propagation, from a protected/invalid memory address to the address bus on a subsequent memory read, affecting the cache. We introduce the theoretical flow, relying on known theoretical results combined and exploited to prove soundness and completeness. Finally, using a state-of-the-art model checking tool, we present preliminary data on formal verification based on Bounded Model Checking, that to support our claims and highlight the feasibility of the approach.
2019
978-3-030-16457-7
978-3-030-16458-4
File in questo prodotto:
File Dimensione Formato  
c2si19.pdf

non disponibili

Tipologia: 1. Preprint / submitted version [pre- review]
Licenza: Non Pubblico - Accesso privato/ristretto
Dimensione 268.13 kB
Formato Adobe PDF
268.13 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
978-3-030-16458-4_27.pdf

non disponibili

Tipologia: 2a Post-print versione editoriale / Version of Record
Licenza: Non Pubblico - Accesso privato/ristretto
Dimensione 469.8 kB
Formato Adobe PDF
469.8 kB Adobe PDF   Visualizza/Apri   Richiedi una copia
Pubblicazioni consigliate

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11583/2731612
 Attenzione

Attenzione! I dati visualizzati non sono stati sottoposti a validazione da parte dell'ateneo