赵翔鹏的Blog Xiangpeng's Thinkpad

WinHEC 2008见闻：static code verification

WinHEC是Windows硬件开发者大会。大部分主题都是针对驱动程序开发的。作为一个技术性会议，所有的session都是微软或者赞助商的讲师在讲课，推广微软的新技术；这个跟学术性会议不同。

一个有趣的topic是static verification。微软提供的驱动开发验证器，Prefast和Static Driver Verifier，分别支持单个函数级别的验证和多函数的全局验证。简单的说它们就是两个symbolic model checker。可以验证的性质包括很多条预定义的规则，如“分配了内存就要释放，而且只能释放一次”（仅此一条规则就已经能证明这个工具的价值了），“提升了IRQL后，以后也要降低”，等等。也可以自己用类C语言写规则。

Prefast大概需要几分钟的时间来验证，SDV需要20-40分钟。（speaker说他们努力改进工具，使验证时间从20小时减少到20分钟）WDK自带这两个工具，用起来也很简单，输一条命令就会自动在后台执行验证，验证结束后会弹个提示。

为保证验证的效果，可能还要加上一些annotation：比如标明某个函数foo(char* s, int len)中，s是一个大小为len的buffer，然后就可以验证一些buffer overflow的问题。

虽然model checking的状态爆炸问题还是存在，但好在一般的驱动程序都不太复杂，所以可以说model checking已经进入工业应用阶段了，speaker说希望所有的硬件厂商们都用一下这个工具。我提了个问题，一般的C/C++程序是否可以用这两个工具来验证？回答是“you can try it”。估计小程序还是能跑一跑的。随着内存容量的不断增加，model checking是否会得到更多的应用呢？