[發明專利]一種匯編程序的形式驗證框架

在審

• 申請號: 201410591523.8
• 申請日: 2014-10-30
• 公開（公告）號: CN105630568A
• 公開（公告）日: 2016-06-01
• 發明（設計）人: 陳偉男
• 申請（專利權）人: 鎮江華揚信息科技有限公司
• 主分類號: G06F9/45
• 分類號: G06F9/45
• 代理公司: 暫無信息
• 代理人: 暫無信息

技術領域

一種匯編程序的形式驗證框架主要涉及計算機語言方面領域。

背景技術

隨著國家和社會對軟件的依賴程度日益增長，關鍵軟件的高可信性質顯得越來越重要，其中安全性(包括可靠安全性和保密安全性)是關注的重點。可靠安全性是指軟件運行時不引起危險、災難的能力，而保密安全性是指軟件系統對數據和信息提供保密性、完整性、可用性、真實性保障的能力。本文所，講的安全性主要是指可靠安全性．但是兩者也是緊密相連的，提高可靠安全性有助于保證保密安全性。

提高軟件安全性的目標是所有的程序錯誤在程序運行前被發現或者在程序運行時被溫和地捕獲，以保證程序不會導致不可預測的系統行為。而軟件安全性研究主要是探索如何建立一個管理安全性的健全的科學和技術基礎，其中軟件滿足安全策略的程序性質證明方法是研究的熱點之一。

分析當前研究現狀，程序性質證明采用類型方法和邏輯方法相結合方式可以兼得兩種方法的長處．而ATS的類型系統過于復雜，以致普通程序員難以掌握；CAP方式的驗證需要程序員進行繁復的匯編程序手工證明，不適合用于大規模開發。

因此，我們選擇采用一個簡單的類型系統結合一個自動的邏輯推理系統的方法來證明程序滿足安全策略．對那些有高安全要求的關鍵軟件、程序設計及安全性證明可以在一種新的編程和編譯框架下進行。

該框架包括斷言與規范語言、合式公式、推理規則和可靠性定理．此外，本文還將介紹一個匯編語言指針邏輯系統，它保證通過驗證的程序不存在懸空指針引用，或對動態分配存儲的訪問越界等．部分內容限于篇幅只做簡要敘述。

發明內容

通過國家專利檢索沒有發現關于此系統方面的申請資料。

該框架主要包括斷言與規范語言、合式公式、推理規則和可靠性證明。在目標機器TM上對程序進行Hoare風格的推理，程序員首先要使用斷言與規范語言對代碼堆(程序)進行標注，然后使用合適的推理規則進行程序良形性(well-formedness)的定理證明。

1)斷言與規范語言。斷言語言直接使用元邏輯。斷言的類型是State—State—Prop，即斷言是以兩個狀態為參數的謂詞．它們分別是所在函數的初始狀態和當前狀態．使用函數初始狀態便于表達函數返回值和參數初值之間的聯系，也便于表達匯編程序的一些特定性質．例如在一個函數運行時，當前活動記錄中保存的返回地址和上一個活動記錄的基地址都沒有被修改，其他活動記錄的內容也沒有被修改等．元邏輯中的Prop在此沒有被進一步描述，這是為了便于定制不同的邏輯，使該驗證框架能被用于不同場合。

函數規范中的P和q分別對應函數前后條件。指令塊規范只需要前條件P，而省略了后條件，這是因為可以使用后繼指令塊的前條件來進行推理(一個指令塊的后斷言應該蘊涵它后繼指令塊的前斷言)。

使用斷言與規范語言對代碼堆的每個指令塊、函數進行標注，即定義代碼堆規范環境寥和函數規范環境三。由于一個函數滿足規范的證明和被調用函數的規范有關，三同時也包含被調函數的規范。

斷青和規范的語法如下：

(CdHpSpecCntxt)Ψ∷={f->l->a};

(FunSpecntxt)∑∷={f->b};

(Assertion)p,q∈State->State->Prop;

(CmdSpec)a∷=p;

(FunSpec)b∷=(p,q)。

2)合式公式．它本質上和Hoare邏輯的合式公式是一致的．斷言加到代碼塊、函數和程序上，形成5個層次的合式公式：合式代碼塊、合式函數體、合式函數、合式代碼堆和合式程序，下面使用這些合式公式來定義推理規則:

(Well-formedInstrBlock)Ψ(f);∑|-{a}I;

(Well-formedFuncBody)Ψ(f);∑|-C(f):Ψ(f);

(Well-formedFunction)Ψ(f);∑|-{(p,q)}C(f);

(Well-formedCodeHeap)Ψ;∑|-C:∑;

(Well-formedProgram)Ψ;∑|-{a}P。

3)推理規則。一個程序(C，S，(F,I)是合式的(規則PROG)，僅當存在規范環境Ψ和∑，使得代碼堆C是合式代碼堆，a在當前狀態S下為真，并且I是合式指令塊。