2017.W34 - 驗證系統沒有漏洞 - 資安

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

--