基于行為等價的遠程程序執行認證

摘要：遠程程序執行的認證是可信計算的重要內容之一，文獻中所提出的眾多框架大體上分為，基于軟件，或基于硬件。初步地提出了一種遠程程序執行的認證框架（命名為Spirit），Spirit綜合地使用了程序分析、信任鏈、互模擬技術和TPM。

關鍵詞：認證； TPM； 程序分析； 信任鏈

中圖分類號：TP393 文獻標識碼：A文章編號：2095-2163（2013）02-0077-03

0引言

在計算機領域學術發展過程中，計算機安全問題始終是其學術界直面并在不懈攻關的挑戰之一。由可信組織開發和推廣的可信計算技術[1]就是要通過硬件或軟件的合理運用使得計算系統能夠按照預定方式正常運行。在可信計算技術中，遠程認證技術就是一種典型技術。該技術可以確保授權方能及時獲知用戶的計算機系統被改變現象的發生。因而，可以將遠程認證技術應用到檢測遠程程序的運行是否正確，以及驗證是否存在被攻擊方改動運行的程序。舉例來說，在SETI@Home[2]項目中，如何保證客戶端運行的程序未被施加改動是確保得到正確計算結果的前提條件。

本文在分析和借鑒相關研究工作的基礎上，提出了一個新型的遠程程序運行的認證框架Spirit。該框架主旨清晰，程序的運行行為是由其跡確定的，即借助可信計算的TPM技術，服務器通過跡等價來對遠程程序運行的語義正確性完成認證。

本文的組織結構如下：第1部分總結相關工作，第2部分闡述相關的概念和框架細節。第3部分總結。

1相關工作

文獻[3]提出了一種在不可信遺留平臺上運用程序執行遠程認證框架的技術，該框架通過可擴展、OS透明、且安全的方式收集客戶端程序的運行信息，并且再將這些信息以輕量級，風險較低的方式傳送給服務器。對于任務密切相關子程序的運行，文獻[4]提出了一種函數級的遠程認證方法。該方法利用了處理器的調試功能，并且建立了基于TPM為根的信任鏈。方法優點如下：

（1）不需要使用度量數據庫；

（2）不依賴源碼和特定的編譯，因其將直接工作于可執行代碼。

BIND[5]提出一個細粒度的代碼認證，只會認證感興趣代碼片段的執行，因此大大簡化了驗證過程。而在文獻[6]中，對影響整個程序的所有對象（如網絡SOCKETS，文件，相關進程）都進行了分析，這些對象在程序運行時均要經歷度量，因此開銷頗大。 Flicker[7]則是一種基于源代碼的，需要對源代碼加以修改，并利用AMD處理器的安全虛擬機，使用完全隔離方式執行安全、敏感代碼的框架。Seshadri 等人先后在文獻[8]、[9]中提出一種基于原語的在非可信遺留主機上的可以驗證的代碼執行解決辦法，兩者間的差別在于，前者完全基于軟件技術，而后者則基于硬件與軟件的結合技術。在文獻[10]中提出的策略則結合了TPM的時間戳功能，并基于定時的遠程代碼完整性驗證機制而共同解決遺留平臺下遠程軟件的執行完整性認證。文獻[11]則設計了一套名為虛擬機完整性度量系統，可用來對遠程系統的配置及軟件的行為完整性加以認證。文獻[12]分析了感知網絡系統中的遠程代碼認證。對于不同的認證目的，使用了不同的內存噪聲填充技術以及與其相關的通信協議。文獻[13]則對在可信計算框架下的遠程認證進行了系統綜述且給出了研究方向。

從總體上說，遠程認證或者基于軟件，或者基于硬件技術。若由此角度對以上方法進行分類，可得：

（1）基于軟件技術，如文獻[3、8、11、12]；

（2）基于硬件和軟件技術，如文獻[4、7、9、10]。

虛擬機技術也是廣泛采用的技術之一，例如文獻[11]。

2相關技術介紹

本文研究主要針對在遠程非可信主機上的可信程序執行問題。下面，將需使用的技術做出簡單的介紹。

2.1TPM

TPM是一種性優價廉的芯片，其功能在于提供阻止軟件及硬件的攻擊。在可信平臺中，TPM是硬件信任根。根據TCG[14]給出的TPM規約，TPM主要包括安全內存、計算引擎、輸入輸出部件、非對稱密鑰、加密/解密、數字簽名、對稱加密引擎、隨機數生成器和SHA-1引擎。文獻[13]中已經明確指出，可信平臺需要可信組件，而TPM則位列其中。第2期梁志榮：基于行為等價的遠程程序執行認證智能計算機與應用第3卷

2.2程序控制流檢查驗證

按可信計算的觀點，程序正確執行就是程序的行為按預期的方式順序實現。為實現可信計算，就需要對程序控制流進行檢查驗證。由此，也決定了程序控制流非法改變就成為了實施軟件攻擊的關鍵一步[15]。對程序控制流的驗證檢查，文獻中已有相關研究[16-18]。在文獻[16]中，提出了利用控制流完整性（CFI）可以根據靜態規則防止程序控制流的非法改變。而在文獻[17]則給出了基于軟件簽名的控制流檢查（CFCSS： Control Flow Checking by Software Signatures），CFCSS為程序圖中的每一個節點賦予簽名，且添加代碼進行錯誤檢查，這些簽名將在編譯時自動嵌入程序中。程序運行時，嵌入的簽名與運行時的簽名相互比較完成錯誤檢查。在文獻[18]中，又提出了一種基于控制流的驗證方法。

2.3程序分析技術

程序分析是一種對計算機程序行為自動開展分析的技術方法，包括靜態和動態程序分析。程序分析技術已經開發有多種，諸如：控制流/數據流、基于約束的分析、抽象解釋、類型效果系統和程序切片。

控制流圖是對程序中分支跳轉關系的整體抽象，描述程序所有可能執行路徑，定義如下：

控制流圖的節點是語句集合，整個控制流圖必須有唯一的入口和出口。從A到B的邊表示語句A執行后可能直接執行語句B，這是以每條語句為節點的控制流圖。實際操作的控制流圖一般以基本塊（basic block）作為單元節點，每個基本塊包括若干條語句，基本塊本身即有唯一的入口和出口。

文獻[19]對程序分析技術進行了綜述。本文使用的主要是基于控制流的分析技術。

2.4互模擬

互模擬（bisimulation），就是兩個系統可以互相模仿對方，即從觀察者的角度，這兩個系統是行為等價的。文獻[20]對互模擬概念的歷史進行了較為全面的回顧。互模擬有強弱之分，并在進程代數，模型檢測中都有較好的應用。現給出互模擬（bisimul-ation）定義如下：

對于一個遷移系統（S， Λ，→），互模擬關系R是一個二元關系，RS×S， p×q∈S，（p×q）∈R， 對于任何α∈Λ，有p′∈S ，p→αp′，q′∈S ，q→αq′and（p′，q′）∈R 。

3Spirit 概覽

3.1問題定義和假設

現給出Spirit框架的前提和假設。由圖1可見，假設Challenger為服務器，而Attestter Platform為客戶端。Challenger和Attestter均有TPM組件，且二者之間有一條可信的通信通道。Challenger將客戶端程序P提交在Attestter端執行。在此假設下，解決問題是Challenger如何確信P在Attestter端的可行實現。

3.2信任鏈

為了能夠遠程確證P的合法執行，需要對證明的過程建立信任鏈。而信任根就是TPM。信任鏈可以擴展到對系統的啟動時間、P程序的加載和操作系統內核的完整性驗證。

在文獻[4]中，使用了處理器提供的安全內核（Secure Kernel ，SK）服務來構造待證明程序的運行環境。與其類似，Spirit框架也采用這種技術。

Spirit框架可以由如下幾個步驟來實現整體流程：

（1）C在提交程序前，使用程序分析技術對程序P進行控制流分析，且使用文獻[16]中的CFI技術對源代碼的控制流加注標簽，并且編譯出可以提交使用的程序P’。

（2）程序P’在A端執行過程中，如果控制流出現了非法跳轉，根據CFI技術，就會發生錯誤。

（3）程序P’在執行過程中，還要將執行的控制流編碼后，借助TPM的相應引擎實現加密后，發回C。

（4）C根據發回的控制流編碼，將其與原來的控制流編碼（即互模擬等價證明）進行比較。如果不匹配，則出錯。

3.3分布式環境下認證

如果在SETI@Home4項目中，僅僅只由Challenger來完成所有客戶端程序的執行認證，就會給Challenger帶來超過載荷量的計算工作。因此，可以將認證工作分配給Attesting platform來分別加以完成。

由圖1可知，多個attesting platform之間可以彼此相互認證，這種認證主要基于信任鏈的傳播機制來完成和實現的。

4結束語

本文給出了一個遠程程序執行的認證框架。其基本思想很簡單，綜合運用了信任鏈、TPM、程序分析和互模擬等技術。通過TPM可以得到信任根，而通過這個信任根可以構建可信的運行平臺。另一方面，通過信任鏈的傳播，使得在各個客戶端間實現了遠程認證，而服務器間的負載也隨之減少。程序分析技術的使用得到了程序的控制流，即程序的行為，而互模擬技術的使用則可以用來觀察行為的等價。框架的應用場景多是限制在類似于SETI@Home4項目的遠程程序執行認證方面。

參考文獻：

[1]http：//en.wikipedia.org/wiki/Trusted_computing

[2]http：//setiathome.berkeley.edu

[3]CHANG X L， et al.， Lightweight， scalable and OS-transparent remote attestation of runtime program[J]. Applied Mechanics and Materials， 2012，198：506-511.

[4]GU L， et al.Remote attestation on function execution （work-in-progre-ss）. Trusted Systems，2010： 60-72.

[5]SHI E ， PERRIG A， VAN DOORN L. Bind： a fine-grained attestation service for secure distributed systems[C]//2005 IEEE Symposium on Security and Privacy ，2005.

[6]GU L， DING X， DENG R H， et al.Remote attestation on program execution. In：XU S， NITA-ROTARU C， SEIFERT J P. eds[C]//Proceedings of the 3rd ACM Workshop on Scalable Trusted Computing， STC 2008， Alexandria， VA， USA，ACM，New York ，2008-10：11-20.

[7]MCCUNE J M， PARNO B， PERRIG A， et al. Flicker： an execution infrastructure for tcb minimization. SVENTEK J S， HAND S， eds[C]//Proceedings of the 2008 EuroSys Conference， Glasgow， Scotland， UK， ACM， New York ，2008-04：315–328.

[8]SESHADRI A ， et al. Pioneer： verifying code integrity and enforcing untampered code execution on legacy systems，2005.

[9]SESHADRI A， et al.， Externally verifiable code execution[J].Comm unications of the ACM， 2006，49（9）： 45-49.

[10]SCHELLEKENS D， WYSEUR B， PRENEEL B. Remote attestation on legacy operating systems with trusted platform modules[J]. Electronic Notes in Theoretical Computer Science， 2008，197（1）： 59--72.

[11]BAIARDI F ， et al.， Measuring semantic integrity for remote attestation. 2009，5471：81-100.

[12]ABUHMED T， NYAMAA N， NYANG D H. Software-based remote code attestation in wireless sensor network， 2009.

[13]LEE-THORP A .Attestation in trusted computing： challenges and potential solutions[R]. Technical report， Royal Holloway. 2010.

[14]www.trustedcomputinggroup.org

[15]ZENG B ， TAN G， MORRISETT G. Combining control-flow integrity and static analysis for efficient and validated data sandboxing， 2011.

[16]ABADI M ， et al.A theory of secure control flow. Formal Methods and Software Engineering， 2005：111-124.

[17]OH N， SHIRVANI P P，MCCLUSKEY E J. Control-flow checking by software signatures[J]. Reliability， IEEE Transactions on， 2002， 51（1）：111-122.

[18]JENSEN T， LE TAYER D M E，THORN T. Verification of control flow based security properties， 1999.

[19]MIDTGAARD J. Control-flow analysis of functional programs. ACM Comput. Surv. issue_date = {June 2012， 2012. 44（3） }： 10：1-33.

[20]SANGIORGI D. On the origins of bisimulation and coinduction. ACM Trans. Program. Lang. Syst.， 2009，31（4）：1-41.