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

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. Sixth, for the different characteristics of the detections of different types of attacks, the algorithm will be optimized to reduce the state space. Seventh, some experiments will be conducted to verify the comparative advantages of the new method. The new universal method for the misuse detection will enhance the detection ability of complex attacks, and it will open up a new pathway under the fundamental principle.

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

与基于模式匹配的方法相比，基于时序逻辑模型验证的方法可更有效实现对网络攻击变化模式的刻画和对复杂攻击动作的自动检测。然而，已有的基于模型验证的误用检测技术均无法对具有实时并发特征的攻击进行自动检测。为解决该问题，本项目探索新的基于模型验证的误用检测的基础性通用方法，为误用检测基础技术从原理上提升对复杂攻击的检测能力开拓出一条新路径。.研究成果：.(1)、定义了一个新的时序逻辑，可描述复杂攻击行为的实时并发特征。.(2)、给出了该逻辑的模型验证算法，为入侵检测提供核心引擎。.(3)、构建了新逻辑的表达性理论，获得了有关新方法检测攻击之能力的一系列结果。.(4)、构建了新逻辑的判定复杂性理论，获得了有关新算法检测攻击之效率的一系列结果。.(5)、使用新逻辑为39种攻击类型建立了模型，有效拓展了模型验证入侵检测共性技术的使用范围。.(6)、研究了新方法针对不同常见攻击类型的相对优劣，获得相关一系列结果。.(7)、针对入侵检测的模型验证基础开展更多探索，研究时序逻辑模型验证的非经典方法，给出了使用DNA分子实施模型验证计算的若干算法。