该论文首次提出了一种针对现代超标量CPU中调度队列（Scheduler Queue）的侧信道攻击——SQUIP攻击。调度队列负责决定指令按何种顺序分配到各个执行单元，以往未被作为侧信道研究，因为Intel CPU仅有一个调度队列，其竞争现象与重排序缓冲区的竞争几乎相同。然而，Apple M1、AMD Zen 2和Zen 3微架构为每个执行单元配备了独立的调度队列，使得攻击者可以通过探测特定调度队列的占用水平来泄露信息。研究者首先逆向工程了这些CPU上调度队列的行为，证明了可以被初始化和探测。SQUIP攻击能够从同一硬件核心内部以及跨SMT线程观察占用水平。在隐蔽信道测试中，攻击在虚拟机之间实现了0.89 Mbit/s的泄露速率（错误率低于0.8%），在进程之间实现了2.70 Mbit/s（错误率低于0.8%）。进一步，在协同定位进程和虚拟机上针对mbedTLS RSA签名过程发起侧信道攻击，仅用50,500次迹（traces）平均即可恢复完整的RSA-4096密钥，平均错误比特数少于5至18比特。论文讨论了必要的缓解措施，尤其是针对Zen 2和Zen 3系统。该攻击揭示了调度队列这一新的侧信道泄露源，对机密计算和云环境中的密钥保护构成威胁。安全研究人员和CPU微架构设计者应重点关注。

本文对 Go 标准库 `crypto/internal/fips140/bigmod` 中的 `extendedGCD` 实现进行了形式化验证。该实现用于 RSA 密钥对生成中的扩展欧几里得算法，是从 BoringSSL 移植而来。然而，研究者发现了两处偏差：一是系数更新方式与原始实现不同，二是允许更大的输入域。第一个偏差导致算法不变量被破坏，第二个偏差使得原有证明不再适用。研究者修复了第一个偏差（性能提升平均 24%），并针对第二个偏差将 BoringSSL 的证明移植并扩展到更大的输入域。他们使用 Go 语言专用验证器 Gobra 证明了修复后实现的正确性和终止性，并借助 Lean 验证了一些非线性算术引理。验证过程表明，即使是经过充分审查的代码也可能存在细微错误，形式化验证是发现此类错误的有效工具，而 AI 代理可通过迭代优化不变量和引理来辅助验证。