2023年12月1日下午，2023年度CCF中国软件大会证明工程与安全编程论坛在上海国际会议中心3E会议室成功召开。
本次论坛由上海交通大学曹钦翔和北京大学王迪两位老师组织举办。论坛包括5个报告和1个圆桌讨论，邀请了清华大学王生原、上海交通大学汪宇霆、中国科学院软件研究所詹博华、粤港澳大湾区数字经济研究院张宏波和上海交通大学曹钦翔5位嘉宾。论坛主要关注如何平衡软件的安全保证和开发效率，并从“证明工程”的视角展开讨论。证明工程旨在打造一套统一软件开发与形式化证明的高效框架。论坛嘉宾的报告涵盖了可信编译、证明模块化、定理自动证明、安全语言设计和程序验证。最后围绕证明工程的现状、难点和未来进行了圆桌讨论。
清华大学王生原做报告《L2C项目及其进展》。报告介绍了同步语言可信编译器L2C的研发背景、内容及最新进展，并从L2C作为证明工程的案例的角度总结了实践经验。L2C可信编译器的源语言拥有兼容于Lustre V6 或 Scade的模型算子，在核工程、航天等领域有业界实际应用。王生原提出证明工程领域应积极推动关键领域工业标准的进步、进一步开展证明方法学的研究、构建基础理论以及推广专业教育。
上海交通大学汪宇霆做报告《面向一阶语言的可组合编译器验证》。报告关注针对一阶语言（即不含高阶程序和高阶状态的语言）的编译器验证，介绍了基于语法和语义的可组合编译器认证方法，以及其团队即将发表于POPL 2024的基于直接精化的可组合编译验证的工作。汪宇霆在报告最后提出可组合编译验证是支持模块化程序验证的重要前提，可组合编译的下一步研究可考虑高阶语言、复杂控制流或新型安全语言。
中国科学院软件研究所詹博华做报告《HolPy交互式定理证明器与证明自动化》。报告介绍了HolPy，是一个由报告人团队设计并开发的使用Python实现的交互式定理证明器，它的一个特点在于允许用户使用基于Python的API实现证明自动化以及其他扩展。报告进一步讨论了在HolPy中实现证明自动化的案例，包括SMT证明的重构以及程序验证中的应用。詹博华最后提出证明工程需考虑工具的易用性、自动化程度和正确性保障。
粤港澳大湾区数字经济研究院张宏波做报告《MoonBit：WASM驱动的云计算和边缘计算智能安全开发平台》。报告介绍了MoonBit，一个由报告人团队设计并开发的自研编程语言。MoonBit专门为WebAssembly（Wasm）设计，利用类型系统安全、删减无用代码以及编译为经过验证的Wasm指令来确保代码可信与数据隐私安全。张宏波提出通过语言设计释放Wasm潜在潜能，比如调整语言特性以方便AI进行代码自动生成等应用。
上海交通大学曹钦翔做报告《VST-A项目及其进展》。VST是基于分离逻辑的C语言程序功能正确性验证工具。VST-A是报告人团队在VST的基础上构建的基于C语言中的断言标注生成功能正确性证明的大致框架，将C函数的功能正确性验证规约为分离逻辑断言推导性质的判定，相关工作即将发表在POPL 2024。曹钦翔最后提出系统软件验证需解决复杂规约书写、复杂算法证明以及支持实际语言的语言特性。
在所有报告结束后，5位论坛嘉宾进行了圆桌讨论。讨论就三个问题展开：（1）证明工程当前有哪些应用？（2）证明工程和安全编程中有什么核心困难，如何解决它们？（3）将来的安全编程语言会是什么样的？论坛嘉宾们认为证明工程目前在一些安全攸关的核心领域有主要应用，但将来随着证明工程难度的降低，安全编程的应用会越来越广。证明工程的主要难度在于证明的成本很高，目前形式化证明和开发效率间还很难平衡。将来的安全编程语言可能会以领域特定语言的形式为不同领域设计，但需要一套统一的理论框架；可以通过语言设计来辅助降低证明的成本，就像Rust之于内存安全；也应当支持渐进式验证，在开发的过程中不立即要求完成证明或者只需要对核心代码进行证明。嘉宾们与听众进行了互动，北京大学胡振江评论道证明工程的发展也需进一步理清证明中真正难的部分，通过将不难的部分自动化来提高证明效率。在大家畅所欲言的交流中，论坛也顺利圆满结束了。
声明：本文来自CodeWisdom，版权归作者所有。文章内容仅代表作者独立观点，不代表安全内参立场，转载目的在于传递更多信息。如有侵权，请联系 anquanneican@163.com。
