基于时序逻辑模型验证的入侵检测方法研究

摘要

目前国际上已实现的入侵检测系统绝大多数使用模式匹配来检测入侵。随着网络数据量的增大，上述系统面临着一些难以解决的问题。为此，一些形式化的方法被提了出来并被应用到入侵检测系统中去。其中基于命题线性时序逻辑(PLTL)的方法即为其中具有代表性的一种，并被证实可用来检测可变化的复杂攻击。然而，基于PLTL的方法与其他相关方法相比，其综合性能有哪些优势与不足，目前尚不清楚，这是本文开展研究和解决的问题。本文所做的主要工作包括两个部分:
　　(1)详细分析了误用检测技术中的模式匹配算法（MPA）和基于模型检测的入侵检测算法(MCA)。并在KDD99数据集的基础上，构造基于行为的入侵检测数据集，开展仿真实验，从而对这两个算法的检测能力、检测效率进行了比较。
　　(2)提出了一种基于投影时序逻辑(PTL)的多类型攻击检测方法(USA)。该方法主要通过对攻击者、攻击过程、攻击效果建立形式化子模型，利用PTL把子模型结合起来，得到多类型攻击的PTL公式模型。将数据集和公式模型作为输入，利用模型检测算法来检测入侵。实验结果表明，新方法的检测能力更加全面和有效。
　　上述的研究工作对入侵检测算法的性能比较获得了一些初步结论，从而为实际应用中相关算法的选择提供了参考依据。

目录

声明

摘要

1 绪论

1．1 研究背景

1．2 入侵检测技术发展史

1．3 研究的内容及解决的关键问题

1．4 论文组织结构

2 预备知识

2．1 入侵检测

2．1．1 基于入侵知识的入侵检测

2．1．2 基于行为的入侵检测

2．2 模型检测

2．3 命题线性时序逻辑(PLTL)

2．4 Dijkstra的guard command语言

2．5 传统入侵检测算法

2．5．1 日志记录

2．5．2 模式匹配算法(MPA)

2．5．3 算法分析

2．6 本章小结

3 基于模型检测技术的入侵检测算法

3．1 检测原理

3．2 对形式化公式构造自动机

3．2．1 由PLTL公式构造图

3．2．2 由图构造自动机

3．3 基于模型检测的入侵检测算法(MCA)

3．4 算法分析

3．5 本章小结

4 基于KDD99数据集的仿真实验与性能分析

4．1 KDD99介绍

4．2 异常类型公式模型

4．3 构造记录集合

4．4 实验结果对比分析

4．5 本章小结

5 基于投影时序逻辑的多类型攻击检测方法

5．1 投影时序逻辑

5．2 多类型攻击检测(USA)原理

5．3 构造PTL攻击模型公式

5．4 实验结果比较分析

5．5 本章小结

6 总结与展望

6．1 总结

6．2 展望

参考文献

个人简历、在学期间发表的学术论文及研究成果

致谢