该论文针对形式化验证程序中的一个关键盲区：即便程序通过了形式化验证，其正确性仍受限于规范（SPEC）的完整性。若规范本身存在漏洞或不完整，验证结果将失去意义。作者提出了一种名为 Fast（Fuzzing-Assisted Specification Testing）的自动化方法，利用同一代码库中规范、实现和测试套件均由同一业务需求派生出的冗余性和多样性进行交叉验证。核心思想是：如果某个意图在实现和测试用例中有所体现，却未被规范捕获，则强烈暗示规范存在盲点。Fast 首先通过变异测试定位规范缺口，即检查代码变体是否仍然符合原始规范；若符合，则进一步利用测试套件推断该缺口是有意引入还是疏忽所致。针对不同规模的代码库，Fast 可选择枚举式或进化式方式生成代码变体。作者在两个具有形式化验证的开源代码库上应用 Fast，分别确认了 13 个和 21 个规范盲点，证明规范不完整在真实应用中普遍存在。该研究为提升形式化验证的可信度提供了一种辅助手段，适合形式化方法、软件测试和安全研究人员阅读。

该论文针对以太坊上最流行的智能合约编译器——Solidity编译器中的误编译漏洞（miscompilation bugs）进行了系统性的发现与分析。智能合约编译器的正确性对于保证区块链上不可篡改的开源代码的正确执行至关重要。作者开发了SolSmith，一种语义感知的差分模糊测试工具，在三年内持续检测Solidity编译器，发现了25个未被发现的误编译漏洞，其中一些已存在多年。SolSmith通过生成有效的测试程序，压力测试编译器的代码生成和优化组件，从而发现常规测试无法捕获的缺陷。论文的贡献包括：1）使编译器测试更加严格，减少因编译器错误导致的智能合约缺陷；2）对发现的误编译漏洞进行了定性和定量分析，按其性质、根本原因和最终用户影响进行分类，揭示了优化编译器的一些常见陷阱。该研究对于提升Solidity编译器的可靠性和安全性具有重要意义。

本文提出 JailFuzzer，一种基于大语言模型（LLM）代理的自动化模糊测试框架，用于黑盒环境下对文本到图像（T2I）生成模型进行越狱攻击。现有越狱方法存在访问需求不切实际、提示语不自然易被检测、搜索空间受限以及查询开销高等问题。JailFuzzer 结合模糊测试原理与 LLM 代理，包含三个核心组件：种子池（存储初始及越狱提示）、引导变异引擎（利用 LLM 代理生成语义有意义的变异）、以及 oracle 函数（评估越狱是否成功）。通过 LLM 代理构建引导变异引擎和 oracle 函数，使得框架在黑盒环境下保持高效性和适应性。大量实验表明，JailFuzzer 在越狱 T2I 模型方面具有显著优势：生成的提示自然且语义连贯，降低了被传统防御机制检测的概率；同时以极少的查询开销实现高成功率，在所有关键指标上优于现有方法。该研究揭示了 T2I 模型面临的新型越狱威胁，为强化生成模型的安全机制提供了重要参考。JailFuzzer 已开源，代码可在 https://github.com/YingkaiD/JailFuzzer 获取。