有界模型检查可执行文件的安全属性

引入模型检查方法对可执行文件进行脆弱性分析.对可执行文件形式化建模,采用有界模型检查技术验证可执行文件的安全属性,并在X86体系结构上开发了一个用于可执行文件的模型检查器.实验以内存泄漏和栈溢出漏洞为例,将其属性描述为线性时序逻辑公式,在可执行文件的状态迁移系统模型中验证公式是否能满足,实验结果表明对可执行文件的有界模型检查是一种有效的静态分析方法.

语义标识的过程模型的可执行性分析

语义标识的过程模型是基于领域本体对过程模型中活动的前置条件&效果进行标识后所产生的模型.语义过程模型的可执行性问题是确保语义过程模型质量的核心问题,同时已被证明是一个co-NP难问题.基于关联变量集模型定义了语义过程模型的动态语义;定义了该动态语义的命题公式的编码规则;提出了基于可满足性求解器的可执行性分析方法;该方法能判定可执行性问题同时当模型不满足可执行性时能反馈出有问题的活动;此外,实现了相应的原型工具SPMT,该工具支持对语义过程模型的建模及可执行性分析;最后通过实际例子对以上理论及工具进行了有效性验证.

基于在线模型检验技术的微内核验证

物联网的兴起,对操作系统的可靠性提出了更高的要求。为确保微内核操作系统的安全性,提出了一种基于事件总线的微内核在线模型验证框架,主要思想是通过映射函数将源代码转换成抽象模型,并从微内核规范中抽取性质。根据源代码的控制流程图查找监控点并进行插桩;在微内核运行过程中,定期监测实际运行信息,并将之转化为抽象信息提交给抽象模型,通过有界模型检查,查看是否满足性质;若不满足,则表明源代码可能存在错误。最后,该验证框架应用于本团队自行开发的基于事件总线的微内核验证中。