Model Checking在病毒行为验证中的研究与应用

扫码查看

原文链接

NETL

中文摘要：随着计算机网络技术的迅猛发展,计算机病毒的传播和攻击方式日新月异,严重威胁大型网络应用解决方案的安全性和可靠性.传统反病毒技术主要是信赖于各种形式的基于签名的指纹来表征一个具体的病毒,为了维护系统的安全性,终端用户的签名库(病毒库)就需要不断的进行更新以发现并清除最新的病毒.为免去频繁更新病毒库给终端用户造成的诸多不便,本文给出一种基于ModelChecking的形式化验证方法,通过用线性时序逻辑来抽象表示病毒的行为特征,结合逆向工程来验证一可执行的静态二进制代码是否具有恶意行为.最后提出今后工作重点是进行ModelChecking在动态病毒行为验证领域的研究.

作者：

赵建利、河北师范大学数学与信息科学学院、宋雨、郭丰娟、孙召伟

展开 >

作者单位：

华北电力大学计算机学院,河北,保定,071003

河北,石家庄,050016

河北省毕业生就业指导中心,河北,石家庄,050061

关键词：

计算机病毒形式化方法 Model Checking 软件工程病毒验证网络安全

主办单位：

中国计算机学会

会议名称：

2004’全国软件与应用学术会议（NASAC）

会议时间：

2004-09-01

会议地点：

北京

会议母体文献：

软件技术进展

页码：

29-31

出版时间：

2004