操作系统形式化验证做到第3篇终于要开始“图省事”的部分了。前面我们聊过什么是形式化验证、为什么操作系统需要它、以及手工证明到底有多痛苦这一篇直接进入工具实操。标题里的“自动证明工具”往大了说包括SMT求解器、自动定理证明器、交互式证明器里的自动化策略、以及模型检测后端往小了说就是让你不用手写几百条推理步骤把目标扔给机器去跑的东西。这篇我会先帮你把各种工具的关系捋清楚然后用两个能实际跑通的最小实验演示怎么用自动工具验证操作系统常见的同步和调度性质。我自己刚开始接触这块时有一个错误预期以为自动证明工具能像编译器一样把“这段代码有没有错”直接给出yes/no。实际用过之后才发现工具给你的更像是一种“加速器”它不会替你想明白规格是什么但能把大量重复、机械的证明工作接过去。这篇文章的目标就是让你以最快速度建立起这个可靠、可复现的实践路径。1. 操作系统验证为什么离不开自动证明工具1.1 操作系统形式化验证的特殊难点操作系统和普通应用程序的形式化验证有个本质区别普通程序验证往往针对算法正确性操作系统的正确性则跟并发、中断、共享内存、硬件交互缠绕在一起。比如一个调度器状态集合包括每个线程的状态、就绪队列、优先级位图、上下文切换标志位一个锁的实现又牵扯到内存屏障、原子指令、快中断路径。这些东西叠加起来状态空间立刻爆炸。如果只靠一个人拿着Coq或者Isabelle手工输入证明步骤大概率会被卡死在琐碎的推导上。我记得自己第一次尝试证明某内存管理模块里的页表操作语义光是维护一堆关于地址对齐和指针有效性的引理就花了两周时间最后发现前置条件少写了一个“页目录项已清零”。这种体验非常打击信心。手动证明不是不可能而是面对操作系统那种规模的模块可维护性太低。于是自动证明工具就变成了刚需。这里说的“自动”不是全自动而是把证明任务拆成两种一是逻辑上机械、但手工写起来很繁琐的推导交给SMT或者自动定理证明器处理二是需要归纳或者扩展证明意图的地方仍然由人给出关键引理工具负责把剩余部分补完。操作系统验证的实际工程里几乎没有人会从头到尾手写证明脚本大家都是在自动化和人工引导之间找一个平衡点。1.2 自动证明工具到底帮你省了什么省下的第一件事是反例搜索。你在设计一个锁协议时最想知道的不是“它为什么正确”而是“它哪里错了能不能找出一个执行序列让两个线程同时进临界区”。这种反例搜索对SMT求解器来说再合适不过。你把状态转移编码成约束把“存在一条路径到达坏状态”编码成可满足性问题求解器会给出一个具体的赋值也就是一条反例路径。省下的第二件事是证明骨架的生成。定理证明环境里的自动化策略能自动处理布尔逻辑、等式推理、线性算术、归纳规则等基础推导。Isabelle/HOL里我最常用的命令是sledgehammer它会并行调用多个外部ATP和SMT求解器直接尝试证明当前目标返回一个可复查的证明片段。这意味着你只需要确定“该证明什么”而不用亲自写“怎么证明”。对于操作系统代码抽象出来的最终同余条件、单步不变式证明这种模式非常常用。省下的第三件事是假设一致性检查。比如你给系统调用接口定义了前置条件写了一个C函数的简化模型又写了一个规范层。自动工具能够检查两个层的逻辑是否矛盾能帮你发现“这个函数实际上在条件不满足时也会修改共享变量”这类问题。这在代码评审里可能要靠肉眼找但形式化工具能给你精确的反例。1.3 哪些证明任务可以自动完成不是所有证明任务都适合自动工具。按照我的经验以下三类最值得交给自动工具建立系统不变式。比如“任意时刻最多只有一个线程处于临界区”、“调度队列不会出现同一个任务两次入队”。这类性质通常可以写成一条逻辑公式交给SMT或者Isabelle的归纳证明策略。函数或状态机的单步等价性。比如“执行某个系统调用前后的状态关系满足某个前向模拟条件”如果涉及的表达式主要是if-else、算术比较、位运算和结构体字段SMT基本能一键解决。路径条件的约束求解。例如在内核代码里面if (a b) 之后发生了什么要证明某个错误路径实际上不可达。把控制流提取成语义上的布尔路径后交给求解器判定可满足性。反过来说依赖复杂归纳假设、涉及高阶递归函数、需要构造新对象或新不变量的时候直接“自动证明”往往不够需要你手工给出关键引理。我能给的实用建议是先尝试自动工具让它告诉你哪里推不动再根据失败信息手动补一条引理循环往复。这个循环本身就是形式化验证实践中最真实的工作状态。2. 工具全景别把SMT和定理证明器混为一谈2.1 SMT求解器反例搜索和约束检查的主力SMT全称是Satisfiability Modulo Theories可满足性模理论求解。你把自己的问题编码成布尔变量加一些理论术语比如整数线性算术、位向量、数组、未解释函数SMT求解器会告诉你这个公式有没有解。最典型的工具是Z3和CVC5国内工作流里用Z3做反例生成非常普遍。举个例子你想检查一个内存分配器的分配逻辑是否可能越界。把分配前的堆状态建模成数组把分配函数建模成修改数组的公式把越界条件写成逻辑公式Z3如果能找到一组赋值说明存在一个输入和堆状态导致越界如果返回unsat说明在这些约束下不会越界。这比暴力枚举所有输入快得多而且不需要你提供测试用例。用SMT时要注意一个问题它不会告诉你“为什么正确”只告诉你“定理是否在特定理论下可满足”。所以在操作系统验证流程里SMT一般充当加速器负责在早期不断攻击你的模型、寻找反例。一旦SMT给出的反例越来越少再进入定理证明器阶段固定结果。2.2 一阶自动定理证明器ATP的角色自动定理证明器ATP比如E、Vampire和Zipperposition主要处理一阶逻辑的推导。它们擅长在庞大的一阶公式集合里找出一组推导证明目标公式必然成立。它们的推理能力很强但面对高阶逻辑和归纳定义往往力不从心。在Isabelle/HOL里sledgehammer就是把这组ATP和SMT工具串起来用的。你把一个目标提交给sledgehammer它会把当前上下文里的所有引理翻译成一阶问题交给后台工具若有工具找到证明再翻译回Isabelle能检查的证明脚本。这样做的好处是外部工具的证明结果会重新被Isabelle内核验证所以外部工具哪怕有bug也不会污染最终结论。这一点对操作系统这种安全攸关领域是非常重要的。实操中我经常在Isabelle里写完一个lemma后直接敲try0先跑一遍内建自动化跑不过再上sledgehammer。很多情况下并不是目标本身有多难而是你忘了把某条关键引理引入上下文。sledgehammer会在结果里告诉我们它用了哪些引理这会反过来帮你理解证明结构。2.3 交互式定理证明器的自动化策略Coq和Isabelle/HOL这些交互式定理证明器严格来说不叫“自动证明工具”但现代交互式证明器内置了大量自动化策略。Isabelle/HOL有auto、force和simpCoq有omega、lia和现在常见的firstorder。这些策略能处理一大类原子运算和命题推导让你不用一步步应用规则。关键区别在于这些自动化策略运行在逻辑内核之上所有证明步骤都要生成可检查的证明项或证明论据。这比外部SMT的可信度更高但也因此更慢、更受限制。操作系统验证里如果要保证最终“机器可检查”那么核心证明脚本应该由这些内建策略完成外部ATP和SMT可以作为发现证明路径的辅助工具。2.4 模型检测器状态空间上的自动验证模型检测工具比如NuSMV和Spin专门在有限状态系统上自动遍历状态空间检查时态逻辑性质。它们不是“证明”工具而是“穷尽”工具但对于操作系统里很多带有时序关系的协议模型检测的自动化程度比定理证明高得多。你可以把自旋锁的协议建模成一个有限状态自动机将互斥性写成CTL或者LTL公式然后用模型检测器一次性跑完所有状态。如果它给出失败路径就可以直接得到一条反例序列如果全部通过说明在有限状态抽象下性质成立。局限也明显模型检测必须面对状态爆炸而且验证结果只对“你建模出来的那个抽象”负责离真实C代码还有一段距离。因为这一篇的主题是“自动证明工具”我把模型检测当作补充性工具来推荐。真正动手做操作系统模块验证时我的路径往往是先用Z3快速找逻辑矛盾再用模型检测器验证有限状态的协议最后用Isabelle/HOL对核心性质做机器可检查的证明。三层互补各管一段。2.5 选型表格与组合策略工具类型代表工具自动化程度擅长的验证任务局限SMT求解器Z3、CVC5较高路径条件检查、反例搜索、位向量和数组约束无法处理复杂归纳和高阶逻辑一阶ATPE、Vampire较高一阶逻辑推导、大公式集上的定理发现对操作系统常见的递归定义支持弱交互式证明器内建策略Isabelle/HOL的simp/auto、Coq的lia中基础推导、等式推理、线性算术面对复杂引理仍需人工引导模型检测器NuSMV、Spin高有限状态协议、时序性质验证状态爆炸、模型抽象过度选型策略简单说就是反例靠SMT协议靠模型检测交付靠定理证明器。三者是协作关系不是替代关系。很多刚入门的同学会问“学了Z3是不是就不用学Isabelle了”答案是否。只要你还需要“机器可检查的证明”就要落到定理证明器的逻辑内核上只要你还在设计阶段快速迭代SMT的反例能力就不可替代。3. 最小实验一用Z3验证互斥锁协议3.1 建模思路把锁协议变成公式这一节我用一个极简的Peterson锁模型演示SMT怎么用于操作系统验证。实际问题里你还要考虑弱内存模型这里先忽略它只看“互斥性”这个基础性质。Peterson锁的核心状态是三个变量两个线程各自想要进入临界区的标志flag0和flag1以及一个表示“谁最后表达意愿”的turn变量。进入临界区的逻辑是先把flag_i设为真再设置turn等于对方线程号然后检查对方是否也想进临界区并且turn是否还被自己持有。如果对方不想进或者turn已经改成了对方那就进去。临界区结束后把flag_i设为假。这个算法只有三个共享变量看起来简单但“为什么会互斥”的论证还得仔细想。用Z3验证时我不会去证明算法在所有执行序列下都正确而是构造“某个状态下双方都满足进入临界区条件并且都在临界区里”的约束让Z3找反例。3.2 用Z3做不变式检查我用Python版的z3来写这个检查。第一步是先定义状态变量把它们声明为布尔变量然后构造“一个线程满足进入临界区条件”的公式。互斥性要求两个线程的临界区条件不能同时成立。如果这个公式有解说明协议在某一时刻可能被破坏Z3会给出具体赋值。from z3 import * flag0, flag1 Bools(flag0 flag1) turn Bool(turn) # False 代表 0 线程意愿True 代表 1 线程意愿 # 线程 0 进入临界区的条件 def can_enter_0(): return flag0 True and Not(flag1 True and turn False) # 线程 1 进入临界区的条件 def can_enter_1(): return flag1 True and Not(flag0 True and turn True) s Solver() # 假设两个线程都希望进入临界区 s.add(flag0 True) s.add(flag1 True) s.add(can_enter_0()) s.add(can_enter_1()) result s.check() if result sat: print(找到反例, s.model()) else: print(互斥性质在给定条件下成立, result)这个模型当然极其简化。我们固定了“两个线程都设置了自己的flag为真”这个状态。在这个前提下Z3如果返回unsat说明它们不可能同时认为自己有资格进入临界区如果返回sat模型里的赋值就是违反互斥的一条线索。真正常见的错误是turn条件的符号写反Z3会很容易找出一组赋值比如flag0true、flag1true、turnfalse时两个can_enter都成立马上让你意识到抽象里的错误。3.3 用有界搜索找反例光检查一个静态状态还不够操作系统并发问题的反例往往要跨越多个步骤。更贴近实际的做法是给定一个初始状态让所有线程任意执行若干步然后看能否到达一个违反互斥的状态。这个叫有界模型检测本质是把“有限步里是否存在坏路径”编码成SAT/SMT问题。def check_bad_path(depth5): s Solver() # 对每一时刻 k 定义状态变量数组 F0 [Bool(ff0_{k}) for k in range(depth 1)] F1 [Bool(ff1_{k}) for k in range(depth 1)] T [Bool(ft_{k}) for k in range(depth 1)] In0 [Bool(fin0_{k}) for k in range(depth 1)] In1 [Bool(fin1_{k}) for k in range(depth 1)] # 初始状态 for k in range(depth 1): if k 0: s.add(F0[k] False) s.add(F1[k] False) s.add(In0[k] False) s.add(In1[k] False) # 每一步线程0或线程1执行“请求进入并可能进入” for k in range(depth): choose0 Bool(fstep0_{k}) # 表示这一步线程0执行 choose1 Bool(fstep1_{k}) s.add(Or(choose0, choose1)) s.add(Not(And(choose0, choose1))) # 统一建模如果线程0执行 s.add(Implies(choose0, F0[k 1] True)) s.add(Implies(choose0, T[k 1] False)) s.add(Implies(choose0, In0[k 1] And(F0[k 1] True, Not(And(F1[k] True, T[k 1] False))))) # 线程1类似 s.add(Implies(choose1, F1[k 1] True)) s.add(Implies(choose1, T[k 1] True)) s.add(Implies(choose1, In1[k 1] And(F1[k 1] True, Not(And(F0[k] True, T[k 1] True))))) # 未修改的变量保持不变 s.add(Implies(choose0, F1[k 1] F1[k])) s.add(Implies(choose0, In1[k 1] In1[k])) s.add(Implies(choose1, F0[k 1] F0[k])) s.add(Implies(choose1, In0[k 1] In0[k])) # 坏状态某一时刻两个线程都在临界区 s.add(Exists(k, And(k 0, k depth, In0[k] True, In1[k] True))) if s.check() sat: return s.model() return None m check_bad_path(6) if m is None: print(在6步内没有找到违反互斥的路径) else: print(m)这个建模同样很粗糙变量“进入后没有退出”这个动作没有建模真实模型还要把退出临界区、任意调度、中断抢占等因素加进去。但我的目的是展示核心思路自动工具不是你按下按钮就魔法般地验证了系统你需要把状态、动作、性质都翻译成约束。任何一步翻译错了结果都不可信。这也是自动化验证里最考验人的地方。4. 最小实验二用Isabelle/HOL证明一个调度器单步性质4.1 抽象出一个极小的调度器如果说Z3负责反例那么定理证明器负责“把它钉死”。这一节拿一个微型调度器举例系统里有若干个任务任务状态分为就绪和运行每运行一个时间片调度器从就绪队列中选一个任务执行运行中的任务要么继续运行、要么被抢占回到就绪队列。我们想证明一个非常基础的性质在一个步进之后“运行中”的任务集合不会包含两个不同的任务。实际在Isabelle/HOL里我会先定义任务类型和调度器状态。任务可以用natural数表示调度器状态用一个三元组表示就绪队列、当前运行任务、当前是否空闲。单步函数有两种情况如果没有运行任务就把就绪队列里最小的任务调度出来如果有运行任务则保持或换入新任务。这里我给一个示意性的定义实际代码会根据你说要支持的调度算法变化但轮廓是稳定的datatype scheduler_state Sched (running : nat option) (ready : nat set) fun schedule_step :: scheduler_state ⇒ scheduler_state where schedule_step (Sched None ready) (if ready {} then Sched None {} else Sched (Some (Least ready)) (ready - {Least ready})) | schedule_step (Sched (Some r) ready) (Sched (Some r) ready)从定义上看这个函数在空闲时会选择一个目前最小的任务作为运行任务并把它从就绪集合中移除有运行任务时则保持不变。要验证的性质是单步执行后running字段要么是None要么只有一个值。这个性质由datatype本身就保证了用一个简单的结构归纳就能完成。实际操作系统调度器当然没有这么显然你会引入优先级、抢占点、时间片到期等因素此时证明就会变得有料。4.2 提交自动证明命令在Isabelle/HOL里这种“由定义几乎显然推出”的引理用一行命令就能完成lemma step_running_unique: schedule_step s Sched (Some r1) ready1 ∧ schedule_step s Sched (Some r2) ready2 ⟹ r1 r2 apply (cases s; auto) donecases s让自动化看到调度器状态的构造形式auto会把两种情况用化简和逻辑推导自动处理。如果这个引理麻烦一些我会先敲try0让Isabelle的内建自动化尝试多种组合策略还不行就用sledgehammer它会启动外部ATP和SMT去工作然后返回类似by (metis ...)的证明命令。这个过程中最有价值的不是最后那句证明而是当你给出的假设不足时自动工具会在哪里停住、报告什么样的剩余目标。比如上面的例子如果ready {}分支处理得不仔细证明目标会残留“某个最小元素等于None”之类的子目标这时你要修改定义或者增加明确的公平性假设。工具不会告诉你“你的需求错了”但它会告诉你逻辑上哪里连不起来。4.3 自动工具失败后怎么拆目标我碰到最多的失败情形是自动工具面对一个看似简单、但需要额外引理的目标时一直转圈。这时候先不要硬试更强的自动策略而是停下来分解目标。一种常见做法是引入一个中间断言。比如想证明某个队列操作后有序性保持不变可以先证明“新插入的元素大于等于队列中所有已有元素”再把这条断言作为引理交给后续证明。对于调度器性质假如我要证明“若系统空闲则就绪队列为空”。单看定义好像很直接但如果schedule_step里有一个把任务放回就绪队列的分支这个性质就不一定成立。自动工具会尝试通过定义展开来证明失败后你需要人工检查是否是在空闲状态下确实没有步骤会往队列里放任务。一旦确认就把“return到ready队列”这个动作建模为不改变空集性质的函数然后交给auto。经验是凡是遇到自动证明卡壳优先怀疑不是工具能力不足而是你的模型缺少了一个该说的假设。我一直把这句话写在笔记本第一页“形式化验证里的每个证明失败都是在提醒你把约束说得更清楚”。这不是玄学是实操总结。5. 常见问题与排坑实录5.1 SMT超时模型不输出怎么办Z3跑很长时间不出来多半不是你模型太复杂而是你把目标公式写成了二重嵌套存在量词或全称量词导致求解器一直在试图搜索一个巨大或者稀疏的空间。一个实用的做法是缩小范围先固定一部分参数为具体常数跑一个更小的实例看是否能够找到反例或者把位向量宽度从32位降到8位先让求解器快速给出一个方向再回归完整模型。我经常用set_option(timeout, 10000)给Z3设一个10秒的超时。如果它返回unknown我不会把这个结果解读为“性质是否成立未知”我会先重审建模看看是不是公式里用了求解器不擅长处理的结构比如非线性算术或者混合实数整数。操作系统代码里的位操作最好直接用位向量类型不要转成整数否则会让求解器做很多额外工作。5.2 定理证明器卡住先调整上下文再调策略Isabelle/HOL里同一个目标有时auto转几秒钟就完成有时sledgehammer跑完所有外部工具也没结果。前者通常是因为目标结构和你定义的化简规则匹配后者是因为外部工具需要一条你没带进来的引理。解决办法是检查sledgehammer的输出它会显示用了哪些已知引理如果里面没有你需要的那条就在目标前用using lemma_name把它导入。有一种常见低级错误是把引理导入之后目标反而更复杂因为自动化工具使用了不恰当的重写方向。比如一个等式引理a b被反复展开导致栈溢出。遇到这种情况我会改用subgoal premises临时把关键前提拿出来手动应用一次引理再继续自动策略。别指望工具能当你肚子里的蛔虫自动化的使用技巧有一半就是知道什么时候该介入。5.3 模型离代码太远证明通过代码却对不上这个问题在整个验证实践里最隐蔽也最要命。你辛辛苦苦用自动工具证明了调度器抽象模型的正确性结果把证明结论映射回C代码时发现C代码里的循环条件多了一个或者普通的数组访问被编译器优化成了向量化指令。证明针对的模型和真实代码之间存在缝隙严格来说之前做的一切都不能算数。针对这个问题的务实方案有两条第一在模型和代码之间建立显式的“细化关系”比如每个抽象的ready集合对应到C模块里就绪队列的首尾指针和元素数组索引范围那么你要把“指针范围内的元素都满足某种谓词不变式”也纳入证明目标第二对无法完全形式化的部分通过运行时断言和静态验证工具兜底比如用契约标注函数的前置后置条件让SMT定期做低成本的回归检查。5.4 自动证明不适合验证什么自动证明工具也不是万能的。对于需要深层归纳的证明比如证明某个调度算法在所有步数下的公平性自动工具很难凭空构造出合适的归纳不变量。操作系统验证里经常遇到这种情况证明“任意时刻只要任务A在等待任务B最终不会一直占用CPU”。这种时序性质超越了简单的不变式依赖排队规则和弱公平性假设通常需要人工设计一个排名函数或者虚拟时钟。自动工具能帮你验证假设和中间步骤但核心归纳步骤还是需要人来定。还有一些硬件层面的问题比如缓存一致性、内存屏障效果这些内容涉及执行语义细节SMT往往只能建模一个小片段无法覆盖全部行为。务实态度是把问题分层操作系统内核的逻辑正确性交给形式化工具硬件保证交给芯片厂商的验证结果两种边界之间用明确的抽象层隔离。写在最后做形式化验证这几年我最大的感受是工具越来越强但“证明”这个动作的瓶颈始终在建模。反例搜索再快证明自动化再猛只要抽象模型没有忠实表达代码的真实行为结果就没有意义。所以我在实际项目里养成了一个习惯每次写完模型第一件事不是去证它是正确的而是改成证一个故意错误的版本。如果工具连错误的版本都能通过那一定是模型和性质翻译出了问题而不是代码真的安全。这种“负向验证”帮我在正式证明之前就排除掉了一大批低级疏漏。这篇里的两个最小实验是在一个很小的抽象层上演示自动工具的用法。后续如果你遇到更复杂的系统调用、内存管理模块办法也是一样的把大系统拆成一层层小模型每一层用Z3搜反例、用定理证明器固定性质再一层层做细化对应。这个过程没有捷径但有了自动证明工具至少那些本该由人一遍遍检查的推导终于可以交给机器去跑了。