搜索
您的当前位置:首页正文

可执行可信软件安全性分析技术研究

来源:小奈知识网
4802 201 0,3 1(22) ・信息安全技术・ 计算机工程与设计Computer Engineering and Design 可执行可信软件安全性分析技术研究 陈 楠, 王震宇, 窦增杰, 姚伟平, 余 弦 (解放军信息工程大学信息工程学院,河南郑州450002) 摘要:为了保证基于可信架构的可信软件的安全性,给出了可信软件安全性分析的总体架构及其工作原理。提出了一个 静态分析技术与动态测试技术相结合的有效机制,实现了静态分析和动态跟踪的交互协作,提高了安全分析的效率。设计 了一种可执行代码中间表示的方法,给出了建立程序存储空间抽象模型和程序抽象运行时刻环境的方法。详细地讨论了程 序的控制流和数据流分析技术,并给出了求解算法。最后,概述了程序动态测试系统。 关键词:可信软件;静态分析;动态测试;控制流分析;数据流分析 中图法分类号:TP309 文献标识码:A 文章编号:1000—7024(2010)22.4802 04 Research on security analysis techniques of trusted software binary executables CHEN Nan,WANG Zhen—yu, D0U Zeng-jie,YA0 Wei—ping,YU Xian (Institute of Information Engineering,PLA Information Engineering University,Zhengzhou 450002,China) Abstract:To ensure the security of the trusted software based on the trusted architecture,an overall architecture and the principle for trusted software security analysis are introduced.This architecture is characterized with coexistence ofstatic analysis and dynamic testing, as well as program attributes sharing.A simple intermediate representation of binary executables is presented.Program’S memo ̄ space abstract model is built and the run—time environment is described.Data flow analysis and control flow analysis are discussed in detail.Finally,the dynamic testing system is given. Key words:tusted sofrtware;static analysis;dynamic testing;control flow analysis;data flow analysis 0引 言 近年来可信计算技术在国内外都取得了长足发展,基于 可信计算技术的可信应用也越来越多。TCG对“可信”的定义 是:“一个实体在实现给定目标时,若其行为总是如同预期,则 该实体是可信的”…。可信计算的基本思想是:首先建立一个 信任根,再建立一条信任链,从信任根开始到硬件平台、到操 化验证和静态分析 。动态测试方法通过软件的实际执行来 发现软件中的错误。形式化验证使用定理证明和模型检验等 方法来验证程序是否符合特定的安全规则,从而判断程序是 否存在安全漏洞。静态分析方法通过对程序代码进行分析, 从语法、语义上理解程序的行为,直接分析程序的特征,寻找 可能导致错误的异常。 本文基于上述几种常见的安全分析技术,设计了可信软 作系统、再到应用,一级认证一级,一级信任一级,把这种信任 件安全分析总体框架。该框架提供了一个静态分析技术与动 态测试技术相结合的有效机制,可实现静态分析和动态跟踪 的交互协作。 扩展到整个计算机系统,从而保证了整个计算机系统的可信。 本文所提的可信软件就是基于可信架构的系统软件和应用软 件,如可信操作系统、可信编译、可信数据库和可信应用软件。 IEEE Computer Society Technical Committee on Dependable Com— 1可信软件安全性分析系统总体框架 本文提出的总体框架如图1所示。静态分析子系统主要 以静态安全性分析技术来实现对二进制代码的安全性分析。 动态分析子系统主要通过构建测试用例,并对二进制代码实 施跟踪调试捕获异常来测试安全性。 puting认为,所谓可信是指计算机系统所提供的服务是可以论 证其是可信赖的,即不仅计算机系统所提供的服务是可信赖 的,而且这种可信赖还是可论证的 。武汉大学张焕国教授提 出:可信 安全+可靠 。这些观点都说明了可信系统和可信 软件首先必须保证其安全性。 目前,软件安全性检测主要有3类方法:动态测试、形式 收稿日期:2009.12—02;修订日期:2010—02—2O。 功能模型组织的是待分析对象的各类程序属性,静态分 析子系统和动态分析子系统均将各自分析得到的程序属性存 基金项目:国家863高技术研究发展计划基金项目(2o07AAO1z483);河南省科技创新基金项目(082102210011)。 作者简介:陈楠(1985--),男,河北邢台人,硕士研究生,研究方向为信息安全、可信计算; 王震宇(1969一),男,副教授,硕士生导师,研 究方向为信息安全、可信计算、嵌入式系统; 窦增杰(1983--),男,硕士研究生,研究方向为信息安全; 姚伟平(1983~),男,硕士研究生, 研究方向为信息安全; 余弦(198O一),男,研究方向为软件工程。E—mail:xdchennan123@163.corn 陈楠,王震宇,窦增杰,等:可执行可信软件安全性分析技术研究 2010,31(22)4803 抽象处理及 可视化子系统 交 互 XML中间结果 子 系 统 、,f,一 t  I抽象处理 』 可视化 图l 可信软件安全性分析系统总体架构 入该功能模型中,待分析目标的功能模型随着动静态分析过 程不断调整细化。该系统中,安全性分析工作与待分析目标 的功能模型调整细化这两个过程相互作用和不断迭代,一方 象表示、可执行代码运行时刻环境抽象表示、控制流和数据 流分析。 2.1可执行代码抽象表示 为了分析的简洁性和严密性,需要把可执行文件反汇编 面使得功能模型更加完善与具体化,另一方面也使得安全性 分析工作更具有针对性,从而大大提高了安全性分析工作的 效率和准确率。 可信软件安全分析系统按功能可划分为4个子系统,分 结果转化成一种易于后续数据流分析和控制流分析的中间 表示形式。在可执行程序分析中引入汇编语言中间表示,有 助于降低反汇编结果的复杂性,提高可执行程序分析的效率。 汇编语言中间表示并没有一个固定的格式,只是为了便于分 别是交互子系统、静态分析子系统、动态分析子系统和抽象处 理及显示子系统。 交互子系统主要负责与用户的交互,如为静态分析提供 入口点信息,为动态分析提供断点信息等。 静态分析子系统主要负责静态分析。它的主要工作包括 析汇编代码提供一个简化的表示形式。汇编语言中间表示在 语义上完全等价于二进制代码,也就是说根据中间表示的语 义执行结果和真实执行二进制代码产生的结果是一样的。本 文设计的中间语言的语法,该语法使用BNF(巴科斯.诺尔范 式)的一种变形形式 ,如图2所示。中间语言表示的每条指 令都有一个对应的标号来标识这条指令,程序的标号集合定 义为Lab。 代码反汇编、简化汇编语言中间形式表示、二进制结构化语义 提取、二进制代码存储空间抽象表示、程序运行时刻环境的描 述、基于抽象解释的程序属性和安全性分析等。 动态分析_f系统主要负责动态分析,它的主要工作包 括根据功能模型中的程序控制流和程序属性等信息产生测 试用例和测试策略,动态执行过程中程序执行路径和数据 流分析,记录函数和程序块的动态执行次数(即动态扇入扇 出度),自动识别调试器的输出信息(包括断点、堆栈、变量、 寄存器等)等。 抽象处理和显示子系统负责对静态分析和动态分析产生 的中间结果进行处理。它的主要工作包括显示函数调用关系 图2中间语言语法 图和程序控制流程图,查看调试状态信息(包括断点、堆栈、变 量、寄存器等),查看函数和程序块的静态扇入扇出度、动态扇 入扇出度等。 图2中,n表示立即数,I表示立即数,P表示程序,ga(I)表 示指令的幂集,1Elab为程序指令对应的标号,o 为二元运算 符,0 为一元运算符,另外 ()表示对内存单元的读取。 2可信软件静态分析系统 静态分析通过对程序代码进行分析,从语法、语义上 2.2可执行代码运行时刻环境抽象表示 2.2.1抽象存储空间的建立 本文假设每一个正在执行的程序可看作是在它的逻辑地 址空间上运行,程序逻辑地址空间由以下区域组成: (1)代码区:存放可执行的目标代码; 理解程序的行为,直接分析程序的特征,寻找可能导致错 误的异常。静态分析主要包括代码反汇编、可执行代码抽 4804 2010,3 1(22) 计算机工程与设计Computer Engineering and Design 数值集合。 (2)静态数据区:存放所有初始化和未初始化的全局变量 和编译器产生的其它数据; (3)堆区:存放程序运行时刻分配和释放的数据; (4)栈区:存放过程的活动记录。 为了分析方便,根据各区域的实际特性以及上述4种区 2.3控制流分析 可执行代码控制流分析分为控制流恢复和控制流结构 化。控制流恢复是指从汇编代码中恢复出程序的执行路径。 控制流结构化则指将控制流图表示的程序转换成用循环、分 支等结构组成的程序 ,程序控制流分为过程内的控制流和过 域特点把逻辑空间划分为互不相关的存储区域并分别建立抽 象存储模型。从而,程序存储空问抽象模型不再是简单的一 维地址空间,其包含了4类抽象域:抽象代码域(记为AD 栈域(AD Stack)。 Code)、抽象静态数据域(AD Data)、抽象堆域(AD Heap) ̄1]抽象 如图3所示,针对一个可执行文件,其抽象存储空间模型 程问的控制流。控制流分析就是得到程序的执行序列,在程 序执行序列的基础上划分基本块,分析过程间的调用关系。以 基本块为节点构造程序的控制流程图,根据过程调用关系得 到过程调用图。 定义3过程调用图 ~一一一一一一一 包含了一个抽象代码域,一个抽象静态数据域,根据情况会有 若干个抽象堆域和若干个抽象栈域。 _鬣 图3程序抽象存储空间模型的基本构成 2.2.2程序运行时刻环境的抽象表示方法 程序状态的表示形式为 ̄rEState=Var ̄Z。定义变量集合 Var ̄registerUg—varuf_varuh—var。其中,register表示寄存器变 量集合,g_var表示全局变量集合,fvar表示局部变量集合,h_ var表示堆变量集合。 变量取值表示形式会影响分析算法尤其是对内存区域的 分析的精确性。一个变量所需要的存储空间大小是由其类型 决定的,为了很好的处理不同字节内存读写操作,需要设计相 应精确的数值表示方式。区间域和同余域是典型的数值表示 方法,但是区间域、同余域的算术运算不能很好的表示内存访 问粒度(例如对双字,字,字节类型数据操作的幅度区间不同), 本文用带跨度的区间域sI来表示数值的表示形式。sI拥有区 间域和同余域的优点,既能表示数值的范围的又能表示数值 的变化幅度 。 定义1 Ix] 表示 rood m的同余类,定义 ] {x+ixmI f∈z)。 定义2对于k位的SI: (,’“)表示下列整数集合:y [f,“])= (f∈[一2 ,2 ]ll<i<u,iE[.『] )。 对于SI: (1)s表示数值每次变化多少: (2)[,, ]为区间域; (3)o[t,f]表示集合Ⅲ。 由此程序运行时刻环境抽象表示为: Var--vs,vsg(SI ̄x (SI )n)×(sI )“)。 SIG表示抽象静态数据域中全局数据的数值集合(也表示 数值域),sI 表示函数栈空间的变量的偏移取值集合,sIu表示 函数堆区问的数值集合,(sI口) =sI,'x…xSIp 表示n个栈区间的 可执行文件可以表示为一个包含“图”的有向图G:=(F,E), G称作过程调用图。过程调用图的节点集合为F:={f1, ,…, 血},fi为可执行文件的过程。E表示边的集合,如果(if,巧)∈E 则表示fi调用了fj。 定义4控制流图 对于过程调用图中的每个过程fi本身也是有向图,称作 控制流图G:=(B,E),其中B:={bl,b2,…,bm}表示基本块的 集合。E表示边的集合,如果存在(bi,bj)∈E,则表示一条从基 本块bi到bj的控制流。每一个过程的控制流图都只有一个入 口(入度为0的点),但可以有多个出口(出度为0的点)。 定义5基本块 基本块是一个由连续的指令组成的序列,控制流从基本 块的开始处进入,从基本块的出口流出,控制流在基本块内部 不会停止也不会出现分支,直到基本块的最后一条指令。过 程的基本块的划分规则为:两条相邻的指令在同一个基本块 中当且仅当前一条指令执行后,后一条指令必须执行。 汇编语言控制结构简单,其控制流信息可以直接通过以 下3个函数获得: (1)函数init:l ̄Lab返回指令集合I的初始标号; (2)函数 口 一 (Lab)返回指令结束标号的集合(F): (3)定义函数,zDw.,一 (LabxLab)计算程序指令的控制流信 息,该信息反映了程序指令的执行先后顺序,例如(,。,厶)表示控 制会从, 直接到厶。 通过这3个函数就可以构造程序的控制流图。 2.4数据流分析 数据流分析通过静态分析程序的结构以及静态收集程序 中各个变量的引用情况来建立数据流方程,对数据流方程进 行求解以得到程序的属性信息 。数据流分析是通过对格的 运算来完成的,格中的元素可以抽象地表示程序的变量、表达 式的性质或者是变量的取值等程序属性。格到格自身的映射 函数厂:三一 称为流函数。 在数据流分析的时候,数据流信息抽象表示为格值并通 过流函数对格值进行运算。流函数通过格到格自身的映射来 模拟程序的运行状态。数据流分析是沿着程序控制流执行序 列来进行的,定义流图G(N,F),其中N表示程序指令对应的 结点,F为程序的执行流。 对于一个程序流图G(N,F)和格L,以前向数据流分析为 例,对于每个节点rl: 陈楠,王震字,窦增杰,等:可执行可信软件安全性分析技术研究 ——2010,31(22)4805 节点n之前程序点的属性集合,即n的入口处的 关键数据结构的依赖关系来指导程序动态执行时候测试的路 径选择策略。在程序动态执行的时候对指令进行记录,自动 分析记录的数据,来指导静态值范围及数据依赖关系分析。这 样的过程反复迭代指导得到最优的测试路径为止。 (2)路径约束条件的求解及测试集合的生成 数据流信息。 Du ——节点n之后程序点的属性集合,即n的出口处 的数据流信息。 ——节点n的流函数, 根据1N.计算OUT.。 数据流分析对所有的nEN,计算1No和OUT.,其中1N.EL, 通过程序仿真机制对记录的程序执行指令序列进行分析 OUT.EL。定义数据流方程如下 r, 咒=entry 'NoL ̄o I ))其它 DU = ( ) 式中:卜程序开始结点的初始值,通常是T或者上。pred(n) 表示节点n的前驱。 表示与节点n对应的流函数,u为节点 的汇合函数。 数据流方程的求解算法如图4所示。 图4数据流方程求解迭代算法 3可信软件动态测试系统概述 动态测试通过软件的实际执行来发现软件中的错误。动 态测试的主要工作包括动态执行过程中程序执行路径、函数 和程序块的动态执行次数的跟踪记录,根据功能模型中的基 于程序抽象运行时刻环境得到的程序控制流和程序数据流等 信息产生测试用例和测试策略等。 3.1安全性动态测试的程序仿真机制 程序动态执行过程的指令级跟踪与记录是动态安全分析 最基础部分。用于安全性动态测试的程序仿真机制应在不影 响被监控程序正常执行的条件下,记录程序的动态执行轨迹, 记录中间运行环境,进一步分析程序的各类属性。 (1)路径选择策略 根据静态分析得到程序每个执行点变量的取值范围以及 和化简,结合数据流分析明确各条件转移分支与输入变量之 间的依赖关系,进而完成约束条件的收集与表示。依据路径 选择策略对当前路径对应的约束集进行部分修改,以引导程 序向新的路径执行。利用约束求解引擎对修改后的约束集进 行优化、化简并求解,生成新的输入测试数据。此过程反复操 作,直到程序执行到目标路径或者目标状态为止。 3.2基于测试集动态生成技术 获得的程序动静态属性,用以对程序执行时收集并优化 了的路径约束条件进行求解,生成新的输入测试数据。程序 仿真调试机制记录程序的动态执行路径,在各断点上采集实 际运行环境,获取约束条件,实际运行环境与程序的抽象表示 结合,进一步分析关键数据结构及其取值范围等属性。结合 程序执行记录和实际运行环境抽象基础上,给出程序属性的 动态分析过程和程序执行过程的回放机制。 4结束语 本文重点介绍了可信软件可执行代码的安全性的方法和 技术,该技术不依赖源代码,直接针对可信软件的可执行代码 来进行安全性分析验证。提出了一种汇编中间表示,保证了 分析的简洁性和严密性,给出了可执行代码运行时刻抽象环 境的表示方法,在此基础上进行控制流和数据流分析可得到 程序运行时刻环境以指导程序的动态测试。 参考文献: 【1]Trusted Computing Group.TCG speciifcation architecture over- view[EB/OL].https://www.trustedcomputinggroup.org/groups/ TCG1 rchitecture Overview pd ̄2007—08—02. 【2】 Avizienis A,Laprie J C,Randell B,et a1.Basic concepts and taxo— nomy of dependable nad secure computing[C].IEEE Trnas De— pendable Secur Comput,2004:1 1-33. [3】 张焕国,覃中平,刘毅,等.一种新的可信平台模块[J].武汉大学 学报(信息科学版),2008,33(10):991—993. 【4] 夏一民,罗军,张民选.基于静态分析的安全漏洞检测技术研究 [J]_计算机科学,2006,33(10):279.282. [5] Glynn Winske1.程序设计语言的形式语义【M】.北京:机械工业 出版社,2004:9—11. [6]Balakrishnan G.WYSINWYX:What you see is not what you exe— cute[D].University ofWisconsin,2007. [7] 曹孟春.反编译器自动评测与中间代码生成研究[D].合肥:中 国科学技术大学,2008. [8] Alrfed V Aho,Monica S Lam,Ravi Sethi,et a1.编译原理【M].北 京:机械工业出版社,2009:338.342. 

因篇幅问题不能全部显示,请点此查看更多更全内容

Top