对量化神经网络位翻转攻击的验证

在神经网络安全快速演变的背景下，针对位翻转攻击 (即攻击者恶意翻转其参数存储存储器系统中极少数量的位数以引发有害行为) 的韧性已成为相关研究的关注焦点。既往研究表明，量化可能作为抵御此类攻击的可行方法。鉴于实值神经网络对此类攻击已知的脆弱性以及量化神经网络 (QNN) 的相对稳健性，本文引入 BFAVerifier，即第一个专为正式验证位翻转攻击是否存在或识别所有脆弱参数而设计的框架。BFAVerifier 包含两个关键组件：基于抽象的方法和基于 MILP 的方法。具体而言，我们首先基于一种具有 sound guarantee 的新型抽象域进行对符号参数进行可达性分析，这些参数代表潜在的位翻转攻击。如果可达性分析未能证明此类攻击的韧性，则我们将该验证问题编码为等价的 MILP 问题，可由现成求解器求解。因此，BFAVerifier 在 sound、complete 和相对高效方面表现良好。我们进行了广泛实验，证明其在 various network architectures、量化位宽和不同攻击者能力范围内的有效性和效率。