在黑客眼里，理论上应该没有不可破解的代码。然而IT之家了解到美国国防部高级研究计划署（DARPA）试图打破这个规矩，利用“形式化验证”技术进行代码编写，让程序无法被攻破。

现有大部分程序代码都是非形式化的，对其可用性的评估主要基于它是否能工作，而安全性并非最主要考量。形式化验证代码读起来就像是数学证明，整个程序的测试具有与数学家作证明题同等的确定性，因此攻击者很难找到破绽。

DARPA的工程师对这种编程技术进行了验证，花费了六周时间也没能攻破验证目标系统的防御。现在DARPA准备将这项技术应用于更多领域，以应对各领域网络上的各种攻击。如果该技术得带推广，可能会给整个行业造成不小影响。