主要观点：C 语言中的未定义行为常导致严重安全漏洞，一种实际缓解方法是分区，本文介绍了 SECOMP 编译器，可将大型程序结构化为相互不信任的分区，其带有机器检查证明，能限制未定义行为范围，保证安全属性对抗对抗性上下文，是首次为主流编程语言证明如此强的准则，通过扩展 CompCert 验证的 C 编译器语言及相关优化和证明来实现。
关键信息：

• 给出了 SECOMP 编译器的相关介绍及作用。
• 提及 CCS'24 版本有更新和扩展，包括附录和更多参考文献。
• 说明了提交历史，包含多个版本的时间和大小等信息。
  重要细节：
• 强调了未定义行为对 C 语言安全的影响。
• 具体说明了 SECOMP 限制未定义行为范围的方式及保证的安全属性。
• 详细列出了 CompCert 编译器的扩展及相关优化和证明的调整。