| 一种基于模型检测的二进制程序脆弱性分析框架 |
| |
| 引用本文： | 王春雷,刘强,赵刚,戴一奇.一种基于模型检测的二进制程序脆弱性分析框架[J].计算机科学,2010,37(4):120. |
| |
| 作者姓名： | 王春雷 刘强 赵刚 戴一奇 |
| |
| 作者单位： | 1. 清华大学计算机科学与技术系,北京,100084;北京系统工程研究所网络技术研究室,北京,100101
2. 北京系统工程研究所网络技术研究室,北京,100101 |
| |
| 基金项目： | 国防预先研究项目(513150601)资助 |
| |
| 摘 要： | 针对二进制程序脆弱性分析的实际需求,提出了一种基于模型检测的二进制程序脆弱性分析框架。首先定义了二进制程序的抽象模型,描述了基于有限状态自动机的软件脆弱性形式化表示和基于事件系统的软件安全属性表示方法。在此基础上,提出了基于模型检测的脆弱性分析过程和算法。根据该分析框架,设计并实现了二进制程序脆弱性分析工具原型。通过脆弱性分析实验,详细说明了该框架的工作原理,验证了该分析方法的有效性。
|
| 关 键 词： | 模型检测 二进制程序 脆弱性分析 形式化方法 |
| 收稿时间： | 2009/5/20 0:00:00 |
| 修稿时间： | 2009/7/23 0:00:00 |
Vulnerability Analysis Framework for Binaries Based on Model Checking |
| |
| WANG Chun-lei,LIU Qiang,ZHAO Gang,DAI Yi-qi.Vulnerability Analysis Framework for Binaries Based on Model Checking[J].Computer Science,2010,37(4):120. |
| |
| Authors: | WANG Chun-lei LIU Qiang ZHAO Gang DAI Yi-qi |
| |
| Affiliation: | Department of Computer Science and Technology/a>;Tsinghua University/a>;Beijing 100084/a>;China;Laboratory of Network Technology/a>;Beijing Institute of System Engineering/a>;Beijing 100101/a>;China |
| |
| Abstract: | In order to analyze vulnerabilities in executable programs,a vulnerability analysis framework for binaries based upon model checking was proposed.Firstly,the abstract model of binary was defined,and the formal models of vulnerabilities based upon finite state automaton and the representations of software security attributes based upon event system were described.Then,the model checking based vulnerability analysis process and algorithm were proposed with respect to the abstract models of binaries and the se... |
| |
| Keywords: | Model checking Vulnerability analysis Formal method |
| 本文献已被 CNKI 万方数据 等数据库收录！ |
|
点击此处可从《计算机科学》下载全文 |
|
