该论文研究 CHERI 这类基于能力(capability)的处理器架构中的一个关键安全缺口。CHERI 通过在架构层面引入不可伪造的能力指针，为软件组件提供了强隔离与内存安全保证；为了进一步抵御微架构侧信道，软件通常按常量时间(constant-time)风格编写，使执行时间与密钥等机密数据无关。然而现代处理器高度依赖推测执行，推测执行可以在时间维度上绕过架构层面的权限检查，把本应被隔离的机密瞬时(transiently)泄露出去，从而使常量时间编程所提供的机密性保证失效。作者首先论证：在 CHERI 上实现“安全推测”并不平凡，已有的一系列推测执行防护提案无法在保持能力语义的同时维持机密性保证，存在可被形式化刻画的信息泄露路径。为此，论文提出一个统一的形式化框架，能够同时推理三件事：能力安全(capability safety，即能力不可被伪造、不可被越权派生或衰减)、推测执行语义、以及基于信息流的非干扰性(non-interference)安全性质。作者利用该框架形式化地展示了现有设计在 CHERI 语义下的潜在泄露。在此基础上，论文给出新的处理器设计 SCHERI，并在同一框架内给出形式化证明：对于遵循常量时间策略的程序，SCHERI 能够提供端到端的安全推测保证，即推测执行既不会破坏常量时间假设，也不会泄露被架构隔离的机密。其核心贡献是为未来基于能力的处理器建立形式化基础并提供工程指引，使这类处理器对面向常量时间程序的 Spectre 类攻击具备韧性。

该论文是一篇系统化知识（SoK）研究，聚焦于密码学实现中的常数时间编程模式——这是抵御计时攻击的主要防御手段。然而，学术界和工业界对“常数时间”的定义并不统一，导致模型保护范围与规格假设之间长期存在脱节。论文系统梳理了常数时间模型的演变，识别出一个反复出现的缺口：模型所保护的属性并不总能覆盖规格中隐含的安全要求。作者进一步提炼出一套攻击性方法论，用于发现源自密码学原语边界之外的计时漏洞。应用该方法，他们定位到一个与私钥加载相关的规格级漏洞，并在OpenSSL和BoringSSL中实际确认了该信息泄露。反直觉的是，尽管BoringSSL采用了更严格的安全威胁模型，其每个观测的信号强度反而比OpenSSL高出多个数量级。该贡献不仅揭示了常数时间建模中的盲区，还展示了规范层面缺陷如何绕过实现层的防护。适合密码学库开发者、安全研究者和系统安全分析师阅读。

该论文研究推测执行攻击对常数时间编程（constant-time programming）安全性的破坏。常数时间编程是密码学等安全敏感软件中防止微架构侧信道攻击的标准技术，但推测执行攻击（如 Spectre）会使其失效。因此，常数时间代码还必须部署针对推测执行攻击的防御措施，以防止存储在内存或处理器寄存器中的秘密数据被泄露。然而，现有的防御手段（如推测加载硬化，Speculative Load Hardening, SLH）虽然能提供强安全保证，但性能开销非常高。针对这一问题，论文提出了一种名为 Declassiflow 的静态分析方法，用于建模非推测知识（non-speculative knowledge），从而在保证安全性的前提下放宽推测执行安全措施的严格性。其核心思想是通过静态分析识别哪些数据在推测执行中不会成为秘密，进而减少不必要的防御加固，降低性能损失。论文的主要贡献包括：形式化非推测知识的概念、设计相应的静态分析算法，并验证该方法能在不牺牲安全语义的前提下提升性能。适合对微架构安全、侧信道防护、编译优化和形式化验证感兴趣的安全研究人员、系统开发者和编译器工程师阅读。由于仅获取了论文摘要，尚无法评估实验细节和具体性能提升幅度，但该研究为缓解推测执行防御的性能瓶颈提供了新思路。

本文首次提出了增广Gabidulin（AG）码的恒定时间解码算法。Gabidulin码是秩度量下的Reed-Solomon码类比，被用于基于秩的密码系统如RQC和Loidreau中。然而，此前缺乏恒定时间实现，这对于实际开发防侧信道攻击的密码系统至关重要。AG码是Gabidulin码的简单变体，通过在码字中添加零列构成，并包含Gabidulin码作为特例，被RQC最有效的变体使用。论文证明了AG码解码可在二次复杂度内完成，并给出了q-多项式左除法的恒定时间算法，完整描述了AG码解码过程。这些算法被集成到RQC-Block-MS-AG方案中，并通过基准测试评估性能。结果表明，该实现优于原始RQC，但比HQC慢约4倍；然而，其密文和密钥大小约为HQC的四分之一，展现了性能与紧凑性之间的优势权衡。本文对密码学实践者，尤其是关注后量子密码系统部署的工程师具有重要参考价值。

本文提出 Xenon，一种求解器辅助的交互式形式化验证方法，用于证明 Verilog 硬件设计在常时执行。常时执行是抵御基于时序的侧信道攻击的关键属性。Xenon 通过引入常时反例的新概念，自动合成最小化秘密假设集合，并在交互式验证循环中定位验证失败根源，显著降低调试工作量。为加速验证，Xenon 利用 Verilog 模块摘要实现模块化，避免重复验证相同实例。实验表明，Xenon 能验证多种电路，包括高度模块化的 AES-256 实现（验证时间从六小时降至三秒）以及 ScarV 侧信道加固的 RISC-V 微控制器（规模比此前验证的设计大一个数量级）。小规模用户研究发现，Xenon 帮助非专家用户比现有工具更正确、更快速地完成验证任务。

该论文系统化了针对密码学实现中时序攻击的防御手段——恒定时间（Constant Time）编程模型。尽管恒定时间编程是抵御时序攻击的主要防线，但学术界和工业界对“恒定时间”的定义和模型理解存在差异。本文首先回顾并整理了恒定时间模型的历史演化，识别出模型所保护的安全属性与密码规范所假设的威胁模型之间存在长期被忽视的差距。作者进一步提炼了一套攻击方法论，用于发现源自密码原语边界之外（例如上层应用或密钥加载流程）的时序漏洞。利用该方法，作者定位了一个与私钥加载过程相关的规范级（specification-level）漏洞。该漏洞存在于OpenSSL和BoringSSL两个流行密码库中，并成功在实验中确认了信息泄露。一个反直觉的发现是：尽管BoringSSL采用了更严格的威胁模型，但其单次观测产生的信号强度反而比OpenSSL高出数个数量级。研究贡献包括：1) 对恒定时间模型进行系统化分类与演化分析；2) 提出可用于发现跨界时序漏洞的通用攻击方法论；3) 发现并验证了OpenSSL和BoringSSL中此前未知的时序泄露点。该论文适合密码库开发者、侧信道安全研究人员以及所有关注密码学实现安全性的工程师阅读。

本文针对嵌入式微控制器（如ARM Cortex-M4）上神经网络推理过程中的激活函数（ReLU, sigmoid, tanh, GELU, Swish）存在的时序侧信道泄露问题，提出了一种常量时间（constant-time）实现方法。该方法通过结合无分支选择、基于Padé近似的固定成本计算、虚拟算术操作以及循环对齐等技巧，确保所有激活函数在不同输入下消耗相同的时钟周期数，从而消除时序侧信道。作者首先评估了一种基于去同步化的防御措施，并证明其仍易受模板化时序攻击，进而提出防御方案。实验结果表明，保护后的实现在三函数和五函数场景下分别实现恒定的88和108周期计数，同时数值误差分析显示近似非线性函数保持高精度。该研究为嵌入式推理中构建抗侧信道的激活函数提供了实用基础，适用于需要安全部署深度学习模型的嵌入式系统开发者及侧信道防御研究人员。