软件复杂度呈指数上升,BUG数量的不断增多,人工测试已经不堪重负。理论界专家纷纷指出,模型检查（ModelChecking）将会成会未来的趋势。本文选用了两款各有针对性的模型检查工具CBMC和MOPS,互为补充,对网络应用中大量使用的OpenSSH系统进行检查,利用两款工具的不同特点,对各自产生的检查结果相互校验,并对验证结果进行了一致性证明。CBMC是一个针对ANSI-C和C++的模型检查器,它擅长用来检查程序的可靠性：诸如检查数组边界、缓存溢出、指针安全等程序性质,同时它也允许使用自定义的断言来对程序进行建模验证。MOPS是一个被设计用来查找C程序中安全性BUG的模型检查器。它可以用来验证程序是否满足时序安全性质。时序安全性质是指一组操作是否按照要求的先后顺序执行,这在程序的安全性特点中尤其重要。OpenSSH是一款免费的加密工具软件,它对包括密码在内的所有数据流量进行加密,有效的防御了侦听、连接截取和其他网络级的攻击。在OpenSSH系统中存在的可靠性或安全性BUG很可能导致重大的损失,所以本文以此软件作为实验的对象。本文首先使用两款软件分别对验证对象进行检查,对产生的有效BUG使用另一个软件进行针对性建模进行复查。最后使用形式化方法证明了检查结果的一致性。
本文来源: https://www.lw50.cn/article/2a0a040c022d985463c428d4.html