Ｈｌｐｓｌ２Ｃｐｐ——一個安全協議編譯器
2007-01-01 00:00:00周天凌黃連生
計算機應用研究 2007年6期
摘 要：安全協議的人工實現是一個低效且易錯的過程。安全協議編譯器Hlpsl2Cpp可以自動從用HLPSL語言描述的安全協議生成C++的協議實現代碼。Hlpsl2Cpp節省了人工實現協議的大量重復勞動，避免了人工實現安全協議帶來的各種訛誤和實現相關漏洞。
關鍵詞：代碼生成；規范語言；安全協議；網絡安全
中圖分類號：TN915.08文獻標志碼：A
文章編號：1001-3695(2007)06-0123-04
目前，安全協議的實現工作仍然強烈依賴于人工編碼，這是各種漏洞出現的重要原因。首先，其存在對細節部分的處理失當；其次，實現代碼未必精確體現了安全協議設計者希望表達的意圖；最后，對協議的修訂難以及時反映到實現中。目前已知在SSL、PPTP、RADIUS、SSH1等安全協議的實現中都出現了與實現相關的漏洞。
安全協議編譯器是一種從形式化的協議描述自動產生一般高級語言代碼的工具。它有效地避免了代碼實現過程中的人工成分，即避免了人工編碼可能導致的各種弱點。Hlpsl2Cpp是筆者開發的一個從AVISPA項目HLPSL語言［1］的協議描述到C++實現的安全協議編譯器。
1 相關工作
已知的最早的安全協議編譯器是A. Perrig等人［2］介紹的Athena到Java工具。其存在較大的局限性，它甚至沒有使用任何實際的網絡通信。
F. Muller等人［3］介紹了一種CAPSL［4］到Java的安全協議編譯器。它采用了一個中心服務器轉發所有消息的模型，這和協議的實際工作環境是不一致的。
X. Didelot［5］詳細介紹了一個從CSP/Casper［6］到Java的安全協議編譯器COSPJ。其局限在于：依賴于Java的序列化機制，難以和其他版本的協議實現互連互通；生成的代碼過于封閉，不方便應用集成。
D. Pozza等人［7］介紹了Spi2Java，從Spi Calculus生成Java代碼。其特色在于加入了密碼算法庫的抽象層，可以在特定的密碼算法庫發現漏洞時，方便地切換到其他版本的庫。其在報文封裝格式和傳輸層上仍有其局限性。
B. Tobler等人［8］介紹了另一個版本的Spi2Java。其特點在于試圖向形式化證明實現代碼等價于協議描述作出探索，但目前尚未披露細節。
S. Lukell等人［9］介紹了SPEAR Ⅱ系統和其內置的協議編譯器。其特點在于使用了通用的報文格式，方便互連互通；但純圖形化的協議描述系統不利于與其他協議驗證工具協同工作。
上述的工作，其目標語言都是Java語言。而本文的工作其目標語言是C++語言。C++和Java在資源管理、內存保護上存在諸多差異，使用Java語言的編譯器無須對資源管理和內存保護作出任何處理，而這正是本工作的難點之一。
2 技術方案的選擇
參考前人的工作，筆者提出了安全協議編譯器在設計和技術方案選擇上的三條原則，并以此為依據對輸入協議描述語言、目標語言、報文格式以及底層平臺作出選擇。
(1)源語言應當具有嚴格定義的形式化和強大的描述能力，具有協議驗證工具的支持。
(2)目標代碼應當結構清晰、易于與協議設計相對照，便于用戶二次開發。
(3)以通用、開放的技術架構作為底層平臺，包括報文格式和密碼算法。
HLPSL（高層次協議規范語言）具有基于TLA邏輯的形式化語義。其他語言如CAPSL［4］、CSP/Casper［6］的描述能力不及HLPSL，如不能選擇入侵者模型和安全目標，不允許報文盲轉發等，而HLPSL提供了控制流、強數據類型、可替換的入侵者模型以及自定義安全目標等強大功能。作為AVISPA Project的一部分，OFMC［10］等多套協議驗證工具的支持，為用HLPSL描述的協議提供了強大的保證。因此筆者選擇HLPSL作為安全協議編譯器的輸入語言。
C/C++語言具有廣泛的支持平臺和充分的性能保證，在相當數量的應用平臺（如嵌入式系統）上C/C++是唯一的選擇。相對于Java，C/C++編程更加容易出錯——缺乏語言內置的垃圾收集和內存保護機制，這使得安全協議編譯器更為重要。因此筆者選擇C++語言作為目標語言。
ASN.1［11］（抽象語法定義）是ISO與ITUT的聯合標準，它描述信息內數據，數據類型、序列格式以及規定如何編碼解碼。其在安全領域已經被應用于X.509、RSA、PCKS等多種應用。筆者自然地繼承了這一選擇，并采用了最常用的ASN.1 DER編碼規則。
筆者選擇OpenSSL作為底層平臺。其具有體系開放、跨平臺、高性能、便于裁減的特點，提供了大部分主流的密碼算法ASN.1等輔助組件的實現。
3 HLPSL語言
與常見的AliceBob描述形式不同，HLPSL描述協議是將協議分解到參與它的每個實體分別用狀態來描述。參與協議的一個實體在HLPSL中被定義為一個role，本文以ISO/IEC 97983中的第四個協議threepass Mutual Authentication為例（以后簡稱為ISO4協議）來說明HLPSL語法。用常用的AliceBob語義表示簡化的協議如下：
如上文所示，每個role的定義由四個小節組成。其中local定義局部變量、const定義常數、init定義變量初值、transition定義狀態機規則（形式為：條件=|>動作）。特別地，Snd和Rec是role對外通信的兩個Channel。HLPSL嚴格區分變量在狀態轉移前和轉移后的取值，后者用“′”特別地標出，如“PKb′”。
一個用HLPSL描述的role狀態機處理過程，可以用圖1的模式簡單表達為一個大循環。每一輪循環先根據當前狀態判斷應當應用的規則，然后按照規則接收和驗證報文、修改狀態、發送回應。
定義狀態機的失敗條件為：狀態機在“Receive Message”階段，接收到一條它當前所不期望的消息或者“Verify Message”失敗；定義終止條件為：經過一條轉移規則后，狀態機在“Dispatch Rule”階段找不到下一條可以應用的規則。
4 總體結構
4.1 框架
Hlpsl2Cpp的輸入是HLPSL協議描述源文件，它為每個協議參與者生成一個C++類作為協議的實現代碼。Hlpsl2Cpp使用C++編寫。其總體框架如圖2所示。它是一個典型的編譯器結構。
詞法分析和語法分析模塊組成了編譯器的前端，分析HLPSL源文件并為每個role生成用于內部表達的Role Descriptor。由一致性檢查和行為關聯分析組成的分析器對Parse生成的Role Descriptor加以分析，并將分析結果作為批注附加其上。最后代碼生成器的三個組件分別根據Role Descriptor及其批注生成C++代碼。生成的C++代碼和本文提供的Demo Framework聯編，即可生成供演示運行的實例程序。
4.2 一致性檢查
一致性檢查用于確保單個role的具體行為都是可實現的。
(1)檢查在規則中使用的所有符號均有定義。
(2)檢查在規則中使用的所有消息均是可計算的。
①role的參數或者常數可計算；
②存在賦值語句的變量可計算；
③存在接收語句的消息可計算；
④可計算的消息，其每一個直接子消息均可計算；
⑤若干可計算的消息連接的結果是可計算的；
⑥加密、解密、簽名、哈希運算中自然蘊涵的那些可計算性規則。
編譯器首先由規則①－③構建一個基本知識庫，然后對所涉及的每個消息在其中搜索可能的計算路徑，當不存在這樣的計算路徑時，則該協議是不可實現的。計算路徑作為批注加入到Role Descriptor中。
4.3 行為關聯分析
行為關聯分析用于確保參與協議的每個role可以相互合作完成整個協議。
(1)檢查不同role中定義的同名符號是否數據類型一致。
(2)檢查Snd和Rcv操作。分析Snd與Rcv之間的配對關系。
HLPSL假定所有role都通過入侵者完成交互，而沒有明確地指出消息發送的目的對象和消息接收的源對象。需要分析role之間的行為關系，找出每一條消息的目的對象。
①檢查所有的Snd操作，為其找出消息類型匹配的Rcv操作。
②若某條Snd操作對應的Rcv只有一個可能的目的對象，則配對它們。
③將剩下的Snd操作和Rcv操作構建一個二分圖，在類型匹配的操作之間連線。若某個操作不存在可匹配的操作，則失敗。
④若該二分圖存在完美匹配，則全部輸出供用戶選擇。
⑤若該二分圖不存在完美匹配，那么作擴展匹配如下：一條Rcv操作可匹配多條來自同一role的Snd操作。輸出所有可能的擴展匹配供用戶選擇。
僅對極少量的存在分支的多人復雜協議可能需要用戶選擇匹配方案。
完成配對分析后，為每條Snd/Rcv操作標記它們對應的role，并為每個role標記與其存在消息交換的其他role。
4.4 代碼生成器
代碼生成器根據Parser生成的Role Descriptor和Analyzer分析給出的批注信息自動地生成協議的C++實現。用戶可以通過選項控制生成的具體代碼，例如：使用何種加密算法、使用的傳輸層接口，是否包含完整的log信息等。
代碼生成器生成三組文件，其每個組件分別負責一組。首先是類型映射器生成的協議報文封裝，其次是Class定義器生成的C++ Class定義，最后是動作編碼器將規則翻譯成具體的Code，實現C++ Class。附帶還提供了一個最基本的應用程序框架Demo Framework，把這四者聯編就可以得到可以演示的協議Demo。
代碼生成器本身做的工作是一條條按照規則生成的目標代碼。
5 目標代碼結構
5.1 數據類型映射和協議報文封裝
在協議實現過程中，必須將抽象數據類型映射到實際的數據類型，并為其選擇具體的密碼算法。
首先，需要建立HLPSL語言中的基本數據類型和ASN.1數據類型的映射關系（表1）。
類型映射器逐個掃描輸入中所有涉及的報文，為每個報文生成對應的ASN.1 SEQUENCE表示。當報文出現嵌套時，為嵌套的子報文對應的也生成ASN.1 SEQUENCE表示。最后將這些ASN.1類型依照OpenSSL定義的規則映射成C++數據類型，并為DER編碼功能生成了相應的支持代碼。
以報文Pka.A.{Pka.A}_inv(Pks)為例，產生如表2中的數據類型定義。
筆者默認以Socket 作為協議報文的傳輸層，用戶也可以控制采用其他傳輸接口，只要指定不同的句柄類型并給出相應的數據接收和發送函數即可。
其中init函數用于初始化對象，play函數負責執行整個狀態機。如圖 1所示，單個role的狀態機表現為一個大循環。play函數簡單的循環調用play_onestep函數，直到協議完成或失敗退出。play_onestep函數負責處理狀態機的Dispatch Rule階段，根據當前的狀態，決定應當應用的規則，并調用對應的處理函數。rule_〈n〉系列函數負責處理第n條規則的Receive Message至Send Message階段。
5.3 動作編碼
代碼生成器中的動作編碼器負責具體實現5.2節所給出的C++ Class。在一致性檢查階段，編譯器已經為需要用到的各個消息和表達式的求解出了計算路徑。在這一步只需要簡單地將計算路徑翻譯成調用OpenSS的C++代碼即可。其偽代碼結構如下：
本文避免了人工實現協議容易出現的一些弱點：首先，自動生成代碼保證對所有的I/O動作都檢查緩沖區是否可能溢出；其次，保證對接收到的所有數據均會有驗證代碼，這避免了False Input Attack；再則，通過文獻[12]介紹的消息tag機制，避免了Type Flaw Attack；最后，對資源泄露等手寫代碼常見的非安全性bug也通過析構函數guard機制進行了保護。
6 總結與展望
Hlpsl2Cpp的目標代碼行為忠實于協議描述，避免了常見的實現弱點，并對常見的通用攻擊手段作了防范。目標代碼結構清晰、功能明確、可擴展性強，為二次開發打下了良好的基礎。基于ASN.1的協議報文體系，使得目標代碼可以與非Hlpsl2Cpp的協議實現互連互通。相對于基于Java目標代碼的工具，Hlpsl2Cpp在應用方面具有更大價值。Hlpsl2Cpp工具為安全協議的設計、測試、評估工作提供了一個良好的平臺，為基于安全協議的應用開發提供了可用的代碼框架。筆者對HLPSL協議庫［1］中的協議進行了測試，證明了該工具是確實可用的。
Hlpsl2Cpp目前僅支持C++一種目標語言，擴展該工具支持更多的目標輸出語言，甚至提供一種方便的目標代碼描述模板是十分有用的，這也是筆者下一步的研究方向。同時也將在下一步的研究中，嘗試對Hlspl2Cpp的轉換正確性進行理論證明的探討。
本文中所涉及到的圖表、注解、公式等內容請以PDF格式閱讀原文。
