认识达内从这里开始

认真做教育专心促就业

代码验证有什么好处？

发布：长沙达内IT培训机构
来源：51CTO
时间：2016-10-14 16:34

形式化验证是自70年代以来就在用的一种编程风格，通过确保程序符合每个用例，达到甚至超出程序应在某些可能用例情况下可用的最低要求。

程序员为达到这种包容性，往往将自己的代码展开得像是数学证明，每条语句都延续前面语句的逻辑。程序员们写下的，是描述程序行为的数学公式，并用某种形式的验证程序检查语句的正确性。

你正在写下一个数学公式来描述程序的行为，并使用几种验证机制去校验程序运行后所达到状态的正确性。

想进行形式化验证，程序员首先需要写出形式化规约，或者对计算机程序应怎样工作作出解释说明。然后，用这一规约来验证软件是否到达既定目标。

达内长沙IT培训要说的是，这可不总是毫不费力的过程。在规约和验证规约所需的语句之间，采用形式化验证的程序，最终可能会比不采用验证却在大多数用例中工作良好的程序代码长度的好几倍。

幸运的是，码农们现在可以用编程语言和证明辅助程序之类的工具来验证自己的程序。事实上，正是几十年前此类资源的缺乏，才导致了直到互联网出现的现代，形式化验证才真正可行。

普林斯顿大学计算机科学教授安德鲁·阿佩尔将之阐述为：科学技术的很多部分，仅仅是不够成熟到能应用的阶段，因此，1980年前后，计算机科学领域很多部分兴趣渐失。

走向应用

安全研究人员一刻也等不及补回失去的时间了。例如，美国国防部高级研究计划局(DARPA)设立的高可靠性网络军事系统(HACMS)计划中，工程师们就着手制作黑不掉的休闲四轴飞行器。他们通过先将飞行器的代码分区，再通过使用“高可靠的构件”重写其软件架构，做到了这一点。其中一个构件就包含了入侵者不能升级权限以访问其他分区的验证。

在其代号“小鸟”的实验中，黑客组成的红队，收到了四轴飞行器摄像头控制分区之一的访问权。他们的任务，就是获取该飞行器基本功能的控制权。但在努力6周之后，他们依然无法进入另一个代码分区。

这一成果吸引了国防部研究人员的注意。HACMS项目经理，塔夫斯大学计算机科学教授卡斯灵·费舍尔说：他们无论如何也突破不进去，破坏不了其运行。该结果让DARPA瞩目，纷纷惊讶：“上帝啊，我们可以在担心的系统里实际使用这种技术了!”

发展前景

自“小鸟”开始，DARPA将形式化验证应用到了其他技术，比如自动驾驶汽车和卫星。

他们还给自己设定了一些未来想达到的崇高目标。阿佩尔希望用1000万美元打造完全经验证的端到端系统，比如Web服务器。同时在微软，工程师们正在创建HTTPS的验证版本，以及无人机之类设备的验证规范。

< 上一篇：如何看待编程漏洞？

下一篇：如何理解“品效合一”？（上） >