基于強化學習的安全協(xié)議形式化驗證優(yōu)化研究

楊錦翔，熊 焰，黃文超

（1.中國科學技術大學 網(wǎng)絡空間安全學院，合肥 230022；2.中國科學技術大學 計算機科學與技術學院，合肥 230022）

0 概述

安全協(xié)議旨在通過應用密碼原語在不安全的網(wǎng)絡上提供安全通信。然而，安全協(xié)議的設計特別容易出錯，研究者在5G［1］、TLS［2］等協(xié)議中都發(fā)現(xiàn)了設計上存在的缺陷。這使得安全協(xié)議的安全性驗證成為一個熱門的研究課題。

目前，已有許多對安全協(xié)議進行建模與分析的工作。最早的協(xié)議分析工具如Interrogator［3］和NRL Protocol Analyzer［4］，能夠驗證時序邏輯中的安全屬性。一些通用的模型檢測工具也已經(jīng)被用于分析協(xié)議，如FDR［5］和Murphi［6］。最近，研究的重點轉(zhuǎn)向了設計專門用于分析安全協(xié)議的模型檢測工具，如Blanchet’s ProVerif［7］、AVISPA tool［8］、MaudeNPA［9］和Tamarin prover［10］。

雖然在安全協(xié)議的設計中利用形式化的方法能夠成功地找到漏洞，但實現(xiàn)對安全協(xié)議的全自動分析仍然是一個挑戰(zhàn)。smartVerif［11］是基于強化學習的一般性框架，其能提高目前最先進驗證工具的自動化能力，但不足之處在于無泛化性，需要對每個安全協(xié)議訓練一個對應的神經(jīng)網(wǎng)絡模型，每個安全協(xié)議的驗證都需要從完全隨機探索開始訓練，因此驗證效率較低。

本文基于無人工特征的強化學習模型對smartVerif框架進行優(yōu)化。該優(yōu)化方案通過Alpha Go zero［12］中將深度神經(jīng)網(wǎng)絡與蒙特卡洛樹搜索相結(jié)合的形式，與smartVerif 中所使用的DQN 網(wǎng)絡結(jié)構相比，只需要利用安全協(xié)議訓練一個模型即可驗證新的安全協(xié)議，無需重新訓練網(wǎng)絡。此外，關注形式化驗證數(shù)據(jù)所包含的結(jié)構化信息，在向量表示方法中使用樹型結(jié)構作為中間表達對形式化數(shù)據(jù)進行轉(zhuǎn)換，同時考慮驗證過程中的歷史信息。與smartVerif 中對字符串進行哈希的向量化方式相比，特征向量包含了形式化數(shù)據(jù)的結(jié)構信息。

1 相關研究

在用于驗證安全協(xié)議的典型模型檢測方法中，ProVerif［7］是一種有效且使用廣泛的協(xié)議分析工具，其通過在Horn 邏輯下對協(xié)議編碼的抽象來進行分析驗證。這種抽象方法非常適合攻擊者知識不變的情形，因此該工具能夠有效地驗證具有無限數(shù)量協(xié)議會話的協(xié)議［13-14］，可證明可達性性質(zhì)、對應斷言和觀察等價性。StatVerif［15］是對ProVerif 的一種擴展。StatVerif 中的擴展設計目的是為了避免許多錯誤的攻擊，常用于自動推斷操縱全局狀態(tài)的協(xié)議。GSVerif［16］將ProVerif擴展到全局狀態(tài)，提供了包括私有信道、工作單元和計數(shù)器在內(nèi)的幾種合理的轉(zhuǎn)換，能夠驗證具有全局狀態(tài)的協(xié)議是有效的。

另一種支持狀態(tài)性協(xié)議驗證的驗證工具是Tamarinprover［10，17］，其未使用抽象技術，而是利用反向搜索和引理來處理驗證中的無限狀態(tài)空間。tamarin 及其相關工具的優(yōu)勢在于，在處理不能通過抽象和解析的方法捕獲到的數(shù)據(jù)之間的形式化關系時，有極大的靈活性。tamarin 能夠處理全局狀態(tài)協(xié)議［18］、無限會話協(xié)議［10］、觀察等價屬性［19］、異或操作［1］等。然而，這是以失去自動化能力為代價的，即用戶必須通過證明復雜協(xié)議的輔助引理來解決問題。目前，tamarin 已經(jīng)被用來分析Yubikey device［20］、security APIs in PKCS#11［21］和TPM協(xié)議族［22］，并且有研究者通過tamarin prover 發(fā)現(xiàn)了V2X［23］協(xié)議的攻擊方式。

上述工具在驗證過程中都是使用靜態(tài)策略，這會在驗證復雜協(xié)議時導致驗證無法成功終止。為了應對這些無法終止的情形，需要分析原因并添加手工證明過程。而smartVerif 則是使用動態(tài)策略對協(xié)議進行驗證，其通過強化學習的方式，使用DQN 網(wǎng)絡結(jié)構［24］學習得到動態(tài)的策略。由于smartVerif 視不同的協(xié)議為不同的任務，因此針對不同的安全協(xié)議需要訓練不同的網(wǎng)絡，導致網(wǎng)絡失去泛化能力，與靜態(tài)策略相比，驗證效率相對較低。

2 優(yōu)化方案設計

為更高效地使用動態(tài)策略對安全協(xié)議進行形式化驗證，同時使得模型學習的策略具有泛化性，需要對驗證框架中的強化學習模型進行一定的優(yōu)化設計，其中存在以下兩個挑戰(zhàn)：1）如何將形式化驗證數(shù)據(jù)在相對完整地保留數(shù)據(jù)信息的前提下，轉(zhuǎn)換成神經(jīng)網(wǎng)絡的輸入；2）如何對強化學習網(wǎng)絡結(jié)構進行改進與優(yōu)化，使得模型具有泛化性。本文提出一種關注數(shù)據(jù)結(jié)構信息的向量表達方式，并且使用Alpha Go Zero 中的強化學習框架替代smartVerif 中的DQN 神經(jīng)網(wǎng)絡結(jié)構。

2.1 優(yōu)化步驟

本文優(yōu)化設計的具體步驟如下：

步驟1選取smartVerif 中所使用的24 個協(xié)議隨機進行分割，將其中的20 個作為訓練集，4 個作為驗證集。

步驟2以多線程的方式對訓練集中的協(xié)議進行訓練。對訓練的每一個輪次中的每個協(xié)議：

步驟2.1使用Tamarin-prover 產(chǎn)生形式化數(shù)據(jù)，并將數(shù)據(jù)轉(zhuǎn)換為證明定理樹。

步驟2.2對當前證明定理樹中仍未完成證明的每個結(jié)點構建特征向量S，使用深度神經(jīng)網(wǎng)絡fθ計算所有這些結(jié)點相應的動作選擇概率P以及當前結(jié)點的價值v：(P，v)=fθ(S)。

步驟2.3對步驟2.2 中所有進行計算的結(jié)點使用蒙特卡洛樹搜索（MCTS），每一次對每個結(jié)點執(zhí)行選擇、擴展、更新操作。重復100 次后，利用MCTS的結(jié)果進行當前結(jié)點的動作選擇。直到對所有結(jié)點完成動作選擇。

步驟2.4將步驟2.3 中所有的動作選擇加入證明定理樹，利用循環(huán)檢測算法檢測證明定理樹中每一條沒有終止的證明路徑。

步驟2.5如果路徑已經(jīng)產(chǎn)生循環(huán)，則將路徑標記為循環(huán)路徑，不再進行證明，否則繼續(xù)對路徑重復執(zhí)行步驟2.1～步驟2.4。

步驟2.6若證明定理樹上所有路徑都已經(jīng)終止證明，則說明當前協(xié)議證明成功或者無法終止證明。此時，需要對證明定理樹上的各個結(jié)點進行評估并設置獎勵z，最后將數(shù)據(jù)（S，P，z）保存到數(shù)據(jù)緩沖區(qū)。

步驟2.7本輪所有協(xié)議完成驗證后，從數(shù)據(jù)緩沖區(qū)中隨機取出256 個數(shù)據(jù)進行訓練。

步驟3每進行5 次訓練，對fθ進行一次評估。比較本次訓練的fnow與保存下的最佳模型fbest，留下效果更好的模型作為新的fbest。

2.2 強化學習框架

本文優(yōu)化方案使用一個深度神經(jīng)網(wǎng)絡fθ，其中，θ表示網(wǎng)絡的參數(shù)。網(wǎng)絡的輸入是由Tamarin-prover 驗證協(xié)議過程中形成的證明定理樹中每條路徑結(jié)點信息組成的向量，以及當前葉結(jié)點的所有可選動作的結(jié)點向量這2 個部分組成特征向量S。網(wǎng)絡的輸出是當前葉結(jié)點的所有可選動作的概率P以及當前葉結(jié)點的價值v，(P，v)=fθ(S)，其中葉結(jié)點的價值表示當前葉結(jié)點能夠完成證明的可能性。這個神經(jīng)網(wǎng)絡將策略網(wǎng)絡和價值網(wǎng)絡組合成一個單一的體系結(jié)構［25］。在整個協(xié)議驗證過程中，需要利用神經(jīng)網(wǎng)絡選擇后續(xù)用來完成協(xié)議證明的結(jié)點擴展定理樹。重復擴展直至協(xié)議證明完成或者產(chǎn)生循環(huán)證明的路徑。

2.2.1 特征向量結(jié)構

特征向量由2 個部分組成：第1 部分是證明定理樹中某條未完成證明的路徑上的所有結(jié)點向量化后所構成的向量V=[v1，v2，…，vt]。其中，vi(1≤i≤t)是路徑中某個結(jié)點的形式化數(shù)據(jù)向量化表達；第2 部分是所有當前可選子結(jié)點向量U=[u1，u2，…，ut]，其中，ui(1≤i≤s)是當前證明定理樹中的葉結(jié)點的某個可選動作的向量化表達。因此，特征向量S=[V，U]。

如圖1 所示，虛線框標識了當前證明定理樹中的一條證明路徑，路徑中末尾結(jié)點的4 個子結(jié)點代表當前的4 個可選動作，因此，在當前狀態(tài)下，方框中末尾結(jié)點的特征向量S=[V，U]，V=[v1，v2，…，vt]，U=[u1，u2，…，ut]。

圖1 證明定理樹中的一條路徑以及可擴展葉結(jié)點的所有可選動作Fig.1 A path in a proof tree and all optional actions of extensible leaf nodes

2.2.2 結(jié)點向量化

本文所使用的向量轉(zhuǎn)換方式為：首先將結(jié)點中的形式化數(shù)據(jù)從字符串形式轉(zhuǎn)換成一個樹形結(jié)構形式，然后將樹形結(jié)構中的結(jié)點信息轉(zhuǎn)換為向量，最后利用樹形結(jié)構的結(jié)構表達進一步地將結(jié)點信息整合，利用根節(jié)點的向量表示形式化數(shù)據(jù)的向量，從而使形式化數(shù)據(jù)的向量化表達包含數(shù)據(jù)的結(jié)構化信息。所有的形式化數(shù)據(jù)可分為5 種類型，分別是Split、Action、Premise、Disj 和Chain［17］。由于每個結(jié)點僅屬于某一種類型，因此可用不同的根結(jié)點表示不同的結(jié)點類型，同時以所有的葉結(jié)點表示各個變量，非葉結(jié)點表示一種操作。然后以哈希的形式將樹形結(jié)構中的每一個結(jié)點轉(zhuǎn)換為向量的形式，再采取自下而上的方式更新樹形結(jié)構中的每一層結(jié)點的向量表達。最后以根節(jié)點的向量作為整個樹形結(jié)構的向量化表達。

圖2 所示為結(jié)點No 的形式化數(shù)據(jù)“State_11111111111（~lock12，pid，k，nonce，npr，otc，secretid，”所對應的樹形結(jié)構表達，其中：是Premise 類型結(jié)點的唯一操作符，可以以為根節(jié)點的樹形結(jié)構表示類型為Premise 的結(jié)點；非葉結(jié)點的“State_11111111111”操作視為一個函數(shù)；“#t1”表示時間戳，視為一個變量，括號內(nèi)各個操作數(shù)也視為變量。

圖2 結(jié)點No 對應的樹形結(jié)構Fig.2 Tree structrue of information in node No

將形式化數(shù)據(jù)的字符串表達形式轉(zhuǎn)換為樹形結(jié)構的結(jié)構化表達形式，然后將樹形結(jié)構中每個結(jié)點中的字符串以哈希的方式轉(zhuǎn)換成一個128 位的01 串，以128 維的向量表示。在此基礎上，以自下而上的順序更新樹形結(jié)構中每一層結(jié)點的向量表達，并以根節(jié)點的向量結(jié)果表示整個樹形結(jié)構的向量化表達。具體而言，對樹中的某個結(jié)點No，若其子結(jié)點向量化表達為c1，c2，…，cp，d1，d2，…，dq，其 中：ci表 示結(jié)點No 的子結(jié)點為葉節(jié)點；dj表示結(jié)點No 的子結(jié)點為非葉節(jié)點。因此，則結(jié)點No 的葉子結(jié)點總數(shù)為p+q，則結(jié)點No 的向量表達xn為：

2.2.3 深度強化學習網(wǎng)絡

深度神經(jīng)網(wǎng)絡由安全協(xié)議通過強化學習驗證過程中產(chǎn)生的形式化數(shù)據(jù)進行訓練。對每一個特征向量S，都會在神經(jīng)網(wǎng)絡fθ的指導下執(zhí)行蒙特卡洛樹搜索（MCTS）。MCTS 搜索結(jié)束后會產(chǎn)生當前所有可選動作的概率π。π經(jīng)過MCTS 后往往會比神經(jīng)網(wǎng)絡fθ產(chǎn)生的動作概率P更接近想要的結(jié)果（協(xié)議完成驗證）。因此，在協(xié)議驗證的過程中使用基于MCTS的增強策略選擇每個動作，然后使用能夠完成驗證的數(shù)據(jù)與無法終止驗證的數(shù)據(jù)作為樣本訓練神經(jīng)網(wǎng)絡，可以將MCTS 過程看作一種有力的策略評估器。本文使用的強化學習算法重復策略迭代的過程，以MCTS 產(chǎn)生的動作選擇策略π作為神經(jīng)網(wǎng)絡fθ產(chǎn)生的動作選擇策略P的指導，更新神經(jīng)網(wǎng)絡的參數(shù)。神經(jīng)網(wǎng)絡的參數(shù)更新使得迭代過程中產(chǎn)生的策略和價值逐步逼近能夠成功驗證協(xié)議的策略和價值。

深度神經(jīng)網(wǎng)絡整體由公共網(wǎng)絡部分和2 個分離的策略網(wǎng)絡與價值網(wǎng)絡組成。網(wǎng)絡的輸入為特征向量S=[V，U]。首先將V經(jīng)過一個公共的textCNN層［26］，將不定長路徑向量V轉(zhuǎn)換為一個1×128 維的向量A。然后將A分別輸入策略網(wǎng)絡和價值網(wǎng)絡。策略網(wǎng)絡對A與U進行注意力計算［27］，再經(jīng)過一個softmax 層得到各個動作的選擇概率。價值網(wǎng)絡首先將U進行最大池化操作得到特征向量B，再將A與B進行點積運算，最后通過一個tanh 層得到當前特征向量S的價值。網(wǎng)絡的訓練是在損失函數(shù)l上的梯度下降過程，損失函數(shù)由方差和交叉熵以及網(wǎng)絡參數(shù)的二階范式（防止過擬合）組成：

MCTS 模擬探索過程可分為選擇、擴展評估、參數(shù)更新3 個階段。在MCTS 的搜索樹中，每條邊（s，a）存儲了選擇概率P（s，a）、當前結(jié)點訪問次數(shù)N（s，a）和當前結(jié)點的價值Q（s，a）。

在選擇階段，t時刻在搜索樹中模擬通過選擇有最大結(jié)點價值Q，再額外加上一個由選擇概率和當前結(jié)點訪問次數(shù)決定的置信上限U的動作。

其中，cpuct=3 為探索常數(shù)，用來在MCTS 模擬搜索的過程中探索盡可能多的結(jié)點。

在擴展評估階段，選擇達到葉結(jié)點時，如果可以繼續(xù)進行協(xié)議驗證，則需要用fθ擴展搜索樹。

在參數(shù)更新階段，對搜索樹上的邊存儲的信息在每個時間節(jié)點向后更新：

在MCTS 模擬搜索T次后，從開始模擬的根節(jié)點根據(jù)模擬結(jié)果做出動作選擇：

其中，τ是一個探索參數(shù)，根據(jù)τ設置不同的值控制當前執(zhí)行探索或者是按策略進行動作選擇。

前5 步選擇動作時概率為：

5 步之后選擇動作的概率為：

其中，η～Dir(1.2)，ε=0.25。添加狄利克雷噪聲的目的是為了覆蓋所有的可選動作。

2.2.4 循環(huán)檢測算法

本文使用smartVerif 中所使用的循環(huán)檢測算法［11］來檢測當前證明定理樹中的某條路徑是否已經(jīng)產(chǎn)生循環(huán)。對于已經(jīng)產(chǎn)生循環(huán)的路徑，不再繼續(xù)進行驗證。由于在smartVerif 中的參數(shù)設置會使得部分安全協(xié)議的循環(huán)路徑被判定為正確證明路徑，因此本文的循環(huán)檢測算法中的參數(shù)與smartVerif 中所使用的參數(shù)設置不同：α=20，β=0.2，ρ=20，δ=3，確保不在循環(huán)路徑上耗費過多的時間而降低驗證效率。

3 實驗結(jié)果與分析

3.1 訓練與評估方法

通過上文所提到的流程執(zhí)行算法得到每個協(xié)議驗證產(chǎn)生的證明定理樹。對每個證明定理樹中的每條路徑而言，路徑上的結(jié)點價值設置為：循環(huán)路徑上從循環(huán)開始的結(jié)點到末尾結(jié)點價值為-1；證明結(jié)束路徑上的最長不與循環(huán)路徑相交部分所有結(jié)點價值為1，其余結(jié)點不做評估，防止陷入局部最優(yōu)。將評估后的數(shù)據(jù)（S，P，z）存放到數(shù)據(jù)緩沖區(qū)。

數(shù)據(jù)緩沖區(qū)是一個大小為10 000 的隊列。每次訓練數(shù)據(jù)的批量大小為256，每訓練5 次對當前模型進行一次評估。分別使用上一次保存的最佳模型fbest與本次訓練后的模型fnow對驗證集進行驗證，有以下3 種情況：1）fbest與fnow都不能驗證所有驗證集中的協(xié)議文件，此時取能夠驗證協(xié)議個數(shù)最多的模型作為fbest；2）fbest和fnow中只有一個能證明所有驗證集中的協(xié)議，此時取能夠證明所有驗證集中協(xié)議的模型作為fbest；3）fbest和fnow都能證明驗證集中所有協(xié)議。

對于第3 種情況，設置信比例為θ=0.1，若fbest證明驗證集中協(xié)議時間分別是（k為驗證集大小），fnow證明第j個協(xié)議（1≤j≤k）時間滿足則認為模型訓練效果對第j個協(xié)議而言沒有變化。

設cS表示的協(xié)議個數(shù)，cL表示的協(xié)議個數(shù)。當cS>cL時，說明當前網(wǎng)絡模型更優(yōu)，使用fnow替代fbest；當cS≤cL時，說明fnow相比fbest沒有得到優(yōu)化，保留fbest。

3.2 實驗結(jié)果

本文實驗在Intel Broadwell E5-2660V4 2.0 GHz CPU、128 GB內(nèi)存、4個GTX 1080 Ti顯卡、Ubuntu 16.04 LTS 的環(huán)境下進行，強化學習交互對象是tamarin prover v1.5.1。實驗的驗證集中包含隨機抽取的TPM-toy、Feldhofer’s RFID、CANauth 和Okamoto 協(xié)議，實驗結(jié)果如表1 所示，其中，∞表示證明時間超過150 min。

表1 不同訓練輪次下協(xié)議的驗證時間Table 1 Verification time of each protocol in different training rounds min

3.3 案例分析

以Okamoto 協(xié)議為案例進行分析。該協(xié)議在沒有安全專家設置的靜態(tài)策略指導下，容易陷入狀態(tài)爆炸的證明狀態(tài)。當網(wǎng)絡訓練輪次較少時，Okamoto 協(xié)議無法在有限的時間內(nèi)完成證明。由表1 所示的實驗結(jié)果可知：Okamoto 協(xié)議在訓練至85 輪次、證明時間為150 min 時，搜索遍歷的證明定理樹結(jié)點數(shù)量為24 853 個；當訓練至165 輪次時，完成協(xié)議驗證共訪問了18 649 個結(jié)點；當訓練至260 輪次時，完成協(xié)議驗證共訪問了13 468 個結(jié)點；而當訓練至350 輪次時，訪問結(jié)點減少到了9 635 個。因此，使用訓練集數(shù)據(jù)對神經(jīng)網(wǎng)絡的訓練，對驗證集中的協(xié)議驗證起到了指導作用，使得驗證集中的協(xié)議進行驗證時遍歷訪問的結(jié)點總數(shù)逐漸減少。

4 結(jié)束語

基于強化學習的形式化驗證工具普遍存在模型無泛化性和驗證效率低的問題。本文使用一種具有泛化能力的神經(jīng)網(wǎng)絡，并通過將形式化數(shù)據(jù)字符串表達形式轉(zhuǎn)換為樹形結(jié)構表達形式來保留形式化數(shù)據(jù)所具有的結(jié)構信息。通過引入完全自學習而不添加人工特征的強化學習模型替代原有的DQN 模型結(jié)構，使得模型經(jīng)過訓練后對安全協(xié)議的驗證具有泛化性。同時，保留形式化數(shù)據(jù)的結(jié)構特征以提高協(xié)議驗證效率，縮短協(xié)議驗證時間。后續(xù)將在形式化數(shù)據(jù)的轉(zhuǎn)換上保留語義特征，進一步提高驗證效率，并尋找合適的模型評估手段加快神經(jīng)網(wǎng)絡收斂速度。此外，還將使用手工建模的方式對一些安全協(xié)議［28-30］進行建模，探究改進后smartVerif 的泛化性和驗證效率。