一种提高时序安全属性静态检测实用性的方法

程序时序安全属性可以用有限状态自动机(FSM)来描述,对该属性的静态检测是当前研究的热点之一.该文提出了FSM切片技术,以需求驱动的模式抽取出关于时序安全属性等价的程序切片.该切片使检测规模减小、程序结构简化,因而减小了检测中组合爆炸情形出现的机会,最终使时序安全属性的静态检测在准确性和可伸缩性上都得到了提高.实验表明,FSM切片可以使Saturn的可伸缩性平均提高到原来的6.34倍,使Fastcheck的准确性平均提高到原来的1.20倍.

改进的程序时序安全属性模型检测技术

针对程序时序安全属性模型检测技术改进模型检测算法,使安全漏洞状态机以函数为单位进行扩展,简化程序模型检测过程,以提高检测效率。在检测过程中加入别名分析,考虑安全操作之间的数据流依赖关系,以提高检测的准确性。实验结果表明,改进后的方法比原检测方法具有更高的效率和准确性。

模型检验技术在软件漏洞自动挖掘中的应用

将在工业设计领域应用很成功的模型检验技术引入到信息技术软件产品的安全漏洞挖掘中,提出了针对源码的漏洞挖掘系统原型,以开放源代码的操作系统Linux为例,建立了特权释放和文件创建的安全属性模型,并举例加以验证.研究结果表明:该方法是一种自动化挖掘软件安全漏洞并证明漏洞存在性的形式化方法,对挖掘已经确认机理类型的漏洞非常有效.