认证鲁棒性遭遇浮点攻击：舍入误差可使认证半径的保证失效

1. 01这篇论文试图解决什么问题？

   作者称浮点舍入误差可使认证半径被高估，从而在认证半径内找到对抗样本，使认证失效。

   核心问题：认证鲁棒性的实现基于浮点运算，舍入误差可能使计算出的认证半径 R̃ 高估真实半径 R，导致认证保证在实践中失效。

   • 场景与重要性：认证机制承诺输入 x 的 ℓ2 半径 R 内预测不变，作者称这类机制若用于安全关键场景，其实现层面的失效会带来风险；目前认证机制的证明大多（隐式）假设实数可被精确表示，而计算机上浮点数只能表示实数的子集。
   • 现有方法不足：作者称 PGD、C&W 等传统对抗样本搜索方法不能有效利用认证半径的舍入——搜索空间太大（浮点取值数量庞大），且不当舍入不一定沿模型梯度出现；已有发现鲁棒性违反的工作 [17, 30] 针对的是特殊构造的模型或实例。
   • 核心观察：认证计算中的舍入可累积，误差幅度可从 10⁻¹³ 到 10³（Figure 2b），即使很小的误差也可被系统性利用；范数计算本身也可能被低估。
   • 论文提出：rounding search 攻击方法（在弱、强两种威胁模型下）、对线性模型精确认证和神经网络保守/近似认证的攻击实验，以及基于 rounded interval arithmetic 的防御。
   • 威胁模型：
     • 目标：在计算认证半径 R̃ 内找到使分类器翻转的对抗样本，使认证的 soundness 失效。
     • 知识：对分类器 f 和认证机制均有 white-box 访问，可用 f 和 x 查询认证机制得到 R̃。
     • 能力（弱模型）：攻击成功只需扰动的浮点范数 ∥δ∥ ≤ R̃，对应范数用常见软件库（如 Numpy 32/64 位浮点）计算的场景。
     • 能力（强模型）：要求扰动真实（实数值）范数违反认证；作者用 rounded interval arithmetic 计算的范数上界 ∥δ∥ 代替真实范数，成功条件为 ∥δ∥ ≤ R̃。

   收起这一问

2. 02有哪些相关研究？

   相关工作包括认证机制、对抗样本搜索、浮点对验证的影响，以及两篇独立并行工作。

   认证鲁棒性机制

   • Cohen et al. [5]——随机平滑近似认证，并给出二分类线性分类器的精确认证半径 R = |wᵀx + b|/∥w∥，在实数运算下证明其 sound 和 complete；本文攻击其线性认证并以其随机平滑为攻击对象。
   • Wang et al. [28]（β-CROWN）、Zhang et al. [29]——bound propagation 保守认证；Bunel et al. [3]、Ehlers [7]、Tjeng et al. [26]——线性规划/混合整数规划认证。本文用 β-CROWN 和 Gurobi MIP solver 作为这两类的实例进行攻击。

   对抗样本搜索

   • Carlini and Wagner (C&W) [4]、Madry et al. (PGD) [21]——白盒对抗样本搜索方法。作者称这些方法搜索空间大、不能有效利用认证半径的舍入，本文方法不用反向传播而利用 ReLU 网络分段线性性质，并在浮点邻域做细粒度搜索。

   浮点表示与神经网络验证

   • Giacobbe et al. [8]、Henzinger et al. [11]、Jia and Rinard [16]——针对浮点表示设计的验证器被指出不一定适用于量化神经网络；Jia and Rinard [16] 对二值化神经网络（BNN）做精确认证，不涉及浮点运算，作者称因此不受浮点误差影响。
   • Singh et al. [22, 23]——在神经网络认证中使用 interval arithmetic，作者指出其用 ℓinf 度量，规避了扰动范数计算中的舍入影响；本文用 ℓ2 度量并在强威胁模型中处理范数计算的舍入。

   最接近的并行工作

   • Jia and Rinard [17]——独立工作，同样利用舍入误差发现认证违反。作者指出区别：本文对未修改的测试集图像 x 在其认证半径内找到对抗样本，而 [17] 攻击的是合成输入 x0（由自然图像调亮度得到）的扰动版本，攻击点在 x 的认证半径之外；作者称本文攻击更强。
   • Voráček and Hein [27]——并行独立工作，利用浮点有限表示攻击随机平滑。作者指出其同样攻击合成数据和模型，而本文攻击未扰动的网络和测试集图像，并提出基于 interval arithmetic 的防御。

   基线与基准：攻击对象为线性模型精确认证 [5]、β-CROWN [28]、Gurobi MIP solver [10]、随机平滑 [5]；数据集为 MNIST [18]。作者称理论上这些认证下攻击成功率基线应为 0%。

   作者将本文定位为：对未修改的目标模型和未改动的实例、在 ℓ2 度量下系统利用浮点舍入使认证失效，并给出有 soundness 保证的防御。

   收起这一问

3. 03论文如何解决这个问题？

   rounding search：分段线性近似定方向、ReluPGD 逼近边界、浮点邻域细搜；防御用 rounded interval arithmetic。

   整体思路：认证计算中的舍入使计算半径 R̃ 可能大于真实半径 R，攻击在这个差值空间内搜索对抗样本。rounding search 分两步：先用 ReLU 网络的分段线性性质求出指向决策边界的最短扰动方向，再在半径边界附近采样浮点邻域扰动逐一检验。

   问题设定与成功判定

   • 认证机制对输入 x 输出计算半径 R̃；攻击者找 x′ = x + δ 使 f(x′) ≠ f(x) 且范数条件成立。
   • 弱威胁模型：浮点范数 ∥δ∥ ≤ R̃ 即成功；强威胁模型：interval arithmetic 范数上界 ∥δ∥ ≤ R̃ 才成功。
   • 线性分类器精确半径 R = |w^T x + b|/|w|，作者用 Numpy 32/64 位浮点自行计算 R̃。

   扰动方向：线性近似与 ReluPGD

   • 线性模型的扰动方向为决策边界法向量 ν = w；ReLU 网络分段线性，在 x 处的局部线性近似是精确的。
   • Algorithm 1（LinApproxPerturbDir）：对未激活的 ReLU 将对应权重置零，得到局部线性化权重，方向取目标类与当前类权重之差 ν = τ[t] − τ[l]。
   • Algorithm 2（ReluPGD）：迭代更新 x′——每步重新计算线性化方向、按步长 s 缩放、clip 到输入域 [Vmin, Vmax]，直到预测翻转或超时；实验中 s 初始取 10⁻⁵。作者称这是 PGD 的精确实例化，新颖性在步长设置和浮点局部搜索。

   浮点邻域搜索

   • 给定方向 ν 和 R̃，种子扰动 δ = R̃ν/|ν|（Equation 1）。
   • Algorithm 3（Neighbor）：对 δ 的每一维，用 beforeFP/afterFP 取相邻浮点值（每维 2p+1 个候选，实验设 p = 2），组合采样 N 个不重复邻居 δ′。
   • 对每个 δ′ 检验 x + δ′ 是否翻转预测且满足对应威胁模型的范数条件；作者称这可找到范数仅在小数第 13 位小于 R̃ 的对抗样本，PGD 和 C&W 找不到这类样本。

   防御：rounded interval arithmetic

   • 思路：把每个浮点标量替换为包含其真实值的浮点区间，运算按 Definition 2 的区间算子进行，端点用 IEEE754 向下/向上舍入（Lemma 1 给出 soundness）。
   • Theorem 1：若认证机制 R(f, x) 在实数运算下 sound 且可由具有 sound 浮点扩展的算子复合而成，则用区间扩展计算并返回区间下界 R 的认证在强威胁模型下 sound。
   • 作者指出固定修正 R̃ − γ（如 γ = 1.0）一般不 sound：高估量依赖数据和模型，对 R̃ − 1.0 仍可构造攻击；该防御可视为输入依赖的修正。
   • 实现用 PyInterval 库 [25]，在线性分类器上演示。

   收起这一问

4. 04论文做了哪些实验？

   在随机线性分类器、MNIST linear SVM、β-CROWN/MIP/随机平滑认证的 ReLU 网络上评测攻击成功率。

   实验设置

   • 被测模型：随机初始化的二分类线性分类器（权重、偏置取自 [−1,1]，32/64 位浮点）；MNIST 上训练的 45 个 linear SVM（ℓ1 正则，验证准确率 91%–99%）；3 层 ReLU 网络三种：1 隐节点正权重二分类器（验证准确率 99.67%）、100 隐节点正权重多分类器（84.14%）、100 隐节点无约束多分类器（96.73%）；随机平滑实验用 100 隐节点 ReLU 网络（验证准确率 99.95%）。
   • 数据集：MNIST；linear SVM 用约 12 000 张训练、约 2 000 张验证和评测（每个标签对组合）。
   • 认证机制：线性模型精确认证（Numpy 32/64 位自算）；β-CROWN（ℓ2）；Gurobi MIP solver（feasibility tolerance 2×10⁻⁵）；随机平滑（α = 0.1%，σP ∈ {1.0, 3.0, 5.0, 7.0}，Monte Carlo 样本 M ∈ {100, 1000, 10000}）。
   • 指标：攻击成功率——成功找到认证半径内对抗样本的样本/模型比例；作者称各认证机制的理论基线均为 0%。
   • 攻击参数：随机线性分类器每维 10 000 个模型、每模型 N = D² 个邻居；linear SVM 每张测试图 N = 5 000 邻居；随机平滑 N = 1000 邻居；ReluPGD 步长 s = 1×10⁻⁵，超时 15 分钟。
   • 硬件：线性模型在 Intel Xeon Platinum 8180M CPU，神经网络在 Tesla V100 16GB GPU；未报告重复次数。

   主结果

   表格较宽，可左右滑动

   目标	认证机制	威胁模型	攻击成功率	出处
   随机线性分类器	精确认证	弱	约 50%（高维处趋平）	Figure 2a
   随机线性分类器	精确认证	强	约 5%（高维处）	Figure 2a
   linear SVM (MNIST)	精确认证	弱	最高 23.24%，44/45 模型非零	Table 1a
   linear SVM (MNIST)	精确认证	强	最高 0.16%，11/45 模型非零	Table 1b
   3 层 ReLU（1 隐节点，正权重）	β-CROWN	弱	2.6%（53/2078）	正文 4.3
   3 层 ReLU（100 隐节点，正权重）	MIP	弱	60.76%（5108/8406）	正文 4.3
   3 层 ReLU（100 隐节点，无约束）	MIP	弱	15.83%（1531/9671）	正文 4.3
   3 层 ReLU（100 隐节点）	随机平滑	弱	最高 21.11%（σP=7.0, M=100）	Table 2

   • 作者称：维度升高使 ∥δ′∥ 和 R̃ 的计算累积更多舍入误差，攻击成功率随之上升；Figure 2b 显示半径计算的最大舍入误差可累积到 10³ 量级。
   • 强威胁模型成功率低于弱模型，作者解释为强模型用 interval arithmetic 范数上界，可利用空间（R̃ − ∥δ∥）更小。
   • 神经网络实验只在弱威胁模型下进行。

   随机平滑认证的详细结果

   • 测了什么：不同 σP 和 M 组合下的攻击成功率（Table 2，2 115 张 MNIST 0/1 图像）。
   • 结果：σP=1.0 时 0.24%/0.05%/0.05%（M=100/1000/10000）；σP=7.0 时 21.11%/12.24%/4.79%。同一 σP 下 M 越大成功率越低；同一 M 下 σP 越大成功率越高。
   • 作者解读：论文未对这些趋势给出解释。

   成功率趋平现象分析（Section 6.1）

   • 测了什么：弱威胁模型、64 位浮点下，用 PyInterval 计算半径上下界并二分搜索最大无违反半径 R̂，统计 R̃ 被高估（R̂ < R̃）的比例（Figure 4）。
   • 结果：Figure 4a 显示攻击利用的舍入误差量级为 10⁻¹⁵；Figure 4b 显示高估率趋平在约 50%，与攻击成功率趋平一致。
   • 作者解读：作者认为一种直觉是舍入近似随机——R̃ 被高估（向上舍入）和低估（向下舍入）各占约 50%，故成功率在 32/64 位下都趋平于 50% 左右。

   防御评测

   • 测了什么：Theorem 1 的区间认证在线性分类器上的效果，64 位浮点、PyInterval 实现。
   • 结果：随机线性分类器（Section 4.1 设置）的攻击成功率在弱、强两种威胁模型的所有维度下都降为 0%。
   • 作者解读：作者称理论和实证结果支持该防御可缓解对精确认证的攻击；弱威胁模型下范数计算的舍入理论上仍可能影响 R 的 soundness，但实践中应能缓解大多数攻击。

   其他消融与分析

   • 强威胁模型下成功率随维度先升后降（Figure 2a 虚线）：作者解释为维度升高使 interval arithmetic 输出的范数区间变宽、上界变大，可利用空间先增后减。
   • β-CROWN 实验：ReluPGD 在 2 108 张图中 30 张超时；单次攻击约 30 秒、单次验证约 1 秒。
   • MIP 实验：ReluPGD 对两个分类器分别超时 8 张和 2 张；单次验证约 10 秒。
   • Figure 3 给出弱模型下原始与对抗图像示例：第一张图 R̃ = 333.6087764918925，对抗扰动 ∥δ∥ = 333.6087764918924，预测从 1 翻为 0。

   收起这一问

5. 05有什么可以进一步探索的点？

   作者列出三条局限：随机平滑攻击与 soundness 概率的关系、防御的泛化、更大模型和数据集。

   作者指出的局限与后续方向

   • 随机平滑攻击的概率性质（Section 6.2）：对随机平滑方法的攻击未研究攻击成功率与这些方法 soundness 概率之间的关系，作者称未来可研究二者如何相互作用。
   • 防御的适用范围（Section 6.2）：防御只在线性模型和精确认证上演示，将其嵌入其他验证器和模型的详细探索留作未来工作。
   • 评测规模（Section 6.2）：评测在相对小的模型（如 linear SVM）和数据集（如 MNIST）上进行，在 state-of-the-art 模型和数据集上的进一步评测留作未来工作。
   • 部署影响（Section 6.2）：作者称目前不知道有任何认证鲁棒性实现已部署，攻击可能用于发现系统实现中的鲁棒性保证违反。

   实验覆盖范围

   • 被测模型为随机线性分类器、MNIST linear SVM、3 个 3 层 ReLU 网络（隐层 1 或 100 节点），共 6 类目标；神经网络均为 MNIST 上训练的小模型。
   • 认证机制覆盖精确认证（线性模型）、保守认证（β-CROWN、Gurobi MIP）和近似认证（随机平滑）三类；神经网络攻击只在弱威胁模型下进行。
   • 数据集只有 MNIST（0/1 标签对用于 β-CROWN 和随机平滑实验，linear SVM 用全部 45 个标签对）。
   • 防御实验只在线性分类器、64 位浮点、PyInterval 实现下进行。
   • 论文未报告实验重复次数；随机平滑实验的样本量为 2 115 张图像，linear SVM 每模型约 2 000 张评测图。

   收起这一问

6. 06总结一下论文的主要内容

   作者称浮点舍入可使认证半径被高估，rounding search 能系统利用这一点，interval arithmetic 可防御。

   一篇关于认证鲁棒性实现层安全的攻击论文：认证机制在实数假设下证明半径内无对抗样本，但浮点实现的舍入误差可使计算半径 R̃ 高估真实半径 R。

   • 问题：认证计算和范数计算中的舍入误差可累积（Figure 2b 中可达 10³ 量级），认证半径内可能实际存在对抗样本；作者称 PGD、C&W 无法有效利用这种误差。
   • 方法：rounding search——利用 ReLU 网络分段线性性质求局部线性近似方向（ReluPGD，步长 10⁻⁵），再在半径边界采样浮点邻域扰动（Neighbor，p = 2）；分弱威胁模型（浮点范数 ≤ R̃）和强威胁模型（范数区间上界 ≤ R̃）。
   • 结果（弱模型）：随机线性分类器成功率约 50%（Figure 2a）；MNIST linear SVM 最高 23.24%（Table 1a）；MIP 认证网络 60.76%（正权重）和 15.83%（无约束）；β-CROWN 认证网络 2.6%；随机平滑最高 21.11%（σP=7.0、M=100，Table 2）。
   • 结果（强模型）：成功率更低但非零——随机线性分类器约 5%，linear SVM 最高 0.16%（Table 1b）；作者称理论上这些认证下基线应为 0%。
   • 防御：基于 rounded interval arithmetic 的认证（Theorem 1 给出强威胁模型下的 soundness），在线性分类器上使两种威胁模型的攻击成功率降为 0%；作者指出固定修正 R̃ − γ 一般不 sound。
   • 作者结论：若认证鲁棒性用于安全关键应用，其保证和实现需要考虑现代计算架构的限制；局限包括评测限于小模型和 MNIST、防御仅在线性模型演示。

   收起这一问

相关论文