该论文针对当前软件安全中广泛使用的消毒器（sanitizer）存在的冗余检查问题展开研究。消毒器通过插入运行时检查来检测内存错误、未定义行为等漏洞，但大量检查是冗余的，因为开发者已在代码中通过类型检查（如显式的类型转换或条件判断）隐含地保证了安全性。作者提出了一种名为“PruneSan”的方法，利用静态分析自动识别并移除那些由开发者已实现的类型检查所覆盖的冗余消毒检查。该方法首先构建程序的控制流图和数据类型流，然后通过符号推理判断消毒检查的条件是否已被类型检查所蕴含。实验评估在多个真实项目（如OpenSSL、FFmpeg等）上进行，结果表明PruneSan能够安全地移除平均30%的消毒检查，同时显著降低运行时开销（最高达45%），且未引入任何新的误报或漏报。该工作为在保证安全性的前提下优化消毒器性能提供了有效途径，适用于需要高安全性与高执行效率的C/C++程序。

该论文提出了一种名为 ILA（Intermediate Language for FHE）的中间语言和类型系统，用于确保全同态加密（FHE）程序的正确性。FHE 允许在密文上进行任意计算，但现有 FHE 编译器容易引入错误，例如密文噪声管理不当或运算类型不匹配。作者设计了一个类型检查框架，该框架在类型层面编码了密文的安全参数（如噪声预算、乘法深度等），使得类型安全的程序能够保证在解密后得到正确结果。具体而言，ILA 的类型系统包含依赖类型，可以跟踪每个值的噪声增长，并在编译时拒绝可能超出噪声阈值的操作。此外，论文还形式化了类型系统的正确性定理，证明类型良好的程序不会产生解密失败的输出。实验评估使用多个经典 FHE 应用（如线性回归、神经网络推理）来验证类型系统的有效性，结果显示 ILA 能够捕获多种常见的错误，且类型检查的开销在可接受范围内。该研究属于密码学与编程语言的交叉领域，为构建更可靠的 FHE 编译器提供了理论基础。