该论文研究推测执行（speculative execution）与信息流语言中“去分类”（declassify）机制之间的相互作用。在实用的信息流编程语言中，程序员可通过 declassify 构造声明有意泄露的数据，例如从私钥计算出的签名或密文通常被信息流分析视为秘密，而密码库可用 declassify 将其公开。论文发现推测执行会导致去分类点产生非预期的信息泄露：攻击者可利用瞬态执行在错误的时间访问正确的内存位置，从而绕过常规信息流保证。作者给出了一个针对 AES 实现的 PoC，能够从标准实现中恢复密钥，该 PoC 是 Spectre 攻击的一个实例，并且在程序使用广泛使用的编译器级防护手段——推测负载加固（SLH）编译时仍然有效。为应对这些攻击，论文提出了形式化对策，包括对 SLH 的重大改进，称为选择性推测负载加固（selSLH）。这些对策能有效地强制执行相对非干涉（RNI），非正式地说，受保护程序的推测性泄露被限制为原程序已有的顺序泄露。作者在专为高保证密码学设计的 FaCT 语言和编译器中实现了最简单的对策，性能开销最多为 10%；虽然未直接实现 selSLH，但初步评估表明，与传统 SLH 相比，selSLH 能显著降低密码学函数的性能成本。该研究揭示了现有防护（如 SLH）在去分类场景下的盲区，为高保证密码学实现提供了新的形式化安全保证和可落地的加固方向。