面向航天嵌入式软件的形式化建模方法

航天嵌入式软件是航天型号任务成败的关键之一.航天嵌入式软件是一种周期性、多模式的软件.软件的每个模式表示系统处于一定的状态,并进行相应的复杂计算.因此,提出了一种名为SPARDL的形式化建模方法.为了满足型号应用的需求,对这一方法进行了若干改进.为了表达航天器的时序性质,提出了一种基于区间逻辑的性质规范语言.为了支持工业应用,还设计了代码生成方法.这一建模方法已在航天工业领域得到了应用.     

中断驱动型航天嵌入式软件原子性违反检测方法

嵌入式软件的可信性对航天任务的成败至关重要. 航天嵌入式软件广泛采用中断驱动的并发机制, 不确定的中断抢占可能导致并发缺陷, 引发严重的安全问题. 研究表明原子性违反是中断并发缺陷中最突出的一类缺陷模式. 目前面向中断驱动型嵌入式软件的原子性违反检测方法都无法同时实现高精度和高可扩展性, 且其对真实航天嵌入式软件的有效性尚未得到证实. 为了有效提升检测该类缺陷的精度与效率, 对82个航天嵌入式软件原子性违反进行实证研究, 获得该类缺陷在原子区范围、中断嵌套层数、访问交错模式、共享数据访问方式、访问粒度等5个方面的表现特征. 并在此基础上, 提出一个精确、高效的原子性违反静态检测方法intAtom-S. 首先, 基于一个由数值不变式参数化的细粒度内存访问模型, 引入基于规则的方法剔除标志变量访问, 并采用抽象解释进行精确的共享数据分析, 该分析能将共享数据访问粒度精确至数组元素, 并可识别共享的内存映射I/O地址. 然后, 使用轻量级数据流分析技术匹配符合缺陷访问交错模式的所有并发三次访问序, 作为潜在的原子性违反缺陷候选. 最后, 采用基于路径条件的约束求解对缺陷候选中的串行访问对和并发三次访问序进行路径可行性分析, 逐步消除误报, 得到最终的原子性违反结果. 在基准测试集和8个真实航天嵌入式软件上的实验表明, 与目前最先进的方法相比, intAtom-S误报率降低了72%, 检测效率提高了3倍. 此外, 该方法能够快速完成对真实航天嵌入式软件的分析, 平均误报率仅为8.9%, 并发现了23个已被开发人员确认的缺陷.

     

基于标志位差异分析的整数溢出漏洞溢出点定位方法

近几年,整数溢出漏洞数量居高不下,危害性较大。目前,漏洞分析定位的方法仅在补丁自动生成或漏洞触发样本文件自动生成中有所涉及,且这些方法大多利用缓冲区溢出会覆盖其邻接内存数据的特点来进行定位分析,而整数溢出漏洞不具有直接覆盖重要数据的特点,所以现有的方法不能对其进行有效的定位分析。现阶段对整数溢出漏洞的分析大多依靠人工完成,效率较低。为了提高分析人员的工作效率,提出了一种结合动态污点分析技术进行EFLAGS标志位信息比对的方法,来将溢出点锁定在少量的地址中。在此基础上实现了一套整数溢出漏洞溢出点定位系统,并对提出的方法进行了验证。     

针对整数溢出潜在漏洞的快速定位系统

整数溢出漏洞作为一种历史悠久的漏洞,在当前的软件生态系统中仍然存在,且仍然可能导致严重的系统安全问题。对于整数溢出漏洞的检测工作主要是通过使用或结合符号执行,污点分析,模糊测试等技术进行,也取得了较好的效果。但是由于这些方法需要对检测目标进行深入的分析,这很大程度上限制了这些检测工具的推广和使用。该文针对整数溢出漏洞,分析了漏洞的产生原因和带来的安全威胁,设计和实现了一个基于静态语义匹配搜索的面向二进制文件的整数溢出潜在漏洞的快速定位系统。经测试,该系统能够检测出已公开的整数溢出漏洞。通过该系统检测软件中的整数溢出漏洞,及时对软件进行修复防护,可以有效提高软件的健壮性,减少整数溢出漏洞带来的安全隐患。     

基于时间STM的软件形式化建模与验证方法

状态迁移矩阵(state transition matrix,简称STM)是一种基于表结构的状态机建模方法,前端为表格形式,后端则具有严格的形式化定义,用于建模软件系统行为.但目前STM不具有时间语义,这极大地限制了该方法在实时嵌入式软件建模方面的应用.针对这一问题,提出了一种基于时间STM(time STM,简称TSTM)的形式化建模方法,通过为STM各单元格增加时间语义和约束,使其适用于实时软件行为刻画.此外,针对TSTM给出了一种基于界限模型检测(bounded model checking,简称BMC)技术的时间计算树逻辑(time computation tree logic,简称TCTL)模型检测方法,以验证TSTM时间及逻辑属性.最后,通过对某型号列控制软件进行TSTM建模与验证,证明了上述方法的有效性.     

基于模型驱动的机载嵌入式软件应用

传统的软件开发方法已无法应对机载嵌入式软件开发面临的严峻挑战,基于模型驱动的软件开发方法将业务模型和软件实现平台分离,有效地提高了机载嵌入式软件开发效率。文中对两种机载嵌入式软件设计方法进行了比较,以基于SCADE平台实现的自动飞行控制系统的自动驾驶仪模态控制软件为例,并对SCADE自动生成代码与手工编写代码的执行效率进行了比较,证明前者更优,验证了基于模型驱动开发的软件设计方法能有效地提高机载嵌入式软件的开发效率。     

基于程序特征谱整数溢出错误定位技术研究

随着软件业的飞速发展,人们对软件质量的要求也越来越高.整数溢出错误以其高危性和隐蔽性成为影响软件安全性和可靠性的重要因素之一.如何准确定位整数溢出错误是软件安全领域研究的热点.论文改进了现有错误定位模型,构建了整数溢出错误定位模型INTRank.实验结果表明:基于INTRank模型的语句可疑度估计方法可以较为准确地计算语句可疑度,使得程序员能够按照基于语句可疑度的优先级顺序检查源代码,找出导致整数溢出错误的原因,同时本文方法具有较低的漏报率.     

面向高可信软件的整数溢出错误的自动化测试

面向高可信软件提出了一种二进制级高危整数溢出错误的全自动测试方法(dynamic automatic integer-overflow detection and testing,简称DAIDT).该方法无需任何源码甚至是符号表支持,即可对二进制应用程序进行全面测试,并自动发现高危整数溢出错误.在理论上形式化证明了该技术对高危整数溢出错误测试与发掘的无漏报性、零误报性与错误可重现特性.为了验证该方法的有效性,实现了IntHunter原型系统.IntHunter对3个最新版本的高可信应用程序(微软公司Windows 2003和2000 Server的WINS服务、百度公司的即时通讯软件BaiDu Hi)分别进行了24小时测试,共发现了4个高危整数溢出错误.其中3个错误可导致任意代码执行,其中两个由微软安全响应中心分配漏洞编号CVE-2009-1923,CVE-2009-1924,另一个由百度公司分配漏洞编号CVE-2008-6444.     

基于层次化时间STM软件设计的形式化验证

状态迁移矩阵(State Transition Matrix,STM)是一种基于表结构的程序建模语言。事件变量类型单一,事件和状态数量的增加很容易造成状态空间爆炸问题,无法表达具有时间语义的软件系统等原因,极大限制了该建模方法的推广应用。文中针对这些问题,首先提出层次化时间状态迁移矩阵(Hierarchical Time State Transition Matrix,HTSTM)模型,用于设计、建模和验证具有时间条件约束的软件系统,并给出形式化表示方法。基于该表示方法提出一种符号化编码方法,采用有界模型检测思想将需要验证的LTL性质输入SMT(Satisfiability Modulo Theories)求解器进行验证,从而在一定程度上证明了软件设计的正确性。     

面向嵌入式软件测试的仿真建模

论述了面向嵌入式软件测试的仿真建模相关理论、技术和方法,提出了基于接口的模型外特性建模、面向测试的模型内特性建模、模型驱动的测试过程。开发了自动化辅助建模工具EasyModel,提高建模效率,保证模型的正确性。该工具已成功地应用于多个型号的软件系统测试中,实验结果证明了该仿真工具的有效性。     

T-CBESD:一个构件化嵌入式软件设计模型验证工具

现代复杂嵌入式软件系统的高可靠性需要有效的基于模型的设计与分析技术.传统的嵌入式软件可靠性保障技术主要关注于系统开发后期.本文在Eclipse平台上设计并实现了一个基于接口自动机模型的构件化嵌入式软件设计的形式化验证原型工具T-CBESD(Tool for Component-Based Embedded Software Designs).工具直接使用UML顺序图模型作为系统规约,可以检验系统设计模型与场景式规约之间多种行为一致性问题;并使用消息事件的时间约束不等式,检验实时接口自动机网络与带时间约束的顺序图模型之间的实时行为一致性问题.工具设计与实现内容包括:输入输出接口、顺序图模型的预处理转换、状态空间数据结构设计、抽象验证算法的实现以及通信构件组合系统的实例应用分析.     

航天嵌入式软件代码逻辑分析

为提高航天嵌入式软件的测试质量、确保航天型号任务的圆满完成,对航天嵌入式软件代码审查重要内容之一的代码逻辑分析进行了研究.通过对软件缺陷的机理、缺陷查找过程、缺陷暴露过程、以及缺陷引发后果的分析,结合多年软件测试工程实践经验的总结,提出了场景分析法、时序分析法、假想故障追源法等10种主要的代码逻辑分析方法.开展了代码逻...     

基于Specman的嵌入式软件验证的设计流程

基于Specman的硬件验证环境,给出一个嵌入式软件验证的设计流程。利用该设计流程,对Linux下的USB驱动程序进行验证,并成功找到该程序旧版本中的一个缺陷。     

New AspectJ Pointcuts for Integer Overflow and Underflow Detection

ABSTRACT

Aspect-oriented Programming (AOP) appears to be a promising paradigm for software security hardening. Using AOP, security experts can be responsible for coding security properties, and developers can concentrate on the basic functionality of the program. AspectJ extends the Java programming language to implement crosscutting concerns modularly in general. In this paper, we have extended AspectJ with new pointcuts in order to detect integer overflows and underflows in Java. Integer overflows and underflows in Java occur silently without throwing an exception. A malicious user can exploit them to produce a security breach. Hence, we implement new pointcuts: addition, multiplication, and subtraction that allow to write advices around integer arithmetic operations to detect integer overflow and underflow and consequently prevent considerable number of security breaches.     

中断驱动控制系统的有界模型检验技术

针对一类中断驱动的航天控制系统,给出了有界模型检验的算法.这类系统由中断处理程序和操作系统调度的任务组成.当中断发生时,对应的中断处理程序响应中断事件,并可以修改控制变量值,以便在系统任务中完成后续工作.操作系统周期性地调度任务序列处理日常事务以及中断事件的后续工作.使用了带中断标记的时间自动机对中断事件和任务调度事件进行建模,并使用中断向量表和中断处理程序的伪代码模型共同描述中断的处理过程.控制变量将中断处理过程和系统任务相关联,中断处理程序可以设定某个控制变量,而系统任务则通过检查该控制变量来确定是否需要进行后续处理.对于这样的形式化模型,给出了检验关键时序性质的有界模型检验算法.该算法使用深度优先的方式遍历所有长度小于等于K的可行路径,并使用SMT Z3实现了对时间约束和规约的处理.     

一种面向CPS的控制应用程序协同验证方法

信息-物理融合系统是一种新型嵌入式系统计算模式,它集成了控制计算过程和受控对象,二者相互影响并有机结合.随着信息技术在现实世界中更加广泛、深入的应用,智能化程度不断提升,在具有信息物理紧密耦合特点的嵌入式系统中,嵌入式控制软件的功能比重急剧上升,作用更加突出.作为安全攸关的系统,需要引入形式化验证方法来保证嵌入式控制应用软件的安全性.本文基于自动机理论建立统一的系统验证模型,并针对系统的可达性、安全性（safety）和活性（liveness）等属性要求,提出了对该模型进行形式化验证的算法：基于有界模型检验方法,基于可达性将对系统模型的相关属性验证问题转换为可满足性判定问题.将活性转换为Büchi自动机,并基于四值语义进行判断.在求解过程中,通过偏序规约等手段化简了问题求解的规模,提高可验证系统的规模.另外结合协同仿真技术,灵活配置验证的场景,提高验证的可用性.实验结果表明,结合仿真,形式化协同验证方法可以有效地对系统进行验证.     

基于流程图的嵌入式软件能耗模型

采用基于流程图的能耗模型对嵌入式软件的能耗进行估计,首先以流程图分析C语言程序流,对于流程图中无法体现的能耗以修正值的形式进行补偿,最终建立软件能耗模型。为了验证该模型的可行性,给出实际电路测量方法。实验结果表明,在ADSP21375硬件平台下,该模型软件能耗估计值和实际测量值的误差较小。该方法可以使软件设计者在系统开发初期对能耗进行估计,便于设计合理的程序语句对系统能耗进行优化。