《針對安全關鍵系統的多語言編程形式化驗證》是依託清華大學，由董淵擔任項目負責人的面上項目。
基本介紹
- 中文名：針對安全關鍵系統的多語言編程形式化驗證
- 依託單位：清華大學
- 項目負責人：董淵
- 項目類別：面上項目
項目摘要,結題摘要,
項目摘要
航空等領域中對安全關鍵軟體的形式化驗證有著迫切的需求，尤其關注存儲安全性和正確性等特性。現實中的安全關鍵軟體通常都採用多種語言共同實現，多語言編程使用非常普遍，而多語言接口部分常常是錯誤高發地帶，而且也是目前研究的薄弱環節。為此，本項目以安全關鍵軟體系統的完整形式化驗證為遠期目標，著重研究C語言與彙編語言這種具有代表性的多語言編程接口的形式化建模，以此為基礎探索多語言編程的驗證方法，並以廣泛套用的開源嵌入實時作業系統為目標，開展原型系統驗證研究。本項目將給出一種考慮多語言編程特徵的程式建模和驗證方法，解決其關鍵問題，為安全關鍵軟體的構造提供技術支持。
結題摘要
航空等領域中對安全關鍵軟體的形式化驗證有著迫切的需求，尤其關注存儲安全性和正確性等特性。本項目以安全關鍵軟體系統的完整形式化驗證為遠期目標，著重研究C 語言與彙編語言這種具有代表性的多語言編程接口的形式化建模，以此為基礎探索多語言編程的驗證方法，並以廣泛套用的開源嵌入實時作業系統為目標，開展原型系統驗證研究。本項目在彙編代碼語義模型建模、出具證明編譯器（certifying compiler）的設計與實現，以及出具證明編譯器與驗證彙編代碼的結合驗證等方面，已進行大量研究工作，本項目已經初步給出一種考慮多語言編程特徵的程式建模和驗證方法，為安全關鍵軟體的構造提供技術支持，基本完成了預期的研究目標。在彙編語言的機器模型建模方面，本課題採用了驗證彙編代碼（certified assembly code）的方式，設計了基於x86指令集的一個抽象機器模型，該模型基於已有的工作CAP，且進一步考慮了對作業系統代碼中出現的特定語義的支持；本課題設計並實現了一個出具證明的編譯器PLCC，該編譯器接受C的一個較大子集，生成驗證機器代碼，PLCC能夠自動將標註在原始碼層級的斷言自動翻譯到目標代碼層並進行證明（基於PLCC編譯器的一個變種已用於中國科學技術大學軟體學院編譯器課程的教學實踐）；本項目設計並實現了出具證明編譯器生成代碼與手工構造的驗證彙編代碼聯合驗證的框架，在該框架中，自動生成的代碼能夠和手工代碼及證明庫進行聯合驗證和連結；本項目開始研究C/C++語言與JAVA接口的建模與描述，並著手構建工具原型，為多語言系統的安全性聯合驗證奠定了基礎。
