基于冗余代码插入外部时间信道屏蔽的算法

张欢欢

(安徽工业大学计算机科学与技术学院，安徽马鞍山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 结语

时间信道一直以来都被认为是计算机信息安全最严峻的挑战之一，而外部时间信道由于其测量的难度，一直都是研究的难点。

本文提出了一种基于冗余代码插入的外部时间信道屏蔽方法，通过额外的计算得到与机密信息有关的条件分支和循环的执行时间，并根据得到的时间对含有机密信息的条件分支和循环进行冗余代码插入，从而消除外部观察者通过观察程序的执行时间而得到机密信息。给出了一种转化方法，并对其进行了证明。

今后的工作，会继续改进方法使其更加接近实用，并将其应用于开发程序。