程序验证的模块化、代码专门化和零成本抽象
摘要：大规模证明开发的结构、架构和工程方面很少有研究，本文提出了一组基于语言的技术，允许程序员在高级抽象层次上模块化编写和验证代码，同时保持对编译过程的控制，生成适合集成到主流软件的高质量、零开销、低级别代码。我们在F*证明助手中实现了这些技术，特别是它的浅嵌入式Low*工具链，可以编译为C语言。通过我们的评估，我们确定我们的技术对于将流行的HACL*库扩展到超过10万行经过验证的源代码至关重要，并显著提高了证明工程师的生产力。我们的方法论的阐述最终聚焦在一个新颖的案例研究上：流式API，这个易出bug的API在过去给高知名度软件带来了很多问题。通过我们的方法，我们成功以一种通用的方式捕捉了流式语义，并将其免费应用于十几个用例。其中六个已经进入了Python编程语言的参考实现，替代了以前有漏洞的代码。
作者：Son Ho, Aymeric Fromherz, Jonathan Protzenko
论文ID：2102.01644
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-07-10