2025 Let’s GoSSIP 软件安全暑期学校预告第三弹——Qide

关心程序分析和代码安全的你，可能经常听说过一个名词——形式化验证（formal verification）。形式化验证是一种通过数学方法验证软件、硬件或系统正确性的技术。它通过建立模型、定义规约，并利用算法对状态空间进行穷尽分析，从而确保系统行为符合预期。通俗一点来说，形式化验证可以用数学方法去数学去精确的论证一个系统是无Bug的，听上去是不是非常高大上？实际上，和传统的各种软件测试方法相比，形式化验证可谓是“超豪华版”的软件测试，用严格的数学论证，保证逻辑没有死角。

可惜，形式化验证技术这些年来一直处于“叫好不叫座”的境地，为什么呢？因为对一套系统（可能是软件，也可以是硬件）建立数学模型是有很高的时间成本的，在有限的人力和时间内，大家写代码就已经很不容易了，如果还要进行数学建模，并写出相关的验证代码，可能会比代码开发本身消耗更多时间，这样可能就让程序员望而却步了。

当然，尽管开销很大，但形式化验证在很多重要的领域还是必不可少的，比如在硬件设计领域，硬件设计周期长，成本高，一旦生产出来就很难改动了，那么就必须要验证设计的正确性；在一些对软件正确性要求极高的行业（比如航空航天、操作系统内核，或者现在的区块链智能合约）也会使用到形式化验证的方式来保障。那大家可能会问了，有没有可能让形式化验证的门槛变得更低一点，让它“飞入寻常百姓家”呢？

当然可以！本次暑期学校，我们邀请到了在形式化验证领域深耕多年的上海交通大学人工智能学院曹钦翔教授，为我们介绍他的团队最新的研究成果——Qide形式化验证交互式开发平台。先给大家介绍下曹老师，他是北京大学哲学（逻辑与科学哲学）和数学双学士、普林斯顿大学计算机博士（大家可以去知乎看看曹老师的评价），长期研究程序验证、程序逻辑与交互式定理证明，并研究人工智能技术在这些领域的应用。自2022年以来，曹老师带领团队研发的形式化验证工具，在若干项操作系统内核的形式化验证工作上得到应用。

推广形式化验证技术是曹老师一直以来的心愿，他在上海交通大学通过开设CS 2206《Programming Verification》这门课程，长期以来向学生传授相关的技术。但是，光有理论（你看下面的这些内容你能理解多少）没有实践，怎么能够更好地推广形式化验证技术呢？为了减少形式化验证的入门门槛，曹老师除了讲课，还开发了一套叫做Qualified C Programming（QCP）的框架，关于这套QCP框架的技术细节，大家可以访问 https://arxiv.org/pdf/2505.12878 去一探究竟。

抛开技术细节不说，在QCP框架的支持下，我们可以获得更友好的形式化验证用户体验。在今年的NSDI会议（录取率不到12.5%，是NSDI历史录取率最低的一次）上，有一篇来自曹老师团队的论文VEP: A Two-stage Verification Toolchain for Full eBPF Programmability就介绍了一个针对eBPF的新型形式化验证工具——VEP（论文在 https://www.usenix.org/system/files/nsdi25-wu-xiwei.pdf 开放访问），充分展示了基于QCP的形式化验证工具的先进性。VEP工具作为一个新型的eBPF验证工具（eBPF程序在内核挂载前都需经过严格的形式化验证过程），实现了完全的可编程性和更好的用户体验，而现有的eBPF验证器（如Linux verifier和PREVAIL）不仅会有很高的安全误报，相关的报错反馈对用户也非常不友好，即使是最为熟练的eBPF程序开发人员，往往也需要花大量时间来定位错误位置和修复。

当然，曹老师的野心不仅限于eBPF，而是朝着面向更通用的C语言代码验证而去。因此，今年暑期学校，曹老师团队会给大家带来更为重磅的在线形式化验证平台——Qide！Qide是一个在线代码形式化验证平台，你可以通过网页版访问，不需要关心底层的形式化验证工具如何部署和执行，只需要一行一行写代码，然后通过注释来描述程序需要满足的相关性质以及必要的检查，Qide就可以自动化帮你检查代码的正确性！听上去是不是很有意思？

本次暑期学校，曹老师团队携Qide重磅出击，会给大家送上一套完整的基于Qide的形式化验证入门课程，包教会！如果你想要在这个夏天掌握一点硬核的技术，那么Qide无疑是最值得的选项之一。感兴趣的同学赶紧点击我们的报名链接（访问 https://summer.gossip.team/2025/signup.php 或者“阅读原文”皆可），预订好上海8月必听的课程吧！