完美的无漏洞软件？形式化验证

肿档哎锅

都说是软件就有漏洞。真的这样吗？
网上无意中看见了一个东西叫形式化验证（Formal Verification）。据称能写出绝对没有漏洞的代码。大家来讨论讨论。

软件开发中一般使用“测试”来找bug，这种方法只能找到bug，不能证明程序没有bug。
形式化验证是用逻辑来验证程序的可靠性，就是把一段程序用逻辑的方法证明一遍，证明它能得到预期的结果，没有bug。一般这类研究主要应用于昂贵的航天器材的操作系统、危险的医疗设备的程序之中。因为航天器材、医疗设备牵扯到人的生命，如果操作系统出现错误，那么很危险，又不能用测试一遍一遍的测，所以用形式化验证来做。比如美国航天局NASA就会雇佣大批形式化验证的专家来验证他们操作系统的正确性。
学习这个方向，最好有比较好的逻辑知识（数理逻辑、拉姆达验算），最好比较了解程序（比如操作系统的设计、编译器的设计等）。
这个方向是比较犀利的研究方向，但不大容易出论文，需要长时间积累才能发一篇好论文。

王健：说说形式化验证（Formal Verification）
http://chainb.com/?P=Cont&id=1957

说形式化验证（Formal Verification）之前，就不能不提一下形式化方法（Formal Method）。形式化方法简单的说就是用数学工具进行定义、开发和验证（specification, development and verification）。数学家们认为，不论硬件还是软件工程，就像世间万物一样，所有的学问一样，归根结底是数学问题。“一个不懂数学的工程师不是一个好工程师”。如果所有的设计开发都能够按照严格的数学方法进行，那么开发出来的系统就会像数学本身一样的完美：软件不会出错，硬件永远正常。当然，这是数学家的理想。

ccboxes

一些人都在说什么东西。。。。。。。。。

形式化验证不是空想，是实实在在、并应用了很多年的技术，的确能写出无已知BUG、漏洞的程序。近四十年来，大型银行、军事设施、卫星的软件系统、超大规模集成电路设计图等都是依靠形式化验证保证其正确性。

问题在于：

1.形式化验证只能验证无已知BUG，一个通过无堆栈溢出形式化验证的软件绝不会出现堆栈溢出，但有可能会出现其他BUG。

2.形式化验证的复杂度随着软件规模的扩大指数上升，对于Windows这种规模的软件，进行形式化验证所需要的时间与金钱都极为庞大。

3.一旦代码/设计出现改动，就要重新进行验证，大大降低开发速度。

所以形式化验证目前只在会为错误付出极大代价的项目中使用。

zhousulin5

就一个根号2，有哪个天才能造出一台电脑计算出它的最精确结果？如果你说你的电脑能计算到小数点后万亿位，我只想要看到它再多计算一位。
有无穷，就不能存在完美。

肿档哎锅

zhousulin5 发表于 2018-12-4 15:43
就一个根号2，有哪个天才能造出一台电脑计算出它的最精确结果？如果你说你的电脑能计算到小数点后万亿位， ...

我想这个还是容易解决的。想要看任意多位，只要有任意多的时间即可。

HEMM

就和它的名字一样，停留在形式化

肿档哎锅

HEMM 发表于 2018-12-4 16:41
就和它的名字一样，停留在形式化

这是不对的。NASA，神舟等系统核心代码都用了这种方法。

kxmp

人们的理想一般都是些臆想.谁知道数学本身有没有什么漏洞

肿档哎锅

ccboxes 发表于 2018-12-4 17:41
一些人都在说什么东西。。。。。。。。。

形式化验证不是空想，是实实在在、并应用了很多年的技术，的确 ...

感谢大佬解答

肿档哎锅

kxmp 发表于 2018-12-4 17:47
人们的理想一般都是些臆想.谁知道数学本身有没有什么漏洞

也许有，但目前为止还没人能想到。既然人不能想到，人也就找不到漏洞了。

HEMM

肿档哎锅 发表于 2018-12-4 17:05
这是不对的。NASA，神舟等系统核心代码都用了这种方法。

如果所有的设计开发都能够按照严格的数学方法进行，那么开发出来的系统就会像数学本身一样的完美：软件不会出错，硬件永远正常。当然，这是数学家的理想。

追求完美没错，但不可能有完美，不可能无BUG......
绝对不会有已知BUG就等于没BUG，那么无话可说。