2017.W34 - 验证系统没有漏洞
> 作者外出取材 趁洗衣服的空档发文
## 前言 ##
证明系统存在漏洞 是一件简单的事情
只要存在一个漏洞 就代表系统存在安全性上的疑虑
证明一个系统没有安全上的漏洞 是困难的问题
用任何的工具扫描之后 依然无法证明系统是安全的
## 内容 ##
一开始是看到 jserv[0] 发的文章[1] 提到利用形式化验证[2]来证明系统的安全
概念是将程式转换成一连串的数学公式 最后再用数学证明系统的安全性
在这篇文章中提到了若干潜在的安全性问题
像是 FDIV Bug[3] 造成只有在少数状况的浮点数运算 才存在的 bug
但对于不少需要精准度的程式来说 这种 bug 是难以侦错的议题
在工作中 可能会被要求设计一个高安全系统 像是不存在 SQL Injection 的论坛
但是设计过类似系统的人或许都知道 如果自行攥写相关逻辑
除非设计一个十分严苛的规则 否则很难做到适当的 SQL Injection 过滤
形式化验证就是除了测试 (Testing)、模拟 (Simulation) 之外的一种验证方式
前面两种都是利用列举的方式 试图找到系统中脆弱的一环
而形式化验证则是将系统转换成 (isomorphism) 成一连串数学公式
借由验证这些数学公式的正确性 证明系统不存在对应的缺陷
[0]: http://wiki.csie.ncku.edu.tw/User/jserv
[1]: https://hackmd.io/s/H1xxp3pF0
[2]: https://zh.wikipedia.org/zh-hant/形式验证
[3]: https://en.wikipedia.org/wiki/Pentium_FDIV_bug