CAST:自動化動態軟體驗證工具

Abstract

軟體測試是軟體工程用以確保軟體品質重要的一部分。此外，在程式中自動驗證特性是軟體測試的遠程目標。近年來，結合具體與符號執行( concolic 測試)成為一個眾所周知的方法用來路徑分支測試並且許多研究表明該方法可以結合全域檢查，來找出程式錯誤。在本論文中，我們提出CAST 的規範語言，建立於concolic 測試結合全域檢查的基礎上，可以描述各種規格檢查C 語言程式的安全特性(從另一個角度來看，我們可以將此作為一種駭客攻擊，以獲得接近exploit 的測試資料)。CAST 是一個自動和動態軟體驗證工具，主要包括樣式匹配，全域檢查和資料流分析，所以可以使我們的全域檢查比一般的concolic 測試的更加靈活和複雜。

Software testing is an essential part of software engineering for ensuring software quality. Furthermore, automatically verifying properties in programs is a long-time goal in software testing. In recent years, combining concrete and symbolic execution (concolic testing) becomes a well-known approach for branch testing and many researches indicate that the approach can combine with universal checks to find bugs. In this paper, we present the CAST specification language which can describe various kinds of specification for checking security properties of C programs (from another point of view, we can take this as a hack attack to attain test cases close to exploit) based on concolic testing with universal checks. CAST, an automatic and dynamic software verification tool, is mainly composed of pattern matching, universal check and data flow analysis such that we can make universal checks more flexible and complex than that general concolic testing uses.