[閒聊] 2017.W34 - 驗證系統沒有漏洞

看板NetSecurity (資安資訊安全)作者CMJ0121 (不要偷 Q)時間7年前 (2017/08/22 19:39)推噓2(2推 0噓 0→)

留言2則, 2人參與討論串1/1

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 -- ※ 發信站: 批踢踢實業坊(ptt.cc), 來自: 220.157.244.173 ※ 文章網址: https://www.ptt.cc/bbs/NetSecurity/M.1503401960.A.82A.html