安全C語言的設計與實現(xiàn).pdf

1、在社會高度信息化的今天，社會生產生活高度依賴軟件系統(tǒng)，因此軟件系統(tǒng)的安全性與可靠性也就顯得愈加重要，通過形式化驗證的方式保證程序的安全是一種重要的手段。
　　形式化驗證有兩種方法，一種是模型檢測，模型檢測能夠通過遍歷系統(tǒng)所有的狀態(tài)空間，自動驗證有窮狀態(tài)的系統(tǒng)并構造不滿足性質定理的反例。另一種是演繹推理，它使用形式化的方式對程序進行數(shù)學推理，盡管以這種方式實現(xiàn)的自動驗證工具早已有實驗室開發(fā)出來，但是至今都無法在工業(yè)界使用。究其原因在

2、于自動定理證明方面的困難，因為不管是斷言語言描述能力的提升、循環(huán)不變式的推斷、別名判斷和驗證條件的證明等，最終還是受到自動定理證明器能力的影響。鑒于這些原因，在研究自動定理證明的同時，應當適當考慮降低對自動定理證明期待，可以通過設計安全的語言去提高合法程序的門檻，同時設計規(guī)范語言來描述程序代碼的行為性質以降低定理證明器的負擔。
　　本文主要貢獻:
　　第一，設計了一種面向驗證的C語言子集，稱為安全C語言。在基于Hoare邏輯

3、推理規(guī)則對程序進行形式驗證過程中，每當使用賦值公理{Q[E/x]}x=E{Q}(Q是賦值語句的后斷言，Q[E/x]表示對Q中所有x代換為E)時，必須保證后斷言Q與賦值語句x=E中沒有潛在別名，否則Q[E/x]是最弱前斷言的結論不可靠，而C語言廣泛存在的別名，給基于Hoare邏輯的推理帶來難題。本文在基于C99標準之上，從別名的角度討論了C語言的安全性以及其會給程序驗證帶來的問題，并以此為啟示設計了安全C語言，在安全C語言中要求對C語言中

4、各種類型增加編程限制來使得對這些被限制類型的變量操作表現(xiàn)得較為規(guī)范，同時還要求使用標注對程序加以說明以減輕定理證明器負擔。
　　第二，設計了一種規(guī)范語言，規(guī)范語言定義了安全C語言要求的標注的語法語義及使用方式，規(guī)范語言以形式化的方式描述C程序的行為性質，這些對C程序行為性質的描述最終都會傳遞給自動定理證明器，從而更大程度上幫助自動定理證明器認知程序的行為，并最終驗證程序行為是否符合規(guī)范中的描述。在規(guī)范語言中還專門引入形狀描述來表示