该论文针对密码学软件中的瞬态执行攻击（尤其是Spectre v1）提出了一种基于类型系统的方法，以确保推测性常数时间（Speculative Constant-Time），从而在保持高性能的同时为密码实现提供形式化保证。当前密码库的黄金标准是在高效实现的同时系统性地防御计时攻击，通常借助高保证密码学工具（如Jasmin框架）进行形式化验证。然而，现有工具基于过于简化的执行模型，忽略了瞬态执行产生的微架构泄漏，导致经过验证的实现仍可能受到Spectre等攻击。已有的防御措施往往因性能开销过大而未被实际采用。作者提出了一种值依赖的信息流类型系统，根据执行是否处于错误推测状态动态跟踪安全级别，从而强制实现推测性常数时间属性。该类型系统被集成到Jasmin框架中，并用于保护一个实验密码学库的全部实现，涵盖对称原语、椭圆曲线密码（如X25519）以及Kyber（NIST选定的后量子KEM）。实验结果表明，性能开销极低：Kyber的开销小于1%，X25519几乎为零。这项工作证明了形式化方法可以在不显著牺牲性能的前提下有效缓解瞬态执行攻击。论文的主要贡献包括：提出推测性常数时间的正式定义、设计并实现相应的类型系统、将其集成到Jasmin框架，并通过实际密码库验证其实用性。适合密码学库开发者、系统安全研究员以及形式化验证社区阅读。

本文研究有限域上的Frobenius线性化算子的一种正规形分类。设K为二元域F_2的有限扩张，σ为K上固定非平凡的Frobenius自同构，其固定子域为F_2。考虑K^3上两个二项式组成的算子L(Y)=AY^σ+BY，其中A、B为3×3矩阵。作者在系数秩和二元核条件下，证明若A和B的K秩都为2，且L在F_2上的一维核，则存在可逆的K线性输入输出变换，使得L等价于规范形(α,β,γ)↦(α^σ+α,β^σ,γ)。该证明通过从两个系数核方向和二元核构造坐标框架实现。在这一坐标下，第一输出行恰好是唯一的非零迹伴随正规元，并得到精确的K值归一化。对于纯σ-二次APN（几乎完全非线性）映射，该结果通过π_F(X)^T F(X)=1识别出orthoderivative；在奇数扩张次数下还得到置换行为和射影平面到其对偶的双射。文中分析了两个具体的构造：Gologlu-Kolsch的三射影构造和Li-Zhou-Li-Qu的范数扭构造，前者具有行列式分解和完全对偶框架，后者展示了纯映射结果无法单独从算子定理推出。此外，Gold表示的系数秩对为(3,3)，限定了秩二子类的范围。该正规形还为已知的分量根和Walsh支撑关系提供了扩域上的精确标签。这些成果对理解APN函数的结构、进而设计抗差分密码分析的S盒具有理论意义。