安全C語(yǔ)言的設(shè)計(jì)與實(shí)現(xiàn).pdf

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

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

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

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