基于实时区间逻辑模型验证的入侵检测---形式理论与关键算法

项目名称： 基于实时区间逻辑模型验证的入侵检测---形式理论与关键算法

项目编号： No.U1204608

项目类型： 联合基金项目

立项/批准年度： 2013

项目学科： 计算机科学学科

项目作者： 朱维军

作者单位： 郑州大学

项目金额： 28万元

中文摘要： 与基于模式匹配的方法相比，基于时序逻辑模型验证的方法可更有效实现对网络攻击变化模式的刻画和对复杂攻击动作的自动检测。然而，现有的基于模型验证的误用检测技术均无法对具有实时并发特征的攻击进行自动检测。为解决该问题，本项目探索新的基于模型验证的误用检测的基础性、普适性方法。定义适合描述实时并发攻击的新的实时区间逻辑；给出新逻辑的模型验证算法，为入侵检测提供核心引擎；研究新逻辑的表达性理论，以界定其描述攻击的能力；研究新逻辑的判定复杂性理论，以获得有关入侵检测算法时空复杂性的相关结论。针对多类型攻击，寻找新逻辑的建模方法；研究从模型验证算法到入侵检测算法的无缝嵌入；结合不同类型攻击检测的不同特点，对检测算法优化状态空间；在新算法基础上开发原型工具，通过实验检验新方法的优势。新型通用方法的提出将为误用检测基础技术从原理上提升对复杂攻击的检测能力开拓一条新路径。

中文关键词： 误用检测；模型验证；实时；时序逻辑；时间约束

英文摘要： Compared with the methods based on pattern matching, the ones based on model checking temporal logic can portray effectively the changing pattern of network attacks, and they can realize automatic detection of complex attack actions. However, the existing misuse intrusion detection techniques based on model checking can not automatically detect the attacks with real-time features. To address the problem, this project will explore a new basis of model-checking-based misuse detection, and we will give a novel universal method. First, suitable description of real-time concurrent attacks will be defined with a new interval logic which can express real-time properties. Second, a model checking algorithm for the new logic will be presented, and it will provide the core engine to intrusion detection systems. Third, expressive ability of the new logic will be study in order to make us clear its ability to describe the attacks. Fourth, complexity theory of the new logic will be study in order to obtain the relevant conclusions of the intrusion detection algorithms with regard to time complexity. Fifth, an approach for modeling multiple types of attacks with the new logic will be obtained, and on the basis of it, an approach for embedding the model checking algorithm into the intrusion detection one will be obtained too.

英文关键词： misuse detection；model checking；real-time；temporal logic；time constraints