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

本文提出了一种在原生编译的 WebAssembly（Wasm）上实现软件故障隔离（SFI）安全保证的方法。研究背景在于，WebAssembly 最初设计为在浏览器中以解释或 JIT 方式运行，其内存安全依赖于运行时检查；然而随着 Wasm 被广泛应用于边缘计算、插件系统和云原生环境，越来越多的场景选择将 Wasm 直接编译为原生代码（AOT）以提升性能。但 AOT 编译会绕过原有运行时边界，导致 Wasm 固有的沙箱隔离能力退化，恶意或受损的 Wasm 模块可能直接访问宿主进程的地址空间，造成严重安全风险。为此，作者提出了一个名为 “Trust, but verify” 的框架，其核心思想是在不牺牲原生执行性能的前提下，通过静态验证与轻量级运行时检查相结合的方式，重新建立 SFI 边界。具体而言，该方法利用编译器在生成原生代码时插入必要的安全检查（如边界检查和间接调用目标验证），并辅以形式化方法证明这些检查的完备性，从而保证即使模块是恶意的，也无法逃逸其隔离域。作者在基于 LLVM 的原生 Wasm 编译器上实现了原型，并通过一系列安全相关基准测试和真实应用测试，验证了该方案能够有效检测并阻止多种越权访问尝试，同时性能开销远小于传统的纯软件沙箱方案。该研究适合系统安全、编译器安全和边缘计算领域的从业者，以及任何依赖 Wasm 插件生态的软件架构师阅读，以深入了解在不安全的原生执行路径上如何保持隔离保证的可行路径与工程权衡。

本文提出并实现了一个名为 Verbatim 的可执行词法分析器（lexer），其开发和验证均基于 Coq 证明助手。词法分析器和解析器常被用作大型软件系统的前端，负责连接外部输入与系统内部逻辑，因此成为攻击者试图攻陷整个系统的天然目标。作者认为，一个经过形式化验证、具备机械化词法分析能力的工具能够显著降低针对这些前端的攻击效力。论文的核心贡献在于：1）给出了 Verbatim 的完整实现，它是一个可执行的、与标准词法分析器规范兼容的 lexer；2）在 Coq 中机械证明了 Verbatim 相对于标准词法分析器规范的正确性，即所有正确性证明均已机器检查，避免了手工证明中可能存在的漏洞；3）分析了 Verbatim 的理论复杂度，并提供了实证性能评估结果。与依赖测试或运行时检查的传统 lexer 生成器不同，Verbatim 从构造上保证了词法分析的正确性，为构建高可信软件前端提供了新的思路。该研究适合对形式化验证、编译器前端安全、高保证软件工程感兴趣的 researchers 和开发者；对于蓝队而言，理解这类验证工具可帮助评估在关键系统中引入形式化验证组件的可行性和收益，从而减少外部输入处理环节的潜在攻击面。然而，由于本文尚未发布完整工具链或大规模应用案例，其实际工程部署价值仍需进一步验证。

本研究首次系统性地揭示了深度学习编译器中的编译不一致性漏洞（Compilation Inconsistency Vulnerability）。作者发现，即使是官方、未经修改的深度学习编译器，也可能在模型编译过程中静默改变模型语义，从而引入隐藏后门。研究从两个角度展开：对抗性设定和自然设定。在对抗性设定中，作者精心构造了良性模型，其中的触发器在编译前不产生任何效果，但经过编译器编译后，触发器变为有效的后门。在6个模型（包括ResNet、BERT等）、3个商用编译器（如TensorFlow XLA、PyTorch JIT、TVM）以及2种硬件平台（CPU和GPU）上的实验表明，该攻击对触发输入的成功率为100%，同时保持正常准确率，并能绕过最先进的防御检测器。攻击泛化到不同编译器、硬件和浮点设置。在自然设定中，作者分析了HuggingFace上排名前100的模型（包括一个下载量超2.2亿的模型），发现其中31个模型存在自然触发器，即在编译后模型对某些正常输入的行为发生改变。这表明即使没有对抗性操纵，编译器也可能引入风险。该工作首次暴露了深度学习编译器设计中被忽视的安全威胁，为构建安全可信的机器学习系统开辟了新方向。