采用完整性威脅樹的信息流完整性度量方法1

吳奇烜，馬建峰，孫聰

?

采用完整性威脅樹的信息流完整性度量方法1

吳奇烜1,2，馬建峰1，孫聰1

（1. 西安電子科技大學網絡與信息安全學院，陜西 西安 710071；2. 騰訊科技(深圳)有限公司，廣東 深圳 518057）

針對傳統信息流完整性分析方法缺乏對具體系統結構及關聯性攻擊事件考慮的缺陷，提出完整性威脅樹對系統信息流完整性做量化分析，提出條件觸發門對存在關聯的攻擊事件進行建模。使用攻擊代價來量化攻擊各信道的難易度，依據架構相關的完整性威脅樹，利用可滿足性模理論及其工具求解最小攻擊代價，以量化分析系統完整性威脅。通過對實際飛控系統模型的建模分析求解說明方法的實用性，并得出條件觸發門參數對系統完整性的影響。

完整性；信息流；可滿足性模理論；攻擊樹

1 引言

計算機系統的安全性要求包括機密性、完整性和有效性等方面。在安全關鍵的嵌入式控制系統中，嵌入式程序、控制指令和系統配置均具有高完整性要求。信息流完整性是指基于細粒度策略保證與系統架構相關的低完整性信息的流動對高完整性數據（指令、配置）的干擾符合特定的策略規則。現有的定性信息流完整性模型存在諸多不足。Denning[1]提出的信息流安全格模型通過分析數據在系統中的流向來驗證信息在不同實體間傳遞的安全性。以BIBA模型[2]為主流的嚴格信息流完整性模型，依據完整性等級劃分對信息的流向進行控制，確保低等級數據不能流向高等級數據。這些用于防止信息非授權修改的定性模型有時太過嚴格，導致系統效率及應用兼容性等問題[3]。

實際上，程序在運行過程中往往需要使用一些低完整性的數據（如網絡數據），這本身會破壞嚴格的信息流完整性策略。大量場景僅要求威脅程度在可容許的范圍內，而無須保證系統絕對安全，因此對于完整性的定量分析必不可少。針對格模型只能定性分析系統安全性的不足，Millen[4]基于信息論中信息熵提出了無干擾與互信息的關系，首次設計了量化信息流安全模型，但其度量結果不夠準確。此后，Clarkson等[5]以互信息為基礎，提出了量化信息流的污染與抑制，給出了完整性破壞度的計算方法。上述的量化信息流完整性模型僅適用于抽象的系統模型，難以對結構復雜的實際系統進行威脅分析。

攻擊樹因其簡潔直觀的描述方式而廣泛應用于解決“攻擊?防御”場景下的量化安全分析評估[6]。針對系統可能受到的攻擊，攻擊樹能夠進行與具體系統結構相關的量化安全性建模，其局限性在于以下兩方面。一方面，由于傳統攻擊樹僅包含“與門”和“或門”，無法對實際攻擊中的復雜攻擊事件關系進行建模，因而表達能力有待擴展。Jhawar等[7]針對序列化攻擊使用SAND門擴展了攻擊樹的動態建模能力，但模型無法描述存在條件關聯的攻擊事件。另一方面，雖然近期研究引入形式化手段提升攻擊樹的建模準確性[8]及面向特定屬性的推理能力[9]，但其求解方法仍主要由各葉節點基本攻擊事件的成功概率分析預測根節點攻擊目標的成功概率，不適用于對系統完整性進行量化分析，需要更細粒度的節點完整性定義。

本文將量化信息流完整性模型與攻擊樹的系統架構相關建模能力相結合，研究復雜組件化系統的信息流完整性威脅分析方法；提出完整性威脅樹并定義了對應的量化信息流完整性模型；針對當前攻擊樹描述能力的不足，提出條件觸發門用以描述存在條件關聯的攻擊事件；利用可滿足性模理論（SMT，satisfiability modulo theories）對完整性威脅樹進行求解，得出針對目標系統的最小攻擊代價和相應的攻擊方式；針對實際飛控系統模型的分析和求解說明方法的實用性。

2 信息流完整性的量化定義

本文基于信息論概念定義信道（channel）的完整性模型。在實際環境中，用戶和攻擊者均能向信道提供輸入并從信道獲取輸出。攻擊者通過提供不可信的輸入破壞信道的數據完整性。

理想情況下，信道規約（specification）接收可信輸入in并產生可信輸出spec，如圖1(a)所示。而在威脅場景下（一般對于具體信道實現而言），由于存在攻擊者，信道不僅從用戶接收可信輸入，還從攻擊者接收不可信輸入in，此時信道輸出的完整性遭到一定程度破壞，產生被污染的輸出impl，如圖1(b)所示。通過觀察對比impl和spec，即可得到真實輸出的完整性受影響的程度，這一程度反映出可信輸出受不可信輸入影響而丟失的信息量。定義信息流抑制（suppression）表示此信息量，作為信息流完整性的量化定義。

定義1 信息流抑制指用戶無法從impl獲得關于spec的信息量，即由于攻擊者不可信輸入而使真實輸出丟失的信息量。信息流抑制的計算公式為

其中，Tspec為tspec的概率分布，Timpl為timpl的概率分布，H(Tspec|Timpl)指用戶在已知Timpl的前提下得到Tspec的熵。

3 基于完整性威脅樹的信息流完整性建模

針對具體系統的信息流完整性攻擊，定義為由攻擊者實施的一系列輸入操作，這些操作使系統正常的數據交互出現錯誤，如產生數據丟失等。復雜的信息流完整性攻擊，即針對影響目標系統信息流完整性的一組信道，按照一定步驟實施不可信輸入的過程。

信息流完整性攻擊的難易程度可由捕獲信道知識所需付出的代價（cost）進行量化。系統中某信道的cost定義如下。

cost()=(in,spec)×

其中，為令=(spec)時，in的比特數。(in,spec)為信道的in與spec間的互信息(mutual information)，表示在沒有攻擊者干擾的前提下信道所傳輸的數據量，其中，in為in的概率分布。

因此，給定信道集合={1,…,c}，攻擊代價cost()定義為

本文將針對目標系統的信息流完整性攻擊表示為樹形結構，稱為完整性威脅樹。完整性威脅樹的根節點表示攻擊所要達成的最終目標，葉節點表示實現這一攻擊效果可能采取的手段（即在各信道上實施非可信輸入），各中間節點表示要達成最終攻擊效果所經歷的子目標。每個節點以其各子樹的cost值為輸入，并輸出一個cost值，所輸出的cost值表示實施該子目標節點對應攻擊所需付出的代價。參考攻擊樹定義[6]，完整性威脅樹的連接門包括與（AND）門和或（OR）門，AND門表示達成其完整性攻擊目標要求其子樹對應攻擊目標全部完成，其輸出為所有子節點的代價之和；OR門表示達成其完整性攻擊目標要求其任一子樹對應攻擊目標完成，其輸出為所有子節點中代價最小的節點的代價。

在實際系統中，存在一系列相互關聯的信息流完整性攻擊事件，無法使用AND或OR門進行建模分析。例如，在飛控計算機系統中，表決模塊需要在表決前后分別讀寫表決存儲器以完成表決，該存儲器的完整性被攻擊者破壞后，對表決模塊的攻擊難度相比直接攻擊該模塊而言大大降低。針對此類關聯性攻擊事件，本文提出條件觸發門對其進行建模分析。

定義2 條件觸發門是一種接收若干主輸入與若干觸發事件，且產生單一輸出事件的門結構。當主事件全部發生時輸出事件發生，而觸發事件將導致主事件的cost變為正常狀態下的倍（0≤≤1），其圖形表示如圖2所示。

圖2 條件觸發門的圖形表示

條件觸發門的使用條件即系統某些信道之間存在依賴關系，當其中一個信道遭到攻擊后，對其他信道的攻擊難度產生一定影響。在圖2中，成功攻擊信道C將達成相關攻擊目標，此時Some event的代價等于攻擊信道C的代價；信道T與該目標無直接聯系，但攻擊T將導致C的攻擊代價降低，從而降低攻擊目標的總代價，則Some event的代價等于攻擊T的代價加C的代價的倍。

一旦攻擊過程確定，即可以將系統中各個信道上的攻擊代價作為葉節點，建立對應的完整性威脅樹模型，從而明確得出需要攻擊哪些信道及如何組合才能達到攻擊目標。具體建立步驟如下。

1) 分析被評估系統，確定攻擊最終目標，以該目標作為完整性威脅樹的根節點，即頂層事件。

2) 從根節點開始，分析達成該目標所需要達成的子目標，根據這些子目標之間的邏輯關系，通過基本門結構及定義的條件觸發門將其連接到總目標節點下方，構成樹的下一層節點。

3)對每一個子節點，重復第2)步的過程，采取自上而下的方法逐步遞推，直到其子目標無法繼續分解且已是對某個具體信道的攻擊事件為止。

4) 對樹的每一個葉節點，計算其所攻擊的信道需付出的代價，作為其攻擊代價寫入節點。

4 信息流完整性的最優化求解

利用完整性威脅樹對系統攻擊過程進行建模，可根據攻擊系統各信道所需的代價（葉節點）計算出攻擊系統所需的代價（根節點）。為了計算出攻擊系統所需的最小代價，需要求解受布爾條件約束的最優化問題。本文提出基于SMT的最優化求解方法，用于分析攻擊系統所需的最小代價，即根據各信道的cost，找到一個信道集合goal，使該集合中所有信道的cost能夠保證攻擊系統所需代價最小。

該最優化問題可通過計算一系列SMT問題模型Π={Π1,…,Π}求解。每個Π由兩方面約束組成：1)所選goal使頂事件發生；2)由goal中信道求得的頂事件目標值goal比當前goal值小。初始條件Π1下，goal值為+∞。若該樹存在某信道集合，使攻擊者通過捕獲這些信道達成攻擊目標，則goal值必小于+∞；而若最終求得goal值為+∞，則說明根據該完整性威脅樹分析的系統是安全的，攻擊者無法觸發頂事件。迭代過程由Π得到Π+1，Π+1的約束強于Π，從而得到對于攻擊目標的一個更小的代價。當Π+1不可滿足時算法停止，當前模型中包含的信道代價之和即為實現攻擊目標的最小代價。目標函數定義為如下形式。

式中為所有葉節點個數，即系統中總信道數，S為布爾類型，代表該信道是否被選入攻擊模型。當前模型可滿足時，添加新的約束以減小goal值，直到模型不可滿足為止。本文基于SMT求解器設計算法1，用于求解最優化cost。其中，={1,…,S| 1≤≤,S=0/S=1}保存使第一方面約束可滿足的信道選擇約束，SMT求解器能夠通過check檢驗中的約束是否滿足并返回SAT（可滿足）或UNSAT（不可滿足）。判斷模型是否SAT是一個NP完全問題，已有多種成熟的理論及工具支持其求解。

算法1 基于SMT的最優代價求解算法

輸入 P(VT)：由完整性威脅樹轉化得到的約束集；cost()：葉節點cost

輸出：攻擊目標系統的最小cost

開始

1) Init SMT solver : S ← ? ;

2) Minimal cost :← ∞ ;

3) S.add(P(VT));

4) for∈V0do /*初始化節點參數*/

5) S.add(cost()); /*僅基本組件*/

6) S.add(P(= 0) + P(= 1) = 1);

7) while S.check(Π) == SAT do

8) M ← S.model ;

9)← goal(M);

10) Π ← M ∧()

11) Return

End

初始問題模型（model）Π1下，goal值為+∞。若該樹存在某信道集合，使攻擊者通過捕獲這些信道達成攻擊目標，則goal值必小于+∞；而若最終求得goal值為+∞，則說明根據該完整性威脅樹分析的系統是安全的，攻擊者無法觸發頂事件。迭代過程的每一步由Π得到Π+1，Π+1的約束強于Π，goal值更小，從而得到對于攻擊目標的一個更小的代價。當Π+1不可滿足時算法停止，當前模型中包含的信道代價之和即為實現攻擊目標的最小代價。

5 實例研究

本節針對雙余度飛行控制系統實例，說明本文信息流完整性威脅建模及最優化求解方法的實用性。由于攻擊者能夠通過在飛控系統信道注入信號、從物理側或網絡側注入組件故障等方式展開系統信息流完整性攻擊，且攻擊可通過系統組件交互和條件依賴關系傳播，因而針對系統進行信息流完整性威脅建模和最小攻擊代價評估，是找出關鍵完整性威脅并進行加固的基礎。

飛機飛控系統由雙余度計算機（CS1/CS2）和交叉控制器（IC, interactive controller）組成[10]，如圖3所示。雙余度計算機同時使用數據總線接收當前數據，然后分別根據接收的數據同步執行相同的計算過程，表決計算結果，實現對飛行姿態或方位、飛行軌跡、結構模態等的操縱控制。交叉控制器負責計算過程中數據的交叉傳輸（IT, interactive transmission）并執行所有的容錯服務，包括故障檢測（FD, fault detection）、故障類型判斷（FTD, fault type determination）、故障定位（FL, fault localization），并在永久性故障后重新配置系統。

圖3 飛控系統雙余度架構

其中，單個計算機節點主要由數據采集模塊、表決模塊和控制率計算模塊構成。數據采集模塊（DC，data collecter）收集外圍設備的數據（如傳感器采集的飛行狀態等），對傳感器數據使用Kalman濾波進行降噪。表決模塊由用于記錄上次表決結果的表決存儲器（VM，vote memory）和表決控制器（VC，vote controller）組成，負責對雙通道數據進行表決。控制率計算模塊（CLC，control law compute）使用輸入表決的數據作為輸入，調用控制率算法計算出飛機飛行模態等數據。

針對該飛控系統建模得到的完整性威脅樹如圖4所示。使系統癱瘓的攻擊有兩種情況：一是攻擊CS1和CS2使其同時發生故障，此時由于雙余度均無法得到正確的控制信號，飛控系統無法正確運行；二是攻擊CS1或CS2中任一計算機，同時攻擊交叉傳輸模塊，使冗余容錯機制癱瘓，雖然另一計算機仍在正常工作，但由于交叉傳輸模塊的故障CS1與CS2無法正確交互，也會導致整個系統癱瘓。為了說明本文提出的完整性度量方法的實用性，本文分別針對采用兩種不同控制率算法[11-12]的雙余度飛控計算機系統進行完整性威脅分析。依據飛機在大地坐標系的橫側向動力學模型[12-13]，結合實際飛控系統[11]，估算兩系統中各模塊接收輸入數據量、輸出數據量，如文獻[12]中控制律輸出結果為方向舵偏角及副翼偏角，約16.98 bit，輸入包括艦載機質量、速度側向分量、滾轉角、滾轉角速率、偏航角速率、俯仰角等，約35.64 bit，其余模塊按照類似方法計算可得表1的第2、4列。再根據本文前述cost定義求得攻擊各模塊的代價，如表1所示。

圖4 飛控系統完整性威脅樹示意

表1 控制律與模塊cost對照

使用Python基于SMT求解器z3實現算法1，以表1數據作為葉節點參數對圖4所示完整性威脅樹進行攻擊代價最優化求解。實驗結果如圖5所示。

圖5 條件觸發門與系統cost的關系

圖5(a)顯示攻擊者成功破壞系統所需最小cost（TEC，top event cost）隨條件觸發門參數（∈[0,1]）的變化。在較小時，先破壞表決存儲器使表決模塊被攻破能取得較大收益，從而TEC隨呈線性增長，而當大于0.7、0.8后（分別對應兩種控制律），破壞表決存儲器的收益過低，從而直接攻擊表決控制器反而能節省攻擊代價，全局攻擊代價變得與變化無關，故曲線呈水平。圖5(b)表示當設為0.3時，攻擊者成功破壞系統所需最小cost隨表決存儲器的cost值的變化，表決存儲器cost取值范圍為[100，300]。在表決存儲器的cost較小時，其作為條件觸發門的觸發事件影響著攻擊整個系統所需的cost，但在觸發事件cost增大到一定程度后，直接攻擊表決控制器反而能節省攻擊代價，因而曲線呈水平。

圖5(a)和圖5(b)反映出條件觸發門能夠正確建模相互關聯的攻擊事件。圖5(c)在降低Quad-Sim控制律計算模塊cost的情況下，觀察攻擊者成功破壞系統（及其模塊）所需最小cost隨條件觸發門參數的變化。圖5(c)中，CLC模塊的cost由于不受影響，因而為一條水平線，Voter模塊的cost則隨著的增大而呈與圖5(a)類似趨勢，飛控計算機（CS）的cost取值始終與兩者中較小的一方保持一致，且TE模塊cost變為水平線的轉折點（與CS相同）。證明了本文提出的基于SMT的最優化求解方法能夠正確分析得出攻擊系統所需的最小代價。

6 結束語

為了滿足當前計算機系統完整性的需求，針對當前信息流完整性量化模型的不足，本文將量化信息流完整性模型與攻擊樹的系統架構相關建模能力相結合，提出了完整性威脅樹并給出了完整性量化模型。在此基礎上，本文實現了一種基于SMT的最優化求解方法，用于分析攻擊系統所需的最小代價，以進一步分析系統威脅。最后，本文結合飛控雙余度計算機系統做了完整性分析，說明方法的實用性。

[1] DENNING D E. A lattice model of secure information flow[J]. Communications of the ACM, 1976, 19(5):236-243.

[2] BIBA K J. Integrity considerations for secure computer systems: technical report: ESD-TR-76-372[R]. 1977.

[3] 吳澤智, 陳性元, 楊智, 等. 信息流控制研究進展[J]. 軟件學報, 2017, 28(1): 135-159.

WU Z Z, CHEN X Y, YANG Z, et al. Survey on information flow control[J]. Journal of Software, 2017, 28(1): 135-159.

[4] MILLEN J K. Covert channel capacity[C]//IEEE Symposium on Security and Privacy. 1987: 60.

[5] CLARKSON M R, SCHNEIDER F B. Quantification of integrity[J]. Mathematical Structures in Computer Science, 2015, 25(2): 28-43.

[6] KORDY B, PIETRE-CAMBACEDES L, SCHWEITZER P. DAG-based attack and defense modeling: don’t miss the forest for the attack trees[J]. Computer Science Review, 2014, (13-14): 1-38.

[7] JHAWAR R, KORDY B, MAUW S, et al. Attack trees with sequential conjunction[C]//The 30th IFIP TC 11 International Conference, 2015:339-353.

[8] AUDINOT M, PINCHINAT S, KORDY B. Is my attack tree correct [C]//The 22nd European Symposium on Research in Computer Security. 2017: 83-102.

[9] HOME R, MAUW S, TIU A. Semantics for specialising attack trees based on linear logic[J]. Fundamenta Informaticae, 2017, 153(1-2): 57-86.

[10] SAMET R. Recovery device for real-time dual-redundant computer systems[J]. IEEE Transactions on Dependable and Secure Computing, 2010, 8(3):391-403.

[11] MAHONY R. KUMAR V. CORKE P. Multirotor aerial vehicles: modeling, estimation, and control of a quadrotor[J]. IEEE Robotics and Automation Magazine,2012,19(3):20-32.

[12] 張楊, 吳文海, 汪杰. 艦載無人機橫側向著艦控制律設計[J]. 航空學報, 2017, 38(S1):128-134.

ZHANG Y, WU W H, WANG J. Design of carrier UAV lateral/di rectional landing control law[J]. Acta Aeronautica ET Astronautica Sinica, 2017, 38(S1):128-134.

[13] HARTLEY E N, MACIEJOWSKI J M. A longitudinal flight control law based on robust MPC and H2 methods to accommodate sensor loss in the reconfigure Benchmark[J]. IFAC Papers Online, 2015, 48(21):1000-1005.

Information flow integrity measurement method using integrity threat tree

WU Qixuan1,2, MA Jianfeng1, SUN Cong1

1. School of Cyber Engineering, Xidian University, Xi’an 710071,China 2. Tencent Technology (Shenzhen) Company Limited, Shenzhen 518057, China

In order to avert the drawback of traditional information flow integrity analysis on ignoring the specific system architecture and associated attack events, an integrity threat tree to quantify the integrity of the system information flow, and the conditional trigger gate to model the associated attack events were proposed. The attack cost was used to quantify the degree of difficulty on attacking each channel. According to the architecture-related integrity threat tree, the minimum attack cost and corresponding target channel set required to achieve the attack target were solved by using the satisfiability modulo theories. The practicality of our approach was demonstrated by the modeling and analysis of the actual flight control system models, and the influence of the conditional trigger gate parameters on the system integrity was discussed.

integrity, information flow, satisfiability modulo theories, attack tree

The National Science Foundation of China (No.61872279)

TP309

A

10.11959/j.issn.2096-109x.2019016

吳奇烜（1992? ），男，陜西商洛人，西安電子科技大學碩士生，主要研究方向為系統可靠性分析、信息流安全。

馬建峰（1963? ），男，陜西西安人，博士，西安電子科技大學教授、博士生導師，主要研究方向為密碼學、網絡安全。

孫聰（1982? ），男，陜西興平人，博士，西安電子科技大學副教授、博士生導師，主要研究方向為信息流安全、可信軟件。

2018?10?10；

2019?01?20

孫聰，suncong@xidian.edu.cn

國家自然科學基金資助項目（No.61872279）

吳奇烜, 馬建峰, 孫聰. 采用完整性威脅樹的信息流完整性度量方法[J]. 網絡與信息安全學報, 2019, 5(2): 50-57.

WU Q X, MA J F, SUN C. Information flow integrity measurement method using integrity threat tree[J]. Chinese Journal of Network and Information Security, 2019, 5(2): 50-57.