基于模型檢查的系統(tǒng)程序的可靠性與安全性驗證.pdf

1、軟件復(fù)雜度呈指數(shù)上升，BUG數(shù)量的不斷增多，人工測試已經(jīng)不堪重負(fù)。理論界專家紛紛指出，模型檢查(Model Checking)將會成會未來的趨勢。
　　 本文選用了兩款各有針對性的模型檢查工具：CBMC和MOPS，互為補充，對網(wǎng)絡(luò)應(yīng)用中大量使用的OpenSSH系統(tǒng)進行檢查，利用兩款工具的不同特點，對各自產(chǎn)生的檢查結(jié)果相互校驗，并對驗證結(jié)果進行了一致性證明。
　　 CBMC是一個針對ANSI-C和C++的模型檢查器，它擅長

2、用來檢查程序的可靠性：諸如檢查數(shù)組邊界、緩存溢出、指針安全等程序性質(zhì)，同時它也允許使用自定義的斷言來對程序進行建模驗證。
　　 MOPS是一個被設(shè)計用來查找C程序中安全性BUG的模型檢查器。它可以用來驗證程序是否滿足時序安全性質(zhì)。時序安全性質(zhì)是指一組操作是否按照要求的先后順序執(zhí)行，這在程序的安全性特點中尤其重要。
　　 OpenSSH是一款免費的加密工具軟件，它對包括密碼在內(nèi)的所有數(shù)據(jù)流量進行加密，有效的防御了偵聽、連接