Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

SemPat: Using Hyperproperty-based Semantic Analysis to Generate Microarchitectural Attack Patterns

Adwait Godbole, Yatin A. Manerkar, Sanjit A. Seshia

TL;DR

SemPat presents a principled method to generate attack patterns from a non-interference hyperproperty, aiming to unify semantic security guarantees with scalable pattern-based verification. By introducing $k$-complete automatic pattern generation guided by a grammar and counterfactual specialization, it converts SH specifications into APs that cover multiple gadget variants up to skeleton size $k$. The approach is implemented in the SECANT tool and validated on Spectre-like vulnerabilities, showing new patterns (e.g., for branch speculation and computation-unit channels) and substantial performance improvements over purely hyperproperty-based checks. This work offers a practical pathway to scalable, formally grounded microarchitectural vulnerability detection with broad applicability to emerging hardware exploits.

Abstract

Microarchitectural security verification of software has seen the emergence of two broad classes of approaches. The first is based on semantic security properties (e.g., non-interference) which are verified for a given program and a specified abstract model of the hardware microarchitecture. The second is based on attack patterns, which, if found in a program execution, indicates the presence of an exploit. While the former uses a formal specification that can capture several gadget variants targeting the same vulnerability, it is limited by the scalability of verification. Patterns, while more scalable, must be currently constructed manually, as they are narrower in scope and sensitive to gadget-specific structure. This work develops a technique that, given a non-interference-based semantic security hyperproperty, automatically generates attack patterns up to a certain complexity parameter (called the skeleton size). Thus, we combine the advantages of both approaches: security can be specified by a hyperproperty that uniformly captures several gadget variants, while automatically generated patterns can be used for scalable verification. We implement our approach in a tool and demonstrate the ability to generate new patterns, (e.g., for SpectreV1, SpectreV4) and improved scalability using the generated patterns over hyperproperty-based verification.

SemPat: Using Hyperproperty-based Semantic Analysis to Generate Microarchitectural Attack Patterns

TL;DR

SemPat presents a principled method to generate attack patterns from a non-interference hyperproperty, aiming to unify semantic security guarantees with scalable pattern-based verification. By introducing -complete automatic pattern generation guided by a grammar and counterfactual specialization, it converts SH specifications into APs that cover multiple gadget variants up to skeleton size . The approach is implemented in the SECANT tool and validated on Spectre-like vulnerabilities, showing new patterns (e.g., for branch speculation and computation-unit channels) and substantial performance improvements over purely hyperproperty-based checks. This work offers a practical pathway to scalable, formally grounded microarchitectural vulnerability detection with broad applicability to emerging hardware exploits.

Abstract

Microarchitectural security verification of software has seen the emergence of two broad classes of approaches. The first is based on semantic security properties (e.g., non-interference) which are verified for a given program and a specified abstract model of the hardware microarchitecture. The second is based on attack patterns, which, if found in a program execution, indicates the presence of an exploit. While the former uses a formal specification that can capture several gadget variants targeting the same vulnerability, it is limited by the scalability of verification. Patterns, while more scalable, must be currently constructed manually, as they are narrower in scope and sensitive to gadget-specific structure. This work develops a technique that, given a non-interference-based semantic security hyperproperty, automatically generates attack patterns up to a certain complexity parameter (called the skeleton size). Thus, we combine the advantages of both approaches: security can be specified by a hyperproperty that uniformly captures several gadget variants, while automatically generated patterns can be used for scalable verification. We implement our approach in a tool and demonstrate the ability to generate new patterns, (e.g., for SpectreV1, SpectreV4) and improved scalability using the generated patterns over hyperproperty-based verification.
Paper Structure (56 sections, 2 theorems, 8 equations, 14 figures, 6 tables, 2 algorithms)

This paper contains 56 sections, 2 theorems, 8 equations, 14 figures, 6 tables, 2 algorithms.

Table of Contents

  1. Introduction
  2. Background and Motivation
  3. Microarchitectural Execution Attacks
  4. Spectre-BCB
  5. Variant Vulnerabilities
  6. Analyzing Software for Vulnerabilities
  7. $\mathrm{AP}$: Attack Pattern-based Analysis
  8. $\mathrm{SH}$: Semantic Hyperproperty-based Analysis
  9. Why convert from $\mathrm{SH}$ to $\mathrm{AP}$?
  10. System Model
  11. State
  12. Instruction semantics
  13. Modelling speculation
  14. Executions
  15. Specifications and Problem Formulation
  16. ...and 41 more sections

Key Result

Lemma 1

For $k \leq d$, if $\mathsf{inst}_1 \cdots \mathsf{inst}_k \not\models \mathsf{NI}$ where instruction $\mathsf{inst}_i = \mathsf{op}_i(\omega_i)$, then, $\mathsf{op}_1 \cdots \mathsf{op}_k \in \textbf{GenerateTemplates}{}(M, \mathsf{NI}, d)$.

Figures (14)

  • Figure 1: Left: Variants of speculative exploits targeting branch (mis)-speculation with cache-based (, ) and computation unit-based (, ) side channels. Centre: While attack patterns that can detect these exploits, variants of the same (Spectre-BCB) vulnerability - and - require different patterns, as do and . In (A, C), the load is performed within the speculative window (after the branch), while in (B, D) it is before the branch. Right: Unlike attack patterns, a semantic hyperproperty uniformly characterizes several exploits aimed a particular microarchitectural vulnerability. The Speculative Non-Interference Guarnieri2020SpectectorPD (SNI) Hyperproperty $\text{H}_{\text{AB}}$ can identify both and (as well as others) as exploits, while the SNI Hyperproperty $\text{H}_{\text{CD}}$ identifies both and . While the hyperproperty changes with the platform's microarchitectural features (e.g., speculation and side-channels), it is robust to variances in the exploit (program) structure itself.
  • Figure 2: Patterns A, B, C, D matched against executions of programs ,,,respectively.
  • Figure 3: Fragment of a platform model with state variables and and operation semantics.
  • Figure 4: A pattern for a computation-based side channel.
  • Figure 5: Buffer chain in $\textsc{PlatSynth}(k)$ with operations.
  • ...and 9 more figures

Theorems & Definitions (9)

  • Example 1
  • Example 2: $\texttt{MulOp} - \texttt{LdOp} - \texttt{MulOp}$ pattern
  • Example 3: Large skeletons: the $\textsc{PlatSynth}(k)$ platform
  • Definition 1: Skeleton
  • Example 4: Template generation for $\texttt{MulOp} - \texttt{LdOp} - \texttt{MulOp}$
  • Lemma 1
  • Example 5
  • Example 6: Multiple counterfactuals for $\textsc{PlatSynth}$
  • Theorem 1