深度 | 无法找到“黑点”的代码，连顶级黑客也束手无策
发布时间：2016-10-09 02:45:16 所属栏目：安全 来源：雷锋网
导读：副标题#e# 编者按：一直以来，我们都理所当然地认为程序就像高墙，无法不透风，自然也无法躲过黑客无孔不入的攻击。而这篇首发于quantamagazine 的文章却要颠覆我们的认知了：采用形式验证(formal verification)编写的软件，代码就像“数学证明一样可靠”。
|
然而这个形式规范却有一个漏洞：这个程序员默认输出会是输入的排序结果，即假设列表为 [7, 3, 5]，这个程序应该返回 [3, 5, 7]，这样就满足了定义。但列表 [1, 2] 也满足定义，因为“这是一个排序好了的列表，只不过可能不是我们希望的那种排序好了的列表。” （编辑：淮北站长网） 【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容! |
