基于插桩和布尔逻辑的运行时程序验证框架

李业华，顾乃杰，张颖楠，彭 飞

(1.中国科学技术大学计算机科学与技术学院，合肥 230027；2.安徽省计算与通讯软件重点实验室，合肥 230027；3.中国科学技术大学中国科学院沈阳计算技术研究所网络与通信联合实验室，合肥 230027)

1 概述

程序验证作为保证软件正确性的一项重要技术得到了学术界的广泛关注。研究人员在20世纪60年代便开始了有关程序验证理论和方法的研究，开发出很多针对特定软件漏洞的检测和验证工具[1-3]。运行时验证技术验证软件执行路径是否满足一定的特征和规范，它比静态验证更加贴近软件系统的实现和执行。这种方法观察和验证的是软件运行时的行为，并不需要分析软件所有可能的行为。所以运行时验证的复杂度不会随着软件规模和复杂性的增加有显著变化[1]。

本文提出一种运行时程序验证框架RPA，以验证和分析运行时程序的行为属性，设计一门基于布尔逻辑的动态逻辑语言RPAL，以刻画运行时程序行为，还实现了该语言的虚拟机。RPA在虚拟机之上执行用户指定的感应器安放，并收集运行时程序状态信息，执行精确的属性分析和验证。感应器是程序状态暴露代码的形象表述，将使用程序插桩技术自动植入到目标程序的执行代码中，完全免去为了分析软件行为而手工添加状态输出代码的工作。

Saturn[2,4-5]是由美国 Stanford大学开发的一个用于静态检查大型软件系统属性的项目。Saturn定义了一门逻辑语言 Calypso[5]来描述属性约束集。该属性约束集定义系统的特征和属性。本文提出的RPAL语言参考了 Calypso语言的设计。但 RPAL在 Calypso的句子、谓词和事实等语法元素基础上扩展了事实操作集，大大增强了事实管理模型。相比Calypso，RPAL是动态语言而不是符号语言，支持完整的类型系统和对象管理。因此分析程序的语义变得更加清晰，大大减少因为分析程序的类型错误导致的分析结果错误。

RPA使用独立的事实仓库管理验证过程中的中间和最终事实结论。事实仓库建模为命名事实栈集合，支持比Saturn更灵活的事实管理操作。

Saturn中的分析以函数为基本分析单位，跨函数范围的分析相对困难，需要借助函数总结来实现。RPA作为一个运行时验证框架，可以使用简单而通用的布尔逻辑直观地定义软件行为特性。

在分布式系统检错领域，Pip[6]、D3S[7]均定义一门系统描述语言以刻画节点间的通信行为。MaceMC[3]是建立在Mace[8]分布式系统开发框架上的基于模型检测的程序验证工具。同样使用模型检测技术的有MODIST[9]、CrystalBall[10]。另外，文献[1]提出了一个面向切面程序的程序运行时验证框架。该框架采用线性时序逻辑语言LTL[11]作为系统描述语言，不需要独立的虚拟机支持。该框架只接受AspectJ程序，可以利用添加切面的方法把运行时验证的任务以新切面的形式整合到目标软件中。而 RPA的验证面向可执行的二进制程序，比该框架更灵活，适用性更广。

2 运行时程序验证框架

RPA是一个用于验证和分析运行时程序属性的工具框架。完整的RPA系统包括RPA核心和RPAL扩展。其中RPA核心包括RPAL语言、RPAL语言解析器和 RPA程序验证虚拟机 3个部分，而RPAL扩展则包括各种扩展谓词库。

2.1 基本验证流程

RPA定义了一门形式语言RPAL来描述运行时软件的行为和属性。这样的一个用RPAL语言表达的合法描述称为运行时软件的规范，在实现上称为RPAL分析程序。RPA运行时程序验证的流程如图1所示，RPA执行的验证分析依赖于2个输入：RPAL分析程序和运行时程序的状态信息。

图1 RPA运行时程序验证的流程

为了收集必需的运行时状态以支撑验证工作，RPA需要在系统分析之前利用插桩技术往目标软件植入状态暴露的代码。所以，RPA的整个分析过程分为2个阶段：

(1)第1阶段是感应器安放阶段，主要根据RPAL分析程序刻画的程序属性执行程序插桩工作。插桩后的目标软件每一次执行将会额外地输出状态信息记录文件。

(2)在第 2阶段，RPA会启动目标程序执行，结束后把合法的RPAL分析程序和状态信息记录文件作为RPA虚拟机的输入，启动分析过程。

第2阶段结束后，分析结论会输出到外部文件。用户使用RPA结论查看工具查看和分析验证结果。

2.2 系统框架

RPA核心实现包括RPAL解析器和RPA虚拟机。RPAL解析器负责分析RPAL分析程序的输入，准备好基本的验证环境。RPA虚拟机则在解析器准备的验证环境基础上执行系统的验证分析工作。图2给出了RPA的主要框架。

图2 RPA系统框架

具体描述如下：(1)内存管理器管理 RPA系统所有内存资源的申请和释放。(2)程序信息管理模块管理目标软件的信息。(3)插桩管理模块调用多种现有插桩工具(PDTOOLKIT[12-13]、Pin[14])进行源码和运行时插桩。(4)模型层包含谓词扩展的实现。这些谓词扩展定义了程序验证所基于的基本分析模型。(5)程序逻辑分析器实现句子调度分析算法，执行系统的验证分析。该模块的分析过程利用模型层的分析模型实现。

3 RPAL动态逻辑语言

RPAL是一门动态逻辑语言。用户使用RPAL语言编写分析程序，刻画运行时软件的行为特性。所以，RPAL分析程序也可理解为运行时软件的规范。本节讨论RPAL的主要元素、相关概念和关键特性。

3.1 概念和元素

运行时软件规范由独立完整的句子组成。每一个独立完整的句子断言了运行时程序的某一行为或属性。句子由谓词组成。谓词是基本断言单位，带有特定的语义，断言一个基本事实。

RPAL句子支持布尔合取和布尔非等逻辑表达式。多个RPAL句子之间是布尔析取关系。这些布尔表达式的文字就是谓词。下面是RPAL句子和谓词的数学定义。

定义 1 句子定义为具有不定参数个数的布尓函数 S：

其中， Pi（1≤ i≤m）是具有ni个参数的布尔函数，句子S的 谓词 ；Sin=｛xik|1 ≤i≤ m, 1≤ k ≤ ni｝是 句子S的输入。上述定义为了书写方便省去了包含布尔非的谓词项。事实上布尔非可以在任何谓词前使用。

句子S的执行或者估值定义为对函数S（ P1, P2, ···,Pm）求值。同样地，谓词P的执行或者估值定义为对函数 P（ x, x2,… , xn）求值。满足句子S定义为S的估值为真。同样地，满足谓词 P定义为 P的估值为真。

谓词是构成句子的最小单位，用于表达特定约束。谓词除了估值得到满足性结果外，还可以有多个输出。精化谓词P的定义后得到定义2。

定义2 谓词P定义为：

其中，1 ≤ k ≤ n,1 ≤ l ≤ m ；ik是P的输入；Ol是P的输出。

RPAL既支持断言谓词以断言运行时程序点上特定性质，也支持事实添加谓词和事实查询谓词以实现事实推理。事实推理是 RPA的另外一个重要特性。事实推理能力使得 RPA在分析验证运行时程序的同时根据句子定义的推理规则发现新的事实。这些新发现的事实可以作为后续推理的中间结论保存在事实仓库。程序分析结束后所有保留在事实仓库中的事实成为整个验证的结论保存到外部数据文件，以供用户查询分析。

RPAL句子可以通过把一个谓词的输出作为另外一个谓词的输入来形成更完整的断言。谓词使用举例如表 1所示，其中包括定义断言谓词 P、Q、R以及事实查询谓词F。

定义句子：

句子S断言了函数father调用过之后，函数func每一次调用的时候，变量v1的值不能为100。其中，“～”是RPAL中布尔非符号。

由此可见，如果 RPA能提供灵活而丰富的基本谓词集合，工程师便可以灵活地表达特定模型下有关运行时程序行为属性的任意断言。事实上，支持灵活的谓词扩展正是 RPA设计上的一个重要的原则。研究者和工程师只要为 RPA设计并实现支持各种运行时验证模型的谓词库便可把 RPA的功能拓展到更加广阔的验证领域中。一般来说一套谓词库支持一种特定的分析模型，包含基本谓词实现，还有扩展对象类型的定义。本文的工作除了实现 RPA核心外，还包括一个RPAL谓词扩展库FCAM。FCAM支持函数调用分析模型和基本的变量值跟踪模型。

3.2 RPAL分析程序组成

与通用的编程语言不同，RPAL更像是一门声明语言，没有条件和循环等流控制语句。RPAL以句子的形式定义运行时程序的属性和约束，以及条件满足时事实的操作，而不是定义 RPA体如何执行系统的分析检测。一个合法的RPAL程序应该由类型定义、变量赋值和运算语句、事实谓词定义和句子集合组成。最终有效的运行时程序规范的定义，以及事实的推理规则由且仅由程序中定义的句子组成。

4 程序验证框架的实现

RPA程序验证框架的实现主要包括RPAL语言解析器和RPA虚拟机的实现。本文主要讨论RPA虚拟机的实现。3个RPA上的术语如表2所示。

表2 术语定义

RPA虚拟机定义了RPAL分析程序运行的环境，处理所有底层的输入输出工作。更重要的是，RPA虚拟机负责调度RPAL分析程序的句子执行，使得用户定义的运行时程序规范能够正确而系统地与软件的某次具体执行相比较，实施具体的事实推理。

虚拟指令映射与事实仓库示意图如图3所示。

图3 虚拟指令映射与事实仓库示意图

合法的 RPAL分析程序传递到 RPA系统之后，理论上，RPA会在目标执行流每条指令之后检查所有句子是否均满足。句子在执行的时候可以发现新事实，去掉已有事实，和检查特定事实是否存在。实际上 RPA的实现并不是在目标执行流每条指令之后都执行检查，而是在数量非常少的关键节点执行检查。RPA会在第1阶段使用插桩技术自动往关键节点中插入感应器。在第2阶段，这些感应器输出作为虚拟指令被 RPA虚拟机捕捉，识别后句子映射到 RPAL分析程序的具体句子(见图 3)。接着句子在虚拟机上被调度执行。

4.1 程序插桩

放置感应器是整个 RPA系统实现正确而全面检测的基础步骤。RPA通过源码插桩技术向目标软件的源码插入合法感应器代码。这些代码段随后会跟软件其他源码文件一起编译链接。感应器代码的主要任务是按照虚拟指令的格式往外部文件写入该插入点上被观察变量的值。感应器就是一个到多个这样的值组成的集合，反映目标系统某方面的状态信息。一个虚拟指令可以容纳任意个感应器。一个感应器可以包含任意个观察值。

正确的程序插桩需要2个步骤：查找插桩点和插入插桩代码。RPA核心向谓词实现提供了一个统一而灵活的插桩模块。谓词实现只要向插桩模块提供插桩点特征信息和待插入的虚拟指令即可完成一次插桩。

RPA的插桩管理模块整合了 PDTOOLKIT[13]工具包和 Pin[14]动态插桩工具。PDTOOLKIT项目的DUCTAPE开发库为RPA提供结构化地分析高级语言(C/C++/Fortran)的接口。使用 DUCTAPE，插桩管理器可方便地定位目标源码插桩点。

4.2 句子调度

在RPA中，程序验证过程是由虚拟指令驱动的。RPA虚拟机顺序地从状态信息记录中读取虚拟指令，然后通过句子映射找到对应的句子，用感应器信息更新谓词内部状态。本文定义这样的过程为一次虚拟指令的执行。

每一次更新谓词状态之后，RPA虚拟机会尝试调度句子执行。RPA虚拟机调度器调度过程分为2个阶段：预处理阶段和调度阶段。虚拟机在预处理阶段的主要任务是估算句子里谓词的满足性。当虚拟机发现句子里所有谓词都可能满足的时候，该句子被标记为待调度并添加到待调度句子集合。同一时刻有可能存在多个标记为待调度执行的句子。这种情况下虚拟机在调度阶段需要计算待调度句子之间的依赖关系，确定句子的执行顺序。如果出现循环依赖，虚拟机报告调度错误并停止RPA系统。

预处理阶段的结果是当前可调度的句子集合S。事实上，句子之间可能存在事实依赖关系，见定义3。

定义 3 若句子 S1的执行会产生事实 F，句子 S2满足的前提是存在事实F，则S2事实依赖于S1。

如果句子A事实依赖于B，那么A满足的前提是B被执行。这种情况下RPA句子调度算法应得到先B后A的句子执行顺序。然而，RPAL程序员可以定义这样一套句子集合。在某种情况下句子 A和句子 B之间相互依赖。这种情况称为句子循环。句子循环是禁止的，理论上这样的句子集合定义经修改可得到合法的没有相互依赖的句子集。一个包含句子循环的例子如下：

假设目标程序存在这样的一个调用序列func1()->func2()->func1()。RPA 虚拟机会在函数func1和func2的起始行插入2个虚拟指令：VI1，VI2。RPA在读取VI1的时候，行4的call谓词状态被更新，虚拟机进入预处理阶段。预处理结束后行4的句子被标记为待调度状态。由于该句子是唯一待调度句子，所以不存在依赖问题。句子4执行后句子3会接着被行 4的Finfunc事实添加操作唤醒执行。另外句子 6第1个谓词标记为满足。当func1调用func2时，句子6被唤醒执行。这时虽然句子11第2谓词call也同时被更新，但第一事实谓词Finfunc不满足，所以句子 11不被调度。句子6执行的结果是 Finfunc(f2)被添加到事实仓库。继而标记句子 8和11的第一谓词满足性为真。最后func2递归调用func1时，句子8、句子4和句子3会标记为待调度并相继执行。这种情况下句子8和句子4之间并不存在事实的依赖关系，所以执行次序可交换。

虽然上述例子没有产生任何错误，但句子 11有可能引起句子循环。假设上述例子中，被func2调用的func1内部再次递归调用func2。这时句子11和句子6成为待执行句子，但是句子11和句子6形成句子循环。

RPA句子还可能存在这样的形式：

Finfunc(F), call([F]), +Finfunc(F);

第3事实谓词Finfunc的参数是第2谓词的输出，与第1谓词参数同名却对应不同对象。这种形式不存在句子循环。这种依赖称为伪事实依赖，这种形式称为伪句子循环。

综上所述，RPA句子调度算法可分 3个阶段：(1)第1阶段为预处理阶段，以事实名为关键字建立依赖关系，去掉伪句子循环。(2)第2阶段使用拓扑排序算法计算待执行句子的执行次序。若排序过程中发现环，则进入第3阶段，否则算法结束。(3)调度器在第3阶段匹配相互依赖的事实对象间的参数，确定句子循环是否存在。若存在则报告错误并退出检测，否则更新句子依赖关系并返回第2阶段。

5 实验结果与分析

RPA的其中一个目标就是帮助代码阅读者理解现有系统。本文通过一个实际的例子来展示如何用RPAL编写实际的运行时程序分析程序，并且给出该例子的验证结果。该例子使用了 FCAM 谓词扩展库。

该例子的实际系统——Haproxy[15]是一个提供TCP和HTTP代理服务的高速网络负载均衡器，具有高可靠性、高可用性和功能强等特点。Haproxy内部处理每一个 HTTP session的主函数是 process_session。process_session的实现是一个巨大的状态机，包括非常多底层I/O接口状态的判断和转移。利用一般的代码阅读工具辅助理解变得非常困难。这时候，RPA工具既能帮助系统分析者验证系统运行时的行为，也能根据分析者制定的推理策略自动发现事实得出结论。Haproxy处理session的相关函数如下：

一个断言在process_session函数调用期间的例子如下，在process_session所有子函数调用之外session的状态(session->flag)不会改变的 RPAL分析程序片段。

process_session函数一方面负责建立和关闭链接、IO错误检查，另一方面调用多个 HTTP包分析函数分析HTTP报文。session_accept函数在新HTTP session到来时调用，负责session结构的初始化。本例子将要展示RPA在谓词扩展FCAM支持下跟踪堆变量值的能力。对于Saturn等只支持静态分析的系统来讲，实现正确动态堆变量值的跟踪和分析非常的困难。然而 RPA却非常适合观察分析堆变量和跨函数调用的程序逻辑。

以上所示 RPAL程序中，行 18的句子断言若http_wait_for_request函数被调用，则添加空事实集合到默认事实栈，然后在该集合里面添加事实：在函数http_wait_for_request内部。行20断言当这个函数返回的时候弹出栈顶事实集。本例子的默认事实栈用作标识运行时程序当前所在的子函数调用。行22～行24使用另个命名事实栈 sess标识 process_session的调用。行 26～行 28读取 session.c文件第 17行上变量s->flag的值，并把该值保存在事实对象 Fval中。值得注意的是Haproxy在每一个新 session到来时在内存堆上动态申请变量s->flag的空间。行29～行31指定在session_free函数调用之后去掉Fval事实标记。行33～行35的句子是本RPA分析程序最关键的句子。它断言了当变量 s->flag值改变时控制流不会在http_wait_for_request函数调用内部。

如果 Haproxy的某次执行满足上述断言，那么RPA运行后会产生包含事实 Fsucceed的结论。由于s->flag的修改遍布process_session函数的整个调用过程，因此最终的测试结果是失败的，RPA输出空结论集。

6 结束语

本文提出了一个基于程序插桩和布尔逻辑的运行时程序验证框架RPA。RPA定义了基于布尔逻辑的动态逻辑语言RPAL。用户使用RPAL刻画软件运行时的行为和属性后，RPA可自动并系统地对软件进行插桩，执行验证和推理。本文给出了一个实际的例子，显示了RPAL框架可作为实际软件开发后期的验证和测试工具，承担软件正确性验证的任务。作为一个基本的验证框架，RPA仍然存在不足的地方。这主要表现在：

(1)现有 RPA谓词扩展库不足，只能支持函数调用模型和简单的变量值跟踪模型；

(2)RPA插桩模块支持的程序插桩方法有待扩充，以支持从源码到二进制代码，再到运行时程序的插桩能力。

下一步的工作是设计谓词扩展库以支持完整的变量跟踪模型，并完善RPA框架。

[1]梁 睿.基于运行时验证的 AOP程序检测框架研究[D].兰州: 兰州大学, 2009.

[2]Aiken A, Bugrara S, Dillig I, et al.Saturn Project[EB/OL].[2012-03-01].http://saturn.stanford.edu.

[3]Killian C, Anderson J W, Jhala R, et al.Life, Death, and the Critical Transition: Finding Liveness Bugs in Systems Code[C]//Proc.of NSDI’07.Cambridge, USA: [s.n.],2007.

[4]Aiken A, Bugrara S, Dillig I, et al.An Overview of the Saturn Project[C]//Proc.of PASTE’07.San Diego, USA:[s.n.], 2007.

[5]Aiken A, Bugrara S, Dillig I, et al.The Saturn Program Analysis System[EB/OL].[2012-03-01].http://saturn.stanford.edu.

[6]Reynolds P, Killian C, Wiener J L, et al.Pip: Detecting the Unexpected in Distributed Systems[C]//Proc.of NSDI’06.San Jose, USA: [s.n.], 2006.

[7]Liu Xuezheng, Guo Zhenyu, Wang Xi, et al.D3S: Debug Deployed Distributed System[C]//Proc.of NSDI’08.San Francisco, USA: [s.n.], 2008.

[8]Killian C E, Anderson J W, Braud R.Mace: Language Support for Building Distributed Systems[C]//Proc.of PLDI’07.San Diego, USA: [s.n.], 2007.

[9]Yang Junfeng, Chen Tisheng, Wu Ming, et al.MODIST:Transparent Model Checking of Unmodified Distributed Systems[C]//Proc.of NSDI’09.Boston, USA: [s.n.],2009.

[10]Yabandeh M, Knezevic N, Kostic D, et al.CrystalBall:Predicting and Preventing Inconsistencies in Deployed Distributed Systems[C]//Proc.of NSDI’09.Boston, USA:[s.n.], 2009.

[11]Pnueli A.The Temporal Logic of Programs[C]//Proc.of the 18th IEEE Symposium on Foundation of Computer Science.[S.l.]: IEEE Computer Society, 1977.

[12]Shende S S, Malony A D.The Tau Parallel Performance System[J].International Journal of High Performance Computing Applications, 2006, 20(2): 287-311.

[13]Shende S S, Malony A D.Pdtoolkit Project[EB/OL].[2012-03-01].http://www.cs.uoregon.edu/Research/tau/do wnloads.php.

[14]Luk Chi-Keung, Cohn R, Muth R, et al.Pin: Building Customized Program Analysis Tools with Dynamic Instrumentation[C]//Proc.of PLDI’05.Chicago, USA:[s.n.], 2005.

[15]Tarreau W.Haproxy Project: The Reliable, High Performance TCP/HTTP Load Balancer[EB/OL].[2012-03-01].http://haproxy.1wt.eu.