2014年4月7日，世界首次知道心脏滴血漏洞。OpenSSL中TLS/DTLS(传输层安全协议)心跳扩展实现上的一个小漏洞，却能使攻击者解开受脆弱OpenSSL软件保护系统中的加密措施。在当时，这些加密措施占据了公网大约2/3的江山。攻击者可以窃听那些看起来加密了的通信，盗取隐私数据，冒充服务和用户。
漏洞一见诸报道，OpenSSL便发布了针对心脏滴血的补丁。即便如此，1年半之后，仍有20多万台设备没有打上补丁。
心脏滴血只是冰山一角
围绕心脏滴血的所有关注(当然还有不必要的心理恐惧)，表明了小小编程失误在当下互联时代会造成多大的破坏。
计算机技术早期，漏洞不过意味着一点点的不便。那个时候，计算机间互不联通，一个编程缺陷最多就是某个软件时不时地故障一下。或许你需要不时重启一下机器，但最多也就是如此了。
但互联网世界中，一切都不一样了。全球连接性让黑客可以瞄准更多的用户。考虑到人们银行凭证和其他敏感数据的激增，在今天，一个漏洞不仅仅意味着不方便这么简单。通常，编程漏洞就是安全漏洞，攻击者可利用来盗取或披露成千上万用户的个人信息。这也就是为什么心脏滴血之类的漏洞会演变成大事件的原因所在。
但也别会错意。我们的软件也不是全部都被攻破了的。OpenSSL的大多数用例仍然运作良好。心脏滴血仅仅构成了少数黑客入侵场景之一，这些场景中，攻击者可以操纵编程缺陷产生软件功能上的非预期结果。
这就是编程的现实。漏洞司空见惯，因为要把自然语言能描述的想法，转换成机器能理解的指令，可不是件容易的事儿。
除此之外，编程的目标，是使计算机程序能够只实现一套既定的操作，不做多余的事。正派程序员都不会希望有人在自己的软件里找到能让他们窃听加密通信或盗取个人信息的漏洞。因此，程序员有责任让自己的代码无懈可击。
但知易行难。稍微学过一点编程的人都会告诉你，编程出错简直太容易了。要是有什么方法，能让程序员确保自己的代码只做应该做的事就好了……
事实证明，还真有这么一种资源。
代码验证好处多
形式化验证是自70年代以来就在用的一种编程风格，通过确保程序符合每个用例，达到甚至超出程序应在某些可能用例情况下可用的最低要求。
程序员为达到这种包容性，往往将自己的代码展开得像是数学证明，每条语句都延续前面语句的逻辑。程序员们写下的，是描述程序行为的数学公式，并用某种形式的验证程序检查语句的正确性。
你正在写下一个数学公式来描述程序的行为，并使用几种验证机制去校验程序运行后所达到状态的正确性。
想进行形式化验证，程序员首先需要写出形式化规约，或者对计算机程序应怎样工作作出解释说明。然后，用这一规约来验证软件是否到达既定目标。
这可不总是毫不费力的过程。在规约和验证规约所需的语句之间，采用形式化验证的程序，最终可能会比不采用验证却在大多数用例中工作良好的程序代码长度的好几倍。
幸运的是，码农们现在可以用编程语言和证明辅助程序之类的工具来验证自己的程序。事实上，正是几十年前此类资源的缺乏，才导致了直到互联网出现的现代，形式化验证才真正可行。
普林斯顿大学计算机科学教授安德鲁·阿佩尔将之阐述为：
科学技术的很多部分，仅仅是不够成熟到能应用的阶段，因此，1980年前后，计算机科学领域很多部分兴趣渐失。
走向应用
安全研究人员一刻也等不及补回失去的时间了。例如，美国国防部高级研究计划局(DARPA)设立的高可靠性网络军事系统(HACMS)计划中，工程师们就着手制作黑不掉的休闲四轴飞行器。他们通过先将飞行器的代码分区，再通过使用“高可靠的构件”重写其软件架构，做到了这一点。其中一个构件就包含了入侵者不能升级权限以访问其他分区的验证。
在其代号“小鸟”的实验中，黑客组成的红队，收到了四轴飞行器摄像头控制分区之一的访问权。他们的任务，就是获取该飞行器基本功能的控制权。但在努力6周之后，他们依然无法进入另一个代码分区。
这一成果吸引了国防部研究人员的注意。HACMS项目经理，塔夫斯大学计算机科学教授卡斯灵·费舍尔说：
他们无论如何也突破不进去，破坏不了其运行。该结果让DARPA瞩目，纷纷惊讶捧脸：“上帝啊，我们可以在担心的系统里实际使用这种技术了！”
发展前景
自“小鸟”开始，DARPA将形式化验证应用到了其他技术，比如自动驾驶汽车和卫星。
他们还给自己设定了一些未来想达到的崇高目标。阿佩尔希望用1000万美元打造完全经验证的端到端系统，比如Web服务器。同时，在微软，工程师们正在创建HTTPS的验证版本，以及无人机之类设备的验证规范。
本文转自d1net（转载）
