C程序證明策略在Coq中的設計和實現(xiàn).pdf

1、計算機系統(tǒng)已在國防、通訊、金融、能源、交通、醫(yī)療等關鍵領域中得到廣泛應用，構建高可信系統(tǒng)已成為世界范圍的重要課題。其中操作系統(tǒng)內核的安全可靠性是構建高可信計算機系統(tǒng)的關鍵，任何一個微小的內核錯誤都有可能導致整個計算機系統(tǒng)崩潰。形式化程序驗證是使用邏輯推理系統(tǒng)來保證計算機程序的正確性，對于規(guī)模相對較小而設計復雜的內核程序而言，它是保證其安全可靠的有效方法之一。底層的系統(tǒng)軟件大都采用C語言編寫，而C程序中的指針操作和系統(tǒng)軟件中數(shù)據(jù)結構間復雜

2、的邏輯關系，使得驗證系統(tǒng)軟件的程序邏輯的斷言語言需要具有足夠的表達能力。然而，具有足夠表達力的斷言語言推理的不可判定性導致推理驗證的過程無法完全自動化，而手動驗證系統(tǒng)軟件需要耗費大量的人力和物力。因此，如何在不犧牲邏輯斷言的表達力的前提下，盡可能的提高C程序的驗證效率是一個亟待解決的問題。
　　本文通過開發(fā)證明策略來提高C程序在定理證明工具Coq中的驗證效率。由于人工交互的手動證明在驗證復雜系統(tǒng)軟件中不可避免，因此在提供自動化支持

3、的過程中同時需要兼顧以下兩個方面:一方面，需要盡可能的減少手動證明的工作量;另一方面，當證明策略失敗時，能夠產生對用戶有用的出錯提示信息，這樣用戶可以根據(jù)提示信息快速地定位問題所在，或者手動證明那些無法自動證明的命題，或者通過調整規(guī)范或代碼來完成證明。基于上述考慮，本文開發(fā)了一組C程序的實用證明策略，包括自動證明分離邏輯斷言之間蘊含關系的證明策略和自動產生驗證條件并證明Hoare三元組的證明策略，它們同時兼顧驗證效率和易用性。
　

4、　本研究主要內容包括：⑴將數(shù)據(jù)結構形狀相關的領域專用知識（譬如單鏈表）引入到證明策略的實現(xiàn)中，并對相關歸納謂詞做自動展開來減少手動證明的工作量，從而提高C程序的驗證效率。⑵通過在證明策略中引入預處理階段來反饋出錯提示信息幫助用戶定位自動證明失敗的問題所在，這在進行人工交互式證明時極大地提高了證明策略的可用性和易用性。⑶根據(jù)上述兩個想法在定理證明工具Coq中實現(xiàn)了一組C程序證明策略（約一萬行Coq代碼），它們能用于全自動的驗證一些簡單的操