安全C語言程序驗證器中驗證條件生成器的擴展設計與實現(xiàn).pdf

1、交通、電力、軍事等關鍵領域對軟件的可靠性和安全性要求越來越高，因為其嚴重關乎國民的人身和財產安全。C語言在上述基礎領域軟件的開發(fā)中有廣泛的應用。C語言靈活高效的特性允許程序員做相當?shù)讓拥牟僮?，但也導致C程序容易出現(xiàn)非法指針解引用、內存泄漏、緩沖區(qū)溢出等缺陷。
　　形式化驗證是一種可以嚴格保證程序可靠性的方法。本課題組正在研發(fā)一個安全C語言驗證器，其功能是對攜有程序標注的安全C語言程序進行演繹推理，驗證程序是否滿足預期規(guī)范。

2、　　安全C語言驗證器中驗證條件生成器的作用是支持安全C語言和規(guī)范語言SCSL的語法，實現(xiàn)每條語句的演算規(guī)則，并根據(jù)演算規(guī)則遍歷源程序進行演算，同時產生程序點的斷言和合理有效的驗證條件。本文的工作是對安全C語言驗證器中的驗證條件生成器進行擴展。
　　本文的主要工作和貢獻如下:
　　第一、參與規(guī)范語言SCSL中邏輯變量、幽靈代碼、字符串類型、帶命名行為協(xié)議和多函數(shù)協(xié)議的設計，提高了規(guī)范語言的表達能力，同時獨立設計和實現(xiàn)了對應的演

3、算規(guī)則。
　　第二、基于Hoare邏輯設計和實現(xiàn)跳轉語句goto、continue和break、選擇語句switch以及函數(shù)調用語句的演算規(guī)則，使得驗證器可以支持更多C的語法和控制結構，擴大了驗證器的適用范圍。同時實現(xiàn)了賦值語句前對全稱量化斷言和謂詞的展開，減輕了自動定理證明器的負擔。
　　第三、根據(jù)C語言的語義提出了一種適用于程序驗證的棧區(qū)內存模型，可以支持結構體和多級指針等數(shù)據(jù)類型，并基于該模型實現(xiàn)了取地址、多級解引用和