郑伟宁,庄 毅,顾浩为
(1.南京航空航天大学计算机科学与技术学院,江苏 南京 211106; 2.中华中学,江苏 南京 211106)
在计算机运行过程中,因为信号或者数据不正确造成的故障被称为软错误[1]。导致软错误的原因有多种,从电路设计出现问题到元件之间相互干扰,乃至于空间辐射均有可能造成软错误[2]。软错误会改变寄存器或数据存储器中的值,从而导致处理器将程序带入错误循环或者直接进入死循环无法跳出。虽然软错误通常不会对硬件电路造成永久性损坏,但仍会造成严重的后果。比如,2000年,美国SUN UNIX因缓存出现软错误而影响了全美数十个服务器的正常工作,造成了数百万美元的经济损失;2011年,我国首颗火星探测卫星“萤火一号”升空后,由于负责运载的俄方Fregat上级控制系统遭受空间粒子辐射诱发软错误,致使火星探测失败。在其他领域,如工业生产、民用设施,软错误也在不同程度上影响了电子设备的正常运行,降低了系统的可靠性。而根据应用场景的不同,对计算机的可靠性要求也不相同。例如发生在卫星控制系统上的错误比发生在视频游戏中的错误造成的后果更加严重。因此,在设计加固方案时需要综合考虑应用场景、加固效果、需求成本等多方面因素。所以在性能受限的平台上,及时有效地对软错误进行检测恢复,针对计算机系统进行软错误加固,减少故障的发生以提高系统的可靠性具有重要的意义。开发一种能够有效检测软件中软错误,同时检测成本较低,可以被接受的检测系统,也是目前的研究重点。
本文着眼于解决软错误中控制流错误的检测问题。程序控制流错误是软错误的一大类型,根据Zhu等人[3]和Ohlsson等人[4]的实验结果可知,在程序发生的软错误中,有33%~77%的可能性造成程序的控制流错误。当高能粒子在与程序调用地址相关的位置引发故障时,就有可能造成控制流错误[5]。对于任何计算机程序,只要给程序输入,其内部执行指令的顺序就是固定的,但是控制流错误会改变这种顺序,从而影响程序的正确执行[6]。目前检测控制流错误的软件技术通常是维护并更新一个全局的动态变量,通过监测变量的变化间接监控程序的控制流,这一变量也就是标签。这种技术也被称为基于标签实现的控制流错误检测技术[7]。
目前国内外对控制流检测技术已经有了许多研究成果。Yau等人[8]在1980年提过一种使用数据库来记录程序控制流的方法,但是这种方法需要维护一个数据库且不同程序控制流信息不同,最终会导致数据库不断扩充,开销太高。该方法虽然本身存在着局限性,但是它提出了一种程序无循环间隔的概念,这一概念就是程序基本块划分的前身。ECCA(Enhanced Control-flow Checking using Assertions)也属于早期软件实现的控制流错误检测方法,该方法通过在程序无分支间隔的入口和出口处插桩断言来检测错误[9]。此文献中的无分支间隔和断言与后来的基本块和标签已经非常接近了,但是由于更新操作采用乘除法,并且插桩的断言本身较为复杂,会产生较大的开销。CFCSS(Control-Flow Checking by Software Signatures)是基于标签实现的控制流错误检测方法中最为经典的方法,它将程序执行的指令划分为众多集合,并以此正式提出了基本块的概念。CFCSS将程序划分为基本块后,通过对每一基本块分配唯一的标签并添加错误检测指令来实现控制流错误检测。作为早期以纯软件方法实现的控制流错误检测技术之一,它有着重要的参考比较价值[10]。
目前主流的控制流错误检测方法大多是基于标签实现的方法,不同方法之间的主要区别在于标签设置的数量、标签更新的方式以及标签比较的位置。Vemu等人[11]提出的CEDA(Control-flow Error Detection using Assertions)就属于标签控制流错误检测技术中表现出色的一种。CEDA继承了部分CFCSS的特性,在每一基本块的入口和出口处添加了标签更新与验证体系,展现出了不错的性能。Chielle等人在CEDA和一种偏硬件的方法HETA[12]的基础上提出了S-SETA[13](Selective Software-only Error-detection Technique using Assertions)方法。S-SETA和CEDA较为相似,利用双层标签机制,通过基本块之间的关联性来计算更新运行时的标签。Zhu等人[14]提出了一种双标签的控制流错误检测方法RCFC (Regularized Control Flow Checking algorithm)。该方法无论是开销还是检测性能上均不太理想,但是其提出的双标签机制却提供了一种新的思路。在检测性能要求较高但开销可以放松限制的情况下,双标签机制就是一种能有效提高错误检测率的手段。国内对基于标签的控制流错误检测方法也有了较为深入的研究。张鹏等人[15]提出了一种使用双指令环设计标签的SSCFC(Structural Signatures for Control Flow Checking)技术,该技术通过引入的双指令环可以有效地解决块间滞后性和配置不灵活的缺点。李爱国等人[16]提出了能够记录基本块关系的RSCFC(Relationship Signatures for Control Flow Checking)技术。RSCFC和其他的标签控制流检测技术不同,它的基本块在设计上可以将基跳转关系直接编码进来,间接地节省了标签更新语句和标签检查语句的开销。但是该方法对于基本块总数有要求,严格受到了机器字长的限制,使算法的灵活性受到了极大的影响,难以在大体量程序上使用。张倩雯[17]提出了名为CEDBR(Control-flow Error Detection based on Basic-block Repartition)的双标签控制流错误检测技术,该方法有完善的规则和算法设计,有效地提高了错误检错率,是一种较为成熟的双标签算法。帕尔哈提江·斯迪克等人[18]通过分析程序控制流,限制间接调用函数的方法来降低调用指令的数量,再加上一种二进制的检查代码,从而达到检测目的。姬秀娟等人[19]基于程序控制流程图设计了一种基于投影的模型检测静态分析算法,来提高错误检测的有效性和准确率。
目前大部分基于标签的控制流错误检测方法的原理大体相似,只是标签设计的结构、规则和位置有所不同,各个方法的检测率与时空开销的差异也来源于此,就目前而言,基于标签的控制流检测算法普遍存在着开销与漏检率矛盾的问题,如何权衡两者以达到最好的检测效果,是本文研究的重点。本文对已有的控制流方法进行改进,提出一种多层分段标签控制流检测方法CFMSL(Control Flow detection method based on Muti-layer Segmented Labels)。
目前已有的面向软件的控制流错误检测方法大多需要依靠程序控制流程图[20],它由基本块及基本块之间跳转关系构成的二元组组成。本文借用LLVM[21](Low Level Virtual Machine)平台及相关图片生成工具,实现程序控制流程实体化,并成功嵌入到程序加固系统中。相关定义如下:
定义1基本块(Basicblock, b)是一组满足特定条件的最小有序指令集合,记为b={Iin,…,Ii,…,Ibra}。基本块内部除去最后一条指令外,没有其它的跳转指令。
定义2控制流(Control-flow, CF)为软件运行时基本块之间的跳转顺序。一般来说,这种跳转顺序是固定不变的,一旦发生改变就有可能产生控制流错误。本文定义控制流为E={eij|1i,jn},其中eij为bi到bj之间的跳转边,n代表了整个程序中基本块的总数量。
定义3任意一个程序均可表示为程序控制流程图(Program control-flow Graph, PG),由二元组PG=〈B,E〉表示。其中B={bin,…,bi,…,bend}代表程序基本块的集合,E={eij|1i,jn}则代表了程序的控制流。
定义4前驱是指程序控制流中任意一段跳转关系的起点基本块,前驱集合是指基本块所有前驱基本块的集合,本文使用pred来表示,如果eij∈E,则bi∈pred(bj)。与前驱集合不同,前驱序列是一种基本块有序集合。某基本块的前驱序列是指在程序的某一条控制流中,按照执行顺序所有处于该基本块前方的基本块集合,并依照与该基本块的距离从近至远排序。如控制流{b1→b2→b3→b4}中,b4的前驱序列为{b3,b2,b1}。
定义5与前驱对应,后继是指程序控制流跳转时的终点基本块。后继集合是指基本块所有后继基本块的集合,本文使用succ来表示。如果eij∈E,则bj∈succ(bi)。
定义6软件运行时因软错误导致软件发生错误跳转,这种软件错误被称为控制流错误。设指令Ii∈bi={Ii1,Ii2,…,Iiend},在程序中存在指令Ii→Ij之间的合法跳转,则指令Ij需满足以下2个条件:1)若i 定义7至多只有一个前驱且至多只有一个后继的基本块为O型基本块,记为TO。基本块若不是O型,则为M型,记为TM。 定义8本文为每一个基本块匹配一个具有唯一性的标签,称为基本块标签,记为BS。当程序正确执行时,动态全局标签需要与其相等。 定义9程序运行时有一个全局动态标签,会根据相应的标签规则进行动态更新,记为GS。当程序正确执行时,更新后的GS要与BS相等。 定义10差值参数主要用于更新全局动态标签GS,使程序在正确执行时,GS能更新成期望值BS。本文使用d来表示差值参数,如d(bi)代表的是基本块bi的差值参数。 定义11层级是一组非空基本块的集合,记为Lv。以M型基本块为核心,所有该M型基本块的前驱序列中从头至尾连续的O型基本块和该M型基本块处于同一层级,直至遇到另一个M型基本块为止。基本块可以同时属于多个层级。 定义12基本块多前驱矛盾是指当一个基本块同时具备多个前驱时,不同前驱跳转至同一基本块需要让不同标签值通过同一更新语句获得同一标签值。但标签具有唯一性,标签更新语句也大多结果唯一,这种唯一性与上述要求产生了矛盾。 图1以数据管理系统的部分逻辑代码为例,给出上述程序控制流相关定义的进一步说明。图1(a)为由if语句实现跳转的示例代码。图1(b)为源代码级基本块划分图。图1(c)为程序控制流程图PG,整个程序由%0、%9、%10和%11这4个基本块构成,分别记为b1、b2、b3、b4,其中b1、b4为M型基本块,b2、b3为O型基本块。依照程序正常执行流程,基本块b1的后继为b2和b3。由于程序内变量b为0~3之间的随机数,与a之间的比较结果随机,故跳转至b2或b3均为正常控制流。若程序执行过程中受软错误影响发生错误跳转,如图1(b)中由b1跳至b4,此时变量c的值仍为0,发生控制流错误。 (d) 程序控制流相关定义 依照定义7将基本块分为2类,M型基本块与O型基本块。本文设计的分层标签需要程序满足一种特定的控制流跳转规律:2个M型基本块不可连续执行,后文将这条规律称为M不连续原则。以此为基础设计标签生成、更新及校验规则。不满足跳转规律的程序,需要使用基本块按层次划分规则来改变程序控制流结构。 规则1若程序中存在一条控制流,其中有2个M型基本块连在一起,则替换其原本跳转路径,在二者之间插入1个空基本块。 规则2以M型基本块为核心,所有该M型基本块的前驱序列中从头至尾连续的O型基本块和该M型基本划分为同一层,直至遇到另一个M型基本块为止。对于任意一个程序,若入口基本块为M型基本块,则将其单独划分为一个层级。若入口基本块为O型基本块,则将之归入程序流中的第一个M型基本块所处的层级。 引理1通过规则1对程序控制流重构后,得到的新程序控制流程图中,不存在可以连续执行2个M型基本块的控制流。即:∀bi∈B,若bi∈TM,则(succ(bi)⊂TO)∨(pred(bi)⊂TO)。 证明:对∀bi∈TM,若∃bj∈succ(bi)⊂TM,则根据规则1调整,必∃bp∈TO,使得bp∈pred(bj),bp∈succ(bi)且bi∉pred(bj),bj∉succ(bi),这与bj∈succ(bi)产生矛盾。因此,任何经过规则1调整后的程序,一定不存在可以连续执行2个M型基本块的控制流。 图2为基本块层次划分规则应用的典型情况。其中,图2(a)和图2(b)分别对应规则1与规则2。虚线所代表的基本块表示新插入的空基本块。图2(a)中b1和b2均为M型基本块,整个程序有2条控制流{b1→b2}与{b1→b3→b2},前者不满足M不连续原则,故根据规则1插入空基本块bp以重构控制流。图2(b)中有一条控制流从b4又跳回了b1,导致b1同时归属2个层级Lv1和Lv3。 图2 基本块按层次划分示例 本文采用静态标签[22]插桩技术,插桩全局动态标签GS(Global Signature),使程序执行时连续地更新GS,并随时检查标签以监视程序的运行状态。这一过程可以被概括地分成3个阶段:标签分配阶段、标签更新阶段以及标签检查阶段。标签分配阶段会为程序中的每一基本块静态地计算并分配基本块标签值;标签更新阶段根据标签分配规则为每一基本块添加标签更新语句,使程序正确运行时得到正确的标签。标签检查阶段在基本块内部添加检查指令,以保证发生标签错误时可以尽早检测出来。 本文设计了用于标签分配的具体规则,给出了相关定理,为了方便描述,引入下列术语: 1位&1位集合:1位是指本文所设计的二进制标签中数值为1的位置(位数从1开始,并且从右向左计算),1位集合是指标签中所有1位的集合,本文中将1位集合表示为1set。如:011的1位集合为{1,2},110的1位集合为{2,3},即1set(011)={1,2},1set(110)={2,3}。 1位包含:1位包含是指某一标签的1位集合包含于另一标签的1位集合。如:010的1位集合包含于011的1位集合,即{2}⊂{1,2}。 多层分段标签:本文所设计的多层分段标签通过分段设计使其具备了双标签的功效。标签共分为前后2段,分别为层号段与标签值段。层号段标识基本块所属层次,记为BS1。标签值段则在同层内标识不同的基本块,记为BS2。 作为标签检错技术的一种,多层分段标签控制流错误检测方法也不可避免地遇到了一个问题:基本块多前驱矛盾。CFCSS为了解决这一问题增加开销引入了变量D,RCFC为了解决这一问题放弃了标签唯一性从而造成了检错率的下降。多层分段标签控制流错误检测方法利用特殊的标签机制及更新规则,在解决这一矛盾的同时未增加任何开销,同时也保证了标签的唯一性,具体规则如下。 规则3程序执行时,全局动态标签GS的更新语句在基本块入口位置,O型基本块执行异或运算,M型基本块执行或运算。即: 规则4程序内所有O型基本块标签的1位集合包含于其后继M型基本块标签的1位集合。即:∀bi,bj∈B,若bi=pred(bj),bi∈TO且bj∈TM,则1set(BS(bi))⊂1set(BS(bj))。 若基本块为O型基本块,分段差值参数为基本块分配标签与其前驱基本块分配标签异或运算的结果。即:∀bi,bj∈B,若bi∈TO,bj∈pred(bi)且bi∈succ(bj),则d(bi)=BS(bi)xor BS(bj)。 规则5若基本块为M型基本块,其分段差值参数层号段为0,标签值段为该基本块所有前驱标签值段或运算的结果。即:∀bi,bj1,…,bjn∈B,若∀bi∈TM,bj1,…,bjn∈pred(bi),则d(bi)=BS(bj1) or BS(bj2) or…or BS(bjn)。 规则6所有M型基本块标签中标签值段为该基本块所有前驱基本块标签中标签值段或运算的结果。即:∀bi,bj1,…,bjn∈B,若∀bi∈TM,bj1,…,bjn∈pred(bi),则BS2(bi)=BS2(bj1) or BS2(bj2) or…or BS2(bjn)。 规则7将程序所有基本块按层次划分,并在标签层号段标识层号。层号具备唯一性,且互相满足1位不包含原则。一般来说,层号仅取标签层号段的某一位为1。即:∀bi,bj∈B,若Lv(bi)≠Lv(bj),则(1set(BS1(bi))⊄1set(BS1(bj)))∪(1set(BS1(bj))⊄1set(BS1(bi)))。 规则8若程序中存在循环控制流,即某一基本块同时处于多个层级中,则该基本块必为M型基本块,且其层号为其所有前驱基本块层号or运算的结果。即:∀bi∈B,bj1,…,bjn∈pred(bi),则BS2(bi)=BS1(bj1) or BS1(bj2) or…or BS1(bjn)。 规则9不同层级间基本块标签值段可重复,但同一层基本块间标签值段必须唯一,且该层所有O型基本块之间互相满足1位不包含原则,M型基本块之间也互相满足1位不包含原则,非前驱后继关系的O型基本块与M型基本块也互相满足1位不包含原则。 规则10程序内每一个基本块均要有标签检查指令,位置在标签更新指令之后,用于比较全局动态标签GS与基本块标签BS的值以检测控制流错误。 上述规则为多层分段标签控制流错误检测方法的基本规则,也是必要规则。规则3~规则6是多层分段标签控制流错误检测方法可以获得较低开销的基础,本文将基本块划分为2种类型:O型与M型。由于O型基本块至多只有一个前驱,故基本块多前驱矛盾都集中发生在M型基本块中。多层分段标签控制流错误检测方法在M型基本块的标签更新语句中使用or运算来替换xor运算。但or运算本身不具备唯一性,有可能导致某些控制流错误无法检测。如图3(a)所示,依照规则3~规则6分配标签,通过or运算解决了b2→b4和b3→b4的基本块多前驱矛盾问题,但发生b1→b4的控制流错误跳转时,就无法检测出来。为了解决该问题,本文引入了层号的概念,并在标签的设计上做出了调整。如图3(b)所示,层号可以检测出程序中发生的b1→b4控制流错误。层号在设计时也要遵循一定规则,否则如图3(c)所示,层号未解决问题。因此,本文提出了规则7。对于整个程序而言,层号之间必须有所区分且唯一。在此基础上,也不允许存在1位集合包含的情况,即任意的2个不同层号之间,1位集合互不包含。层号不允许设置为0,一般层号仅取标签中的某一位为1即可。如程序共分为3层,则层号可分别设为:001,010,100。程序的循环结构是一种较为常见的结构,体现到程序控制流程图中就代表会出现如图3(d)中b1的结构。这种情况下使得基本块b4同时处于010层和100层中,故层号也包含了010和100。为了解决这一现象,本文引入了规则8,依照此规则此时基本块b4的所属层号为010 or 100=110,同时兼顾了b2→b4、b3→b4和b5→b4的控制流跳转。 (a) (b) (c) (d) 规则3~规则8解决了控制流跨层错误跳转的问题,但未顾及同层错误跳转问题,尤其是当同一层含有2个或2个以上的M型基本块的情况。如图4(a)所示,b2、b4和b5均为M型基本块,在程序中存在2条控制流b2→b4和b2→b5,依照规则1在上述2条控制流中插入了空基本块bp1和bp2,按照规则2划分层次。如图4(b)所示,在仅考虑规则3~规则8的情况下,本文设计了一款样例标签。可以看出图4(b)中,标签无法检测出b1→b5或b4→b5的控制流错误跳转。故此设计了规则9。同一层的O型基本块间标签值段必须唯一,且满足互相1位不包含原则,M型基本块同理。图4(b)程序中的O型基本块b1的1位集合被同层O型基本块b2和b3所包含,M型基本块b4的1位集合被同层M型基本块b5所包含,故产生了上述2条无法被检测的控制流错误。依据规则10可插入检查指令,考虑所有规则重新设计了如图4(c)所示的标签方案,解决了上述问题。 (a) (b) (c) 接下来,本文引入一些定理来证明本文提出CFMSL的安全性及完备性。安全性是指当程序正确执行时,多层分段标签方法所分配的标签不会检测出错误。完备性则是指若程序在执行过程中发生了基本块间错误跳转,多层分段标签方法可以将其检测出来。 引理2通过规则1重构后,得到的程序控制流任意M型基本块均与其前驱基本块处于同一层次。 证明:若存在一基本块为M型基本块前驱,且和该基本块不属于同一层次。根据规则2,所有M型基本块的前驱序列中的O型基本块和该M型基本划分为同一层,可知该前驱基本块只能为M型基本块。根据引理1,M型基本块的前驱不可为M型基本块,产生矛盾。因此,不存在这样的基本块前驱,即任意M型基本块均与其前驱基本块处于同一层次。 定理1当程序正确执行时,若标签在进入基本块前满足GS=BS,则无论程序执行至基本块内任何位置,仍满足GS=BS。 证明:设∀bi,bj∈B,且程序中存在控制流eji,即bi∈succ(bj)且bj∈pred(bi)。当全局动态标签GS到达基本块bi时GS=BS(bj),所执行的标签更新语句取决于此时基本块的类型。根据定义,程序中任意基本块均属于O型或者M型,故分2种情况讨论: 1)bi∈TO。根据规则3,此时基本块的更新语句为GS=GS xord(bi)=BS(bj) xor BS(bi) xor BS(bj)=BS(bi)。 2)bi∈TM。根据规则3,此时基本块的更新语句为GS=GS ord(bi)。根据规则6和规则8,GS更新语句为GS=GS or d(bi)=BS(bj) or BS(bj1) or … or BS(bjn)=BS(bi)。 综上所述,此时的全局动态标签在基本块任何位置均满足GS=BS。 引理3若因程序发生错误跳转而导致全局动态标签层号段在程序中任何一处与基本块标签层号段不同,则此错误会被检查出来。 证明:若层号与期望值不同,证明此时发生了跨层错误跳转。错误产生后,GS会在基本块入口处进行标签更新。GS抵达不同类型的基本块,会遇到不同的标签更新运算。若抵达O型基本块,则更新语句为GS=GS xord。异或运算的结果具备唯一性,已有的层号段错误不会被掩盖,故此错误可以被检查出来。若抵达M型基本块,则更新语句为GS=GS ord。根据规则7,此时层号段与期望值不同,但也满足1位互不包含原则。根据规则8,更新语句中的差值参数d层号段1位与基本块所处层次1位相同,即d1和GS的1位不同。显然,1位是无法被或运算掩盖的,故此错误也能被检查出来。 引理4若因程序发生错误跳转而导致全局动态标签值段在程序中任何一处与基本块标签值段不同,则此错误会被检查出来。 证明:根据引理3,层号段出现错误会被检查出来,所以现在考虑层号段未出错,标签值段出错的情形。层号段未出错,证明程序发生的是同层错误跳转。根据GS抵达基本块的类型进行分类讨论。若抵达O型基本块,则更新语句为GS=GS xord。异或运算结果具备唯一性,根据规则9同层基本块标签值段也具备唯一性,故此时的标签值段错误不会被掩盖。若抵达M型基本块,则更新语句为GS=GS ord。因发生同层错误跳转且跳到M型基本块,故此时也有2种情况:1)O型基本块错误跳转到M型基本块,由于是同层错误跳转,此O型基本块和M型基本块不是前驱后继关系;2)M型基本块错误跳转到M型基本块,此时也是同层错误跳转。根据规则9,无论是上述哪种情况,起点基本块和错误跳转基本块的标签值段均满足1位不包含原则,故二者标签值段有不同的1位,或运算无法掩盖,故此错误可以被检查出来。 引理5所有抵达O型基本块的错误跳转,均会被该基本块内的检查语句检测出来。 证明:设∀bi,bj∈B,程序发生错误跳转bj→bi,且程序运行至bj前均正确执行。因发生的是错误跳转,则bj∉pred(bi),根据规则6~规则9,BS(bj)≠BS(pred(bi))。程序运行在至bj前均为正确执行,故此时全局动态标签与其期望值相等,即GS=BS(bj)。跳转后,全局动态标签GS立刻进行更新操作,则GS=GS xord(bi)=BS(bj) xor BS(bi) xor BS(pred(bi))≠BS(pred(bi)) xor BS(bi) xor BS(pred(bi))⟹GS≠BS(bi)。根据引理3与引理4,GS任意一位与BS(bi)不相等,均会被检测出来。 引理6所有抵达M型基本块的错误跳转,均会被该基本块内的检查语句检测出来。 证明:∀bi,bj∈B,程序发生错误跳转bj→bi且至bj前均为正确执行。bj∉pred(bi),BS(bj)≠BS(pred(bi)),GS=BS(bj),分情况讨论。 若bj与bi属于不同层次,则GS1=BS1(bj)≠BS1(bi)。据M型基本块标签更新语句,此时GS1=GS1xord1(bi)=BS1(bj) or BS1(bj1) or … or BS1(bjn),其中bj1,…,bjn∈pred(bi)。根据规则2,BS1(bj1)=BS1(bj1)=…=BS1(bjn)=BS1(bi),故GS1=BS1(bj) or BS1(bi)。根据规则7,BS1(bj)与BS1(bj)互相1位不包含,故GS1=BS1(bj) or BS1(bi)≠BS1(bi)。据引理3,层号段的错误会被检测出来。 若bj与bi属于相同层次,则错误跳转不会引发层号错误。根据规则9,GS在错误抵达bi前GS2=BS2(bj)≠BS2(bi)。据M型基本块标签更新语句,GS2=GS2or d2(bi)=BS2(bj) or BS2(bj1) or…or BS2(bjn)=BS2(bj) or BS2(bi),其中bj1,…,bjn∈pred(bi)。据规则9,无论bj是O型还是M型基本块,BS1(bj)与BS1(bj)互相1位不包含。故GS2=BS2(bj) or BS2(bi)≠BS2(bi),根据引理4,标签值段的错误会被检测出来。 定理2多层分段标签控制流错误检测技术是完备的。在程序中任何违反正确控制流的基本块间错误跳转均可被检测出来。 证明:程序中的控制流错误会导致2种情况,程序非法跳转至程序基本块内部或跳出程序至非代码部分。跳转至非代码部分代表程序进入了数据部分或者未经初始化的存储区域,根据参考文献[11],若跳转至这一部分,处理器在尝试执行数据或未初始化的存储区域时会引发指令异常而导致系统报错。如果跳转至程序内部,则将跳转至O型基本块或者M型基本快。根据引理5与引理6,无论跳转至哪种类型的基本块,均会在检查指令中检测出错误。 根据上述定理可知,CFMSL方法是完备的,为了进一步说明定理2,本文给出了控制流非法跳转示例,如图5所示。 图5 控制流非法跳转示例图 如图5所示,灰色为M型基本块,白色为O型基本块,图中共给出了8种控制流错误的示例。err1与err2为M型基本块跳转至M型基本块,由于b1、b4和b6三者层级不同,err1/err2跳转时层号段出错,根据引理3和引理6,2个错误均会被检查出来。err3/err4为O型基本块跳转至O型基本块,b2、b3和b5处于不同层次,根据引理3和引理5,2个错误均会被检查出来。err5/err6为M型基本块跳转至O型基本块,b1与b5不同层,故err5可根据引理3和引理5检查出来。b5与b6处于同一层次,但由于逆向跳转,导致标签值段发生了错误,故根据引理4和引理5可将err6检查出来。err7/err8为O型基本块跳转至M型基本块,此时b1与b3处于不同层级,b2与b6处于不同层级,故根据引理3与引理6可知,2个错误均会被检查出来。 本文设计了多层分段标签控制流错误检测算法,针对以C语言编程的数据库管理系统,通过相应规则进行基本块层次划分,并分配基本块标签层号段及标签值段。插桩标签更新指令和标签检查指令,最终生成具有检错能力的目标程序。具体的步骤如下: Step1将目标程序编译成中间代码,以进行控制流分析。 Step2分析程序控制流关系,根据规则1重构程序基本块,使整个程序满足M不连续原则。 Step3根据规则2按层划分基本块,根据规则7、规则8分配基本块标签层号。 Step4依照基本块层次遍历基本块,同层基本块依照规则6、规则8和9分配基本块标签值段。 Step5遍历所有基本块,依照规则3、规则4和规则5插桩基本块更新指令。 Step6根据规则10插桩标签检查指令。 在程序执行时,指令进行跳转的目标地址受软错误影响而改变,这会导致2种结果: 1)改变后的目标地址仍在程序代码区内。此时程序计数器的值虽然发生了变化,但是并没有跳出程序,只是在程序内部的基本块间互相跳转。 2)程序计数器发生改变后,指向了程序代码区以外的地址。 根据上述控制流错误结果,使用2种错误类型来模拟软件控制流错误:控制流错误跳转和控制流错误跳出。控制流错误跳转是指程序控制流执行时发生控制流错误,控制流发生错误跳转,但仍然在程序内部。控制流错误跳出是指程序控制流执行时发生控制流错误,使控制流错误跳出至程序外。 本文使用的故障注入工具是基于GDB(GNU Project Debugger)[23]二次开发实现的。工具分为2种类型:控制流错误跳转故障注入工具和控制流错误跳出故障注入工具,分别对应上述2种控制流错误类型。 1)控制流跳转故障注入工具。 Step1启动GDB并加载要注入控制流跳转错误的程序。 Step2完整运行一次程序,记录所有程序指令跳转的PC值。 Step3随机选择一条PC值,记录下来,作为控制流错误跳转的起点。。 Step4使用GDB重新加载程序。 Step5运行程序,至Step3所选起点指令PC值处设置断点。 Step6在剩余PC值中随机选择1条,控制程序跳转过去。 Step7根据程序的输出来统计故障注入的结果。 2)控制流跳出故障注入工具。 Step1启动GDB并加载要注入控制流跳出错误的程序。 Step2完整运行一次程序,记录所有程序指令跳转的PC(Program Counter)值。 Step3随机选择一条PC值,记录下来,作为控制流错误跳出的起点。 Step4使用GDB重新加载程序。 Step5运行程序,至Step3所选起点指令PC值处设置断点。 Step6在程序计数器内的地址随机选择一位或者多位进行翻转,同时保证翻转后的地址不在Step2记录的程序内部PC值中,将程序跳转至翻转后的地址。 Step7根据程序的输出来统计故障注入的结果。 本文使用错误检错率来评估CFMSL方法的错误检测能力。CFMSL方法可以通过标签检测控制流错误。本文对测试程序注入控制流跳转错误与控制流跳出错误,以此来模拟程序发生控制流错误时的状态。为了验证CFMSL方法的性能,本文另外选择3种控制流错误检测加固方法CFCSS、CEDBR和RCFC来进行横向对比。CFCSS为2002年的方法,尽管年代较为久远,但是作为最具代表性的单标签控制流方法,仍然具有较高的参考价值。RCFC是2016年提出的一种双标签方法,尽管标签设计有一定的缺陷,却也提供了一种新思路。CEDBR是2018年提出的双标签方法,相比于RCFC,CEDBR已经有了较好的标签设计和详细的规则,属于双标签方法中较为优秀的方法。分别使用这3种方法和CFMSL对快速排序算法、最短路径算法和数据管理系统3个程序进行加固,得到了12个加固后的程序。为了体现鲁棒性和有效性,本文对每个加固后程序分别注入了2500次控制流跳出错误和2500次控制流跳转错误,共60000次故障来验证CFMSL方法的性能。实验结果如图6所示。 图6给出采用不同的加固方法下,错误检测性能的对比。漏检率与检错率的统计是综合了控制流错误跳转与控制流跳出2种故障注入实验数据的综合结果。其中CEDBR和RCFC是基于双标签的控制流加固方法,CFMSL和CFCSS则是单标签多规则的加固方法。 图6 不同加固方法错误检测性能 本文对使用方法加固后的每一个程序,注入了2500次控制流跳出错误和2500次控制流跳转错误。即本文对每一个加固后的程序进行了5000次故障注入实验。系统报错率为这5000次实验中系统报错次数所占的比率。方法报错率为实验次数中由检错方法报错次数所占的比率。无错误率为向程序注入故障,但未出现错误次数所占的比率。漏检率为程序出现异常,但是方法和系统均未检测出错误次数所占的比率。1减去漏检率,即为错误检测率。 表1 故障注入实验数据 表1给出了具体实验数据,SYS表示系统错误的次数,Find_err表示方法发现错误的次数,Correct表示程序尽管注入了错误,但仍正确执行的次数。从实验结果可以看出,控制流错误跳出故障类型大部分可以通过系统直接检测出来,小部分对程序没有影响,只有极少的一部分错误会漏检。与之相反的是,控制流错误跳转故障中方法检测出的错误占据了大部分。与图6相同,表1中最后2栏的错误检测率与错误漏检率是综合了控制流错误跳转与跳出2种故障的实验结果。根据图6和表1,所有的加固方法中CFMSL具有最高的错误检测率和最低的错误漏检率。 各方法的时空开销如图7所示,具体实验数据如表2所示。从中可以看出CEDBR方法的开销是最高的,RCFC方法比它稍低一些,CFCSS和CFMSL方法比上2种方法开销要低。 图7 各方法的时空开销 表2 方法开销数据 综合图6和图7的实验结果,可以发现基于双标签的方法成本一般要比单标签多规则的方法高,而且只要规则设置得合适,单标签的方法错误漏检率也可降低。而在上述4种方法中,单标签的CFMSL开销最低,漏检率也是最低的。 RCFC是一种双标签算法,在O型基本块插桩标签G1,在M型基本块插桩G2。其G2标签仅使用1和0这2个数来区分标签类型,不具备唯一性。且标签更新函数为“store”赋值语句而非运算,容易将标签错误掩盖,故存在着较高的漏检率。CEDBR是基于RCFC的改进算法,在标签更新上进行了改进。CEDBR在基本块内部使用加减运算进行G1标签更新,尽管开销增加,但显著提高了检错率。另一方面,CEDBR的G2标签仍使用1和0,只能区分基本块类型,不具备唯一性,这导致CEDBR仍然存在漏检情况。CFCSS则是一种传统的单标签方法,但是为了解决基本块多前驱矛盾,引入了变量D来对标签进行更新,导致开销增大。CFMSL作为一种单标签方法,却通过分段的形式起到了双标签的作用。将基本块划分层级后,跨层的错误跳转可以通过层号段检测出来,同层的错误跳转可以通过标签值段进行检测。CFMSL使用XOR和OR运算的组合,在不添加任何指令和标签的情况下成功解决了基本块多前驱矛盾问题,最后又使用标签更新规则保证了标签更新过程的唯一性。这使得CFMSL在具备较高检错率的同时具有较低的开销。 本文提出了一种多层分段标签控制流错误检测方法CFMSL。通过分析程序中的控制流信息和基本块结构,按层次重新划分基本块。对重构后的基本块,分配多层分段标签,插桩标签更新指令和标签检查指令,最终可得到控制流检错加固后的程序。本文设计了基本块按层划分规则、基本块标签更新规则、基本块标签检查规则。通过定理证明和逻辑分析证实了本文方法的正确性和完备性。最终通过控制流故障注入工具对程序进行故障注入实验,通过实验结果验证了方法的有效性。2.2 基本块按层次划分规则
2.3 多层分段标签规则
2.4 多层分段标签控制流错误检测算法描述
3 实验及结果分析
3.1 故障注入工具
3.2 方法评估
4 结束语