这学期OS的课程挑战性实验，我尝试着对清华祖传教学OS uCore进行验证。按照验证的传统，这个项目被命名为CertiCore。但最后的结果是，我们只完成了对uCore物理页面分配器的验证。我想从某种意义上说，这次尝试算是失败了，不过既不是一败涂地，也不是功败垂成。细细想来，最主要的原因还是我们对OS验证的经验不足。我们并没有太多开发OS的经历，也许甚至搞不清楚OS的典型性质。我们对OS验证的经验，只有几篇论文而已。
验证技术是否已经变成了一种阳春白雪呢？经历这次尝试，我的最大感受是，如果你没有验证的经验，那么即使有完备的逻辑和形式理论基础也很难推进。即便是符号执行这样最为基础，最为自动化的验证方式，对刚接触的人来说一样深奥难懂。
当我们学期初阅读Serval的论文时，以为其中两周验证CertiKOS的例子确凿无疑，而且认为我们也能很快地完成uCore的验证。但事实是，你需要大量的经验，对工具的极度熟悉，才能快速地完成系统的验证。
这种必需的经验就是领域专用知识，一种独属于某个领域的约定与直觉。毫无疑问，Serval并不是给普罗大众，而是OS验证专家准备的。它提高的是精通验证者的效率，而不是OS开发者的效率。其中充斥着大量工程实践固化下的概念，如果你没有经验，就必须去读Serval的源码，而且不一定能读懂；至于论文，它只会介绍基本原理。嗯，非常象牙塔，非常学术范。
当然，除此之外Serval本身也有不少缺陷。作为一个基于Rosette的库，自然而然地，必须同时忍受Rosette带来的好处与坏处——糟糕的调试环境，为了支持符号执行而不显式处理异常，以及Lisp风格带来的不变。另外，没有文档也是一个大问题。
不过Serval的确提供了它宣称的验证方便性。只可惜这学期的大量开发精力，实际上都投入到了环境搭建和工具调整上。要说实际的验证工作，其实也就五百来行不够精炼的代码。一个页面分配器，现在看来不过几个接口，算法也不算复杂，却耗费了三个人月的时间。回忆开发过程，大部分时间都是在debug，让我感觉不是在开发验证系统，而是在和软件工程失败产物做斗争。
工具的不易用和经验的不足（也许还有懒惰），使得开发举步维艰。这个过程中最大的障碍，我们也许知道最后一刻才弄懂，那就是验证系统的边界——什么是可以被验证的，而什么是无法被验证的？我们对验证如此缺乏经验，以至于定下了验证uCore宏内核的目标。即使这个内核如此微小，其复杂度却依然远远超越了现有的大部分验证内核。我们寄希望于用符号执行的方法细粒度验证页面分配算法，从而在其上耗费了过多的时间。
这些教训都让我想到，也许验证一个系统最关键的不在于逻辑或者形式化理论，而是对被验证系统的认知和理解，从而能够清楚地选择验证的目标，使其契合使用的验证工具的表达力。系统验证本身如此，开发验证工具也是如此。没有目标，没有深思熟虑的验证是难以为继的。
