BP类攻击建模

Branch Prediction Attack

Define

BP 类攻击 指的是利用CPU 分支预测机制及其副作用 来泄露敏感信息或在隔离边界上建立侧信道的攻击。它属于一种微架构侧信道（microarchitectural side-channel），常见的代表是Spectre 系列攻击。这些攻击不是针对软件算法错误，而是针对处理器预测逻辑和投机执行（speculative execution）的硬件行为。

核心思想：

  • 现代 CPU 为提高性能，会对条件分支/间接跳转做预测，并投机执行路径。
  • 如果预测错误，CPU 会回滚架构状态，但 微架构状态（如缓存）可能已被改变。
  • 攻击者能通过对这些副作用的测量（例如缓存命中时间）来推断敏感数据。

Threat Model

攻击目标

目标类型 例子
机密数据泄露 进程内密钥、用户密码、其他内存内容
跨进程/跨 VM 数据泄露 虚拟化场景下的邻居 VM 隐私泄露
沙盒环境绕过 浏览器 JavaScript 利用 Spectre 读取内核/其他进程数据

攻击者能力假设

BP 类攻击通常假设攻击者可以：

  • 在同一处理器核心或共享预测器资源上执行代码；
  • 构造特定模式的分支历史输入；
  • 测量系统行为变化（如 cache timing）；
  • 在某些场景下无需内核权限（pure JavaScript 也可利用）。

这种能力模型类似于一种“白盒微架构侧信道访问”，不需要直接访问内存内容本身。

抽象模型

BP 攻击可以抽象为以下四个阶段：

① 污染/训练分支预测器（Branch Predictor Training）

攻击代码通过精心构造的分支序列来“训练”分支预测器，使其偏向某一分支方向。

→ 目的是在真实 victim 代码执行期间造成错误预测。

② 触发投机执行（Speculative Execution）

当 victim 代码遇到分支时，由于预测器的状态“被污染”，CPU 会错误预测路径并投机执行错误路径。

投机路径可能会读取敏感数据（本来不会发生的读取）。

③ 留下微架构泄露（Microarchitectural Side Effects）

错误路径的执行影响 CPU 微架构状态，如加载缓存某些行，改变分支历史缓冲器等。

这些状态并不被体系结构回滚机制撤销，因此可以被外部可测量。

④ 侧信道测量与推断（Side-Channel Observation）

攻击者测量缓存访问时间、分支预测历史等，从这些统计量恢复敏感数据。例如，时间差异表明某个缓存行被 victim 访问过，从而反推 secret value。

常见BP攻击

攻击类型 攻击原理 关键副作用
Spectre V2 间接分支预测污染 (Branch Target Injection) 错误返回目标 执行
分支历史注入（BHI） 利用分支历史表（BHB）污染预测 注入错误历史，引导误预测
BiasScope / Spectre-BHS 利用不准确的分支历史 二级侧信道泄露更高带宽信息

BP攻击系统模型

建模目标

零泄露：

或 可控泄露上界:

或 不可达性：

在防御机制下，投机路径永远无法访问 secret-dependent memory

数学模型

1.系统状态定义（Minimal State）

我们定义系统在任意时刻的状态为：

其中：

  • A：架构可见状态（寄存器、PC）
  • B：分支预测器状态
  • M：缓存状态（或更一般的 microarchitectural state）

2.程序模型（Victim + Attacker）

Victim 程序抽象为：

  • x：攻击者可控输入
  • 𝜙(𝑥)：边界检查
  • ：包含对 secret s 的访问（在架构语义下不可达）

投机执行的形式化定义

定义一个投机转移关系：

即：

  • 预测器状态 决定下一条路径
  • 即使 ，仍可能执行 ​

泄露唯一来源

我们定义：

  • 唯一可被攻击者观测的量是：

攻击者不能直接观测 或 ，只能观测泄露状态 (例如 cache timing)

攻击成功的定义

攻击成功 ⇔

也即：

攻击证明

在无防御时：

1.存在 使得：

​

2.中存在：

3.因此：

⇒

防御策略的形式化建模

防御策略 D：投机不可达性（Speculative Non-Interference, SNI）

防御定义（形式化）

防御 D 保证：

任意投机执行路径中，不允许 secret-dependent memory access

形式化为：

或更直观地：

防御有效性证明

定理（SNI ⇒ 零泄露）

若系统满足 Speculative Non-Interference，则：

证明：

1.攻击者的观测量：

2.根据防御假设：

3.因此：

4.由于 是 的确定性或随机函数：

5.得证：

推广

如果 ，可以建模：有概率 访问 secret，有噪声

可以推导：

应用举例

BiasScope / Spectre-BHS

根据论文攻击流程（例如 BiasScope）：

  • 攻击者训练或置入某个分支状态 (Bias-Free BHB 条目)
  • Victim 执行某个 secret-dependent 分支
  • 攻击者验证 BHB 是否被更新（或被驱逐）
  • 从 BHB 记录状态的变化间接推断 secret 值（例如分支是否 taken）

这说明：

  • 投机历史 会依赖 （victim secret branch 状态会修改 BHB）

  • 这种修改又会被攻击者通过后续分支行为产生的微结构影响 （比如缓存时间差）

因此模型中的攻击链路存在：

即：

1.Victim secret 影响 BHB 状态

2.攻击者通过自身的推测执行利用 BHB 干扰预测路径

3.推测执行泄露副作用到缓存／时序

4.攻击者测量观察到不同的 ，从而间接泄露

为了证明攻击有效，需要证明：

说明：

不同 secret 对 BHB 更新有不同概率或不同最终状态

该差异通过 被攻击者测量捕获（cache 时序）

例如在 BiasScope 中：

Victim 分支 taken 会 evict／update 特定 BHB 条目

攻击者随后执行自己的分支序列
→ 会因 BHB 差异导致预测行为不同
→ 侧信道可测量（如 mis-prediction 计数、cache 影响等）

因此可以构造：

从而：

防御目标

防御策略目标是打断这个链条的一环使得：防御 不成立或可控。

IBT

IBT 的硬件语义可以抽象为以下不变式：

任意间接跳转 / 间接调用的投机目标，必须是合法 ENDBR 入口

形式化定义：

令：

  • ：预测器给出的目标
  • ：所有以 ENDBR 开头的地址集合

IBT 强制：

否则：

speculative execution aborts

防御目标

IBT 不改变预测器 𝐵，但约束预测器对架构状态 𝐴 的影响函数：

被限制

变为：

IBT 阻断 BTB-based Spectre-V2

证明：

1.攻击成立的必要条件是存在 gadget 𝐺，使得：

2.IBT强制：

3.若，则：

4.因此不存在：

5.即：

IBT 的“证明边界”

IBT 仅证明：

  • 阻断 BTB-target injection
  • 阻断 Spectre-V2 gadget 跳转

但 不能证明：

  • Branch History Side-Channel
  • 条件分支投机（Spectre-V1）

因为：

仍可能成立（IBT 不隔离 B）
Microarchitecture Security > Branch Prediction
#Branch Prediction #Attack Modeling #Side-channel Attack #Microarchitecture Security #Formal Verification
BP类攻击建模
http://ruak.github.io/2026/01/20/BP类攻击建模/
作者
HUANGDAN
发布于
2026年1月20日
许可协议