[發明專利]軟件系統的自動驗證

有效

• 申請號: 201580053927.4
• 申請日: 2015-10-01
• 公開（公告）號: CN107111713B
• 公開（公告）日: 2020-02-07
• 發明（設計）人: C·霍布利澤爾;B·帕諾;J·R·洛奇;J·R·豪厄爾;B·D·齊爾
• 申請（專利權）人: 微軟技術許可有限責任公司
• 主分類號: G06F21/52
• 分類號: G06F21/52
• 代理公司: 11256 北京市金杜律師事務所
• 代理人: 王茂華;丁君軍

1.一種計算機實現的方法，包括：

接收以高級語言編寫的軟件代碼，所述軟件代碼包括多個組件，所述多個組件包括操作系統和至少一個應用；

編譯所述軟件代碼以創建與所述軟件代碼相對應的匯編語言代碼；

接收高級規范，所述高級規范指定由所述軟件代碼執行的一個或多個功能；

至少部分地基于所述高級規范，生成低級規范；

驗證所述匯編語言代碼的輸出不支持秘密數據被確定，所述秘密數據包括一個或多個私鑰；

驗證所述匯編語言代碼根據所述低級規范表現以執行由所述高級規范制定的所述一個或多個功能；以及

提供所述匯編語言已經被驗證執行所述一個或多個功能的指示。

2.根據權利要求1所述的計算機實現的方法，還包括：

驗證所述多個組件中的第一組件不能夠破壞所述多個組件中的第二組件。

3.根據權利要求1所述的計算機實現的方法，還包括：

驗證所述多個組件中的個體組件與所述低級規范中的相應的狀態機之間的等效。

4.根據權利要求1所述的計算機實現的方法，其中：

所述高級規范包括：

前置條件、后置條件或終止度量中的至少一項；以及

標識與所述軟件代碼相關聯的狀態的一個或多個斷定；并且

所述計算機實現的方法還包括：

驗證所述一個或多個斷定的有效性。

5.根據權利要求1所述的計算機實現的方法，其中：

所述軟件代碼包括關于所述軟件代碼所進入的多個狀態的斷定。

6.根據權利要求5所述的計算機實現的方法，其中驗證所述匯編語言代碼執行所述一個或多個功能包括：

證明關于所述軟件代碼所進入的所述多個狀態的所述斷定對于所有可能的輸入是有效的。

7.根據權利要求1所述的計算機實現的方法，其中：

所述高級規范包括指定由所述軟件代碼使用的特征子集的慣用規范。

8.根據權利要求1所述的計算機實現的方法，還包括：

優化所述匯編語言代碼，所述匯編語言代碼使用中間驗證語言來描述證明義務；

由驗證引擎至少部分地基于所述匯編語言代碼，生成與所述證明義務相對應的一個或多個驗證條件；以及

由推理引擎驗證所述證明義務。

9.一種計算設備，包括：

一個或多個處理器；以及

一個或多個存儲器存儲設備，其存儲由所述一個或多個處理器可執行用于執行操作的指令，所述操作包括：

接收以高級語言編寫的軟件代碼，所述軟件代碼包括多個組件；

編譯所述軟件代碼以創建與所述軟件代碼相對應的匯編語言代碼；

接收高級規范，所述高級規范指定由所述軟件代碼執行的一個或多個功能；

至少部分地基于所述高級規范，生成低級規范；

驗證所述匯編語言代碼的輸出阻止秘密數據被確定，所述秘密數據包括一個或多個私鑰；

驗證所述匯編語言代碼根據所述低級規范表現以執行由所述高級規范制定的所述一個或多個功能；以及

提供所述匯編語言已經被驗證執行所述一個或多個功能的指示。

10.根據權利要求9所述的計算設備，其中所述操作還包括：

接收所述軟件代碼的行；以及

針對所述高級規范驗證所述軟件代碼的所述行。

11.根據權利要求9所述的計算設備，其中所述操作還包括：

接收執行所述一個或多個功能中的至少一個功能的所述軟件代碼的行；

確定所述軟件代碼的所述行未能執行所述至少一個功能；以及

顯示錯誤消息，所述高級規范的失敗的前置條件在所述錯誤消息中被突出顯示。