[發明專利]針對運行已驗證軟件的硬件的端到端安全性

在審

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

背景技術

當用戶向遠程服務(例如，基于云的服務)提交個人數據時，不能保證個人數據將保持安全，或者甚至不能保證該服務將產生正確的結果。最多，服務可以具有隱私策略并且在數據泄露的情況下限制服務的責任。然而，最近的標題已經提供了操作系統、庫或應用(例如，軟件應用)的脆弱性如何使得個人數據能夠被訪問的示例。

發明內容

提供本發明內容以便以簡化的形式介紹將在以下具體實施方式中進一步描述的一些概念。本發明內容不旨在標識所要求保護的主題的關鍵或必要特征；也不用于確定或限制所要求保護的主題的范圍。

已驗證軟件系統可以在安全硬件(例如，可信硬件)上執行。在被執行之前，軟件系統的屬性可以被驗證為符合軟件規范。證明軟件系統的身份的第一憑證可以被發送給外部應用。由安全硬件的提供方(例如，制造商)簽名的第二憑證可以被發送給外部應用。第二憑證可以證明安全硬件的身份。以這種方式，可以在低級(例如，匯編語言級)驗證作為整體的系統(例如，完整軟件棧)，并且然后將其引導到安全硬件并由安全硬件執行以提供安全系統。第一憑證和第二憑證可以使得外部應用能夠以如下方式與軟件系統的軟件應用通信：發送給軟件應用或從軟件應用接收的消息被加密并且可以由外部應用和軟件應用解密，但是不能由其他實體解密或修改。

附圖說明

參考附圖描述詳細描述。在附圖中，附圖標記的一個或多個最左邊的數字標識附圖標記首次出現的附圖。不同附圖中的相同的附圖標記指示相似或相同的項目。

圖1是根據一些實現的包括規范翻譯器的說明性架構。

圖2是根據一些實現的包括應用的說明性架構。

圖3是根據一些實現的包括可信增量(TrInc)應用的說明性架構。

圖4是根據一些實現的包括已驗證軟件棧(例如，系統)的說明性架構。

圖5是根據一些實現的在安全硬件上執行的已驗證軟件的說明性架構。

圖6是根據一些實現的包括離線和運行時的說明性架構。

圖7是根據一些實現的包括從軟件應用接收公鑰的示例過程的流程圖。

圖8是根據一些實現的包括執行已經被驗證為符合軟件規范的軟件系統的示例過程的流程圖。

圖9是根據一些實現的包括執行軟件系統的已驗證引導的示例過程的流程圖。

圖10是包括已驗證軟件系統的說明性架構。

具體實施方式

服務的軟件代碼的正式驗證可以提供服務與正式規定的安全標準精確匹配的數學保證。遺憾的是，盡管軟件驗證可以提供關于軟件代碼的可信賴性的有力保證，但是計算成本可能如此高，以至于服務提供方可能無法執行其整個系統的軟件驗證。因此，服務提供方最多可以提供關于被大量未驗證軟件代碼包圍的、用高級語言編寫的小程序的有力保證。例如，已驗證傳輸層安全協議實現可以依賴于未驗證操作系統和未驗證軟件庫。作為另一示例，針對公鑰加密系統(例如，RSA或類似系統)的機器檢查的正確性證明可以假定實現公鑰加密系統、對應運行時庫和操作系統的加密庫的正確性。作為另一示例，依賴于可信匯編代碼的微內核可以不對應用級語義的正確性進行聲明。因此，服務可能不能執行服務的軟件代碼的完整形式驗證，并且因此可能不能提供服務與正式規定的安全標準精確匹配的數學保證。

本文中所描述的系統和技術可以用于執行已經被驗證為端到端安全的應用，使得驗證能夠覆蓋可以被執行的所有軟件代碼(“代碼”)，例如，已驗證代碼不僅包括應用，還包括操作系統、庫(運行時庫、程序庫、動態庫)和可以執行的驅動器。因此，在一些情況下，不需要假定在一個或多個服務器上執行的軟件的任何部分是正確的。經歷驗證的代碼是被執行的匯編代碼，而不是可以編寫代碼的一個或多個任何高級語言。驗證過程可以假定硬件是正確的，但不對編譯器的正確性或代碼的運行時執行進行假定。驗證過程因此可以證明(demonstrate)整個系統實現代碼的高級抽象狀態機的功能正確版本。驗證過程可以證明安全遠程等效性，例如，遠程用戶可以建立到其輸出不能與高級抽象狀態機的輸出區分開的代碼的安全通道。