基于冗余代碼插入外部時間信道屏蔽的算法

張歡歡

(安徽工業大學計算機科學與技術學院，安徽馬鞍山243032)

0 引言

隨著計算機和網絡技術的迅猛發展，保障計算機和網絡上的信息安全性變得越來越重要。但是，傳統保障信息安全的機制仍存在缺陷，不能夠充分保障信息端到端的安全。D.E.Denning首先提出了信息流的概念，信息流是指若存儲在對象y(源頭)中的信息直接或間接地影響x(目標)，則對象y和x之間存在信息流。D.E.Bell和L.J.LaPadula提出并描述了安全信息流。J.Goguen和J.Meseguer也分別闡明了程序訪問的安全信息流特性。程序的信息流安全是信息流安全的一個重要研究方向。[1]事實上，攻擊者可以以多種不同方式獲取機密信息或者隱私信息：直接泄密(最簡單且直截了當的泄密方式)，直接將機密信息傳給攻擊者；間接泄密(有時候也稱為隱蔽存儲信道)，機密信息被編碼在可觀察程序行為的程序中，程序可能根據機密數據的數據值不同而執行不同的數據訪問；時間泄密(或者通過一個隱蔽時間信道)，當程序將機密數據編碼在與時間有關的行為時，或攻擊者通過在一個特定時間間隔期間測量資源的可用性從而可以觀察操作方式來操作共享資源時，時間泄密就會發生了。程序也可能通過其終止行為泄密信息。例如，當機密數據滿足一些條件時，程序就正常終止或者進入無限循環，可以認為通過非終止泄密是一個特殊的時間泄密情況。[2]外部時間隱蔽信道已經被用于在實踐中泄露信息和打破密碼系統。[3]現有緩解外部時間信道的機制，對于基于語言的信息流來說那些之前的機制在應用中是非常受限的。現提出基于冗余代碼插入來平衡時間差，經過轉換規則轉換的代碼，攻擊者不能通過測量執行與機密信息有關的操作時間來得到機密信息。

1 命令式語言：語法和操作語義

命令式語言SIPL(Simple Imperative Programming Language)作為本文討論方法的載體，以下分別給出其語法和操作語義。SIPL語法和語義的定義參考了文獻[4]～文獻[5]的部分內容。

1.1 語法

SIPL語法包括表達式和命令，其BNF范式如下：

e∷=(表達式)

n(整型)

υ(變量)

！(非)

c∷=(命令)

υ∶=e|skip|skip(n)|

ifethenc1elsec2

whileedoc

語法說明：本文所使用的表達式和命令的語法構件與常見的命令式語言相同,以下僅給出必要的解釋和假設，如skip(n)表示有n個skip (n為2時：skip;skip)。

1.2 操作語義

為定義SIPL的操作語義，需要一個表達存儲狀態的函數σ:υ→(?υ,συ無定義)，它是變量名集合υ到自然數的函數。其次是表達式的語義函數，其歸納定義如下：

為了簡化對執行時間的計算，定義了函數τ。τ(e)，表示執行表達式e所需要的時間單位數；τ(c)，表示執行命令c所需要的時間單位數。

單位時間是指基于Intel core i7的一個指令周期。[5]

SIPL命令(線程)的操作語義是通過程序格局上的遷移關系“→”來定義的,格局G是一個三元組(c,σ,κ),其中：c是當前正要執行的命令;σ是程序的狀態;κ(κ∈)是多少個時間單位。SIPL命令的結構化操作語義定義如下。

1)if條件分支

(skip,σ,κ)→(_,σ,κ)

(x∷=e,σ,κ)→(_,σ[x|→eσ],κ+τ(e)+1)

2)while循環和sequence

2 轉換規則

給出的轉換規則包括以下算法1、算法2和算法3。算法中加粗字體是語法元素，而其他語法元素是源程序中的語句。

為了保證程序的安全，雖然給出的算法在一定程度上對程序的執行時間產生了影響，但并不會影響源程序的語義，而且隨著處理器能力的提升，產生的時間影響是可以接受的。

2.1 轉換規則

1)算法1 轉換規則

//輸入：可以通過外部事件泄漏信息的源程序p

//輸出：攻擊者不能通過外部事件得到機密信息的程序

① Trans(p){

②ifpiscthen//單條命令

③ifpis skipthenp

④ifpis assignmentthenp

⑤ifpis cond-branchthenBasicF(p)//算法2，條件分支的處理

⑥ifpis while-loopthenBasicW(p)//算法3，while循環的處理

⑦elseifpisc1;c2thenTrans(c1);Trans(c2);//組合命令

⑧}

2)算法2 條件分支的處理

① BasicF(ifethenc1elsec2){

②ife不包含機密信息then

③returnifethenc1elsec2; //源程序無需改變

④elseife包含機密信息then

⑤ifc1是基本表達式then

⑥t1←τ(c1)

⑦ifc2是基本表達式then

⑧t2←τ(c2)

⑨ift1>t2then

⑩returnifethenc1else{c2;skip(t1-t2) };//在源碼中添加冗余代碼

//嵌套的處理

3)算法3 while循環的處理

① BasicW(whileedoc){

②ife不含敏感信息then

③returnwhileedoc;//源程序無需處理

④elsee含敏感信息then

⑤e′=e;//防止在c中會改變e

⑥ifc是基本表達式then;//通過在源程序添加冗余代碼來平衡時間

⑦returnwhileedoc;while !e′ doc′;

⑧ifc含有while循環thenBasicW(c);

⑨ifc含有條件分支thenBasicIF(c);

⑩}

算法說明：c′為c的影子，并且在c′中使用新的變量稱為影子變量(例如算法3中的e′)。將c中的賦值使用影子變量進行重新賦值，類似加減乘除操作。同樣使用影子變量進行再次操作，不影響源程序語義的同時彌補時間以消除外部時間泄漏機密信息。

2.2 實例分析

1)實例1

secret = 0;

i = 0;

while(i < 10000){

if(i%2 == 0){

secret +=1;

}

i++;

}

假設secret為機密變量，例中執行時間主要在while循環中，而while循環的執行時間又都在if分支中，if分支中存在機密變量的計算。攻擊者可以根據if分支的執行時間而得到機密變量secret的值。

secret = 0;

i = 0;

while(i < 10000){

if(i%2 == 0){

secret += 1;

}else{ //平衡時間

skip;//加操作占用1個時間單位

}

i++;

}

例中代碼段是對源程序進行轉換后的源碼，通過添加冗余代碼，使得if分支和else分支的執行時間相同，攻擊者不再能夠根據程序的執行時間而得到機密變量值。

2)實例2

sum = 1;

if( h == 1){

while (h<101){

sum = sum + 1;

}

} else {

sum = 5000;

}

假設h為高級別機密變量，由于if分支和else分支的執行時間相差很大，攻擊者可以根據條件分支的結束時間得到機密變量h的值。

sum = 1;

sum′ = 1;

h′ = h;

if( h == 1){

while (h < 101){

sum = sum + 1;

}

} else {

sum = 5000;

while(h′ < 101){

sum′ += 1;

}

}

通過轉換的程序可以平衡掉if分支和else分支的時間差。通過添加影子變量的形式為源程序作出轉換，根據源程序的時間差添加冗余代碼。這樣就不能通過觀察if分支和else分支的執行時間得到高級別機密變量的值，以達到保護機密變量的目的。

3 證明

對于給定的程序c，分下面2種情況進行證明。

1)情況1

?σ,?κ

(Trans(c),σ,0)→(_,σ′,κ)

(Trans(c),σ,0)→(_,σ′,κ′)

有κ=κ′

對于給定的程序，從開始執行到結束也許有多條路徑。程序的執行時間可能根據不同的路徑而不同。經過轉換規則進行轉換的源碼，只要是能正常結束，那么無論走哪條路徑，其執行時間是相同的。

2)情況2

如果轉換的程序有一條路徑不能執行結束，那么對于任意一條執行路徑都是不能終止的。

4 相關研究

Smith和Volpano在文獻[6]中描述了通過禁止那些依賴于機密數據的循環來解決終止信道的類型系統，形式化了Timing agreement理論。Timing agreement理論指出擁有獨立于高級數據的循環和分支條件的順序程序將會執行在lock-step中。而lock-step具有環境的低安全部分獨立于高安全級別數據。但是他們并沒有處理時間泄漏，而是以一種靈活的方式泄漏給外部觀察者。

Agat在文獻[2]中描述一個代碼轉化的方法。通過冗余計算來填充程序移除外部時間泄露，并且通過禁止在機密數據上循環來避免終止信道。Agat′s轉變的一個缺點：如果有一個條件上有機密數據，并且只有其中一個分支是非終止的，轉換后的程序就是非終止的。

外部緩解是另一種控制外部時間信道的方法，它們通過定量限制多少信息通過外部事件交互泄漏。[7]但是由于外部緩解將計算看作黑盒，因此并不能區分良性時間變量和泄漏信息的變量。當多數變量是良性變量時，將導致效率明顯地下降。

文獻[8]提出了一種基于語言的緩解方法。使用mitigate原語擴展簡單的While-language，他們的工作依賴于靜態注釋來提供有關底層硬件信息。

5 結語

時間信道一直以來都被認為是計算機信息安全最嚴峻的挑戰之一，而外部時間信道由于其測量的難度，一直都是研究的難點。

本文提出了一種基于冗余代碼插入的外部時間信道屏蔽方法，通過額外的計算得到與機密信息有關的條件分支和循環的執行時間，并根據得到的時間對含有機密信息的條件分支和循環進行冗余代碼插入，從而消除外部觀察者通過觀察程序的執行時間而得到機密信息。給出了一種轉化方法，并對其進行了證明。

今后的工作，會繼續改進方法使其更加接近實用，并將其應用于開發程序。