摘要
与其他检测方法相比,基于时序逻辑的入侵检测方法可以有效地检测许多复杂的网络攻击。然而,由于缺少网络攻击的时序逻辑公式,该方法不能检测出常见的back,ProcessTable以及Saint 3种攻击。因此,使用命题区间时序逻辑(ITL)和实时攻击签名逻辑(RASL)分别对这3种攻击建立时序逻辑公式。首先,分析这3种攻击的攻击原理;然后,将攻击的关键步骤分解为原子动作,并定义了原子命题;最后,根据原子命题之间的逻辑关系分别建立针对这3种攻击的时序逻辑公式。根据模型检测原理,所建立的时序逻辑公式可以作为模型检测器(即入侵检测器)的一个输入,用自动机为日志库建模,并将其作为模型检测器的另一个输入,模型检测的结果即为入侵检测的结果,从而给出了针对这3种攻击的入侵检测方法。
Compared with other detection methods,the intrusion detection methods based on temporal logic can detect many complex network attacks effectively.There is no network attack temporal logic formula,so common back,ProcessTable and Saint attacks can not be detected using the above method.Thus,this paper employed propositional interval temporal logic(ITL)and real-time attack signature logic(RASL)to model the temporal logic formula for the three attacks,respectively.In general,based on attack basic principle of the three attacks,the key attack steps are decomposed into atomic actions.Next,this paper defined atomic propositions.Lastly,according to the relationship between the atomic propositions,this paper constructed the network attack temporal logic formula which is an input of the model checker.In addition,the automaton was used to model the log library as another input of the model checker.The output of the model checker is the result of intrusion detection in the three network attacks.Besides,the intrusion detection method for three attacks was given.
出处
《计算机科学》
CSCD
北大核心
2018年第2期209-214,共6页
Computer Science
基金
国家重点研发计划(2016YFB0800100)
国家自然科学基金(U1204608
U1304606
61572444)
中国博士后科学基金(2015M572120
2012M511588)资助
关键词
命题区间时序逻辑
实时攻击签名逻辑
模型检测
入侵检测
Propositional interval temporal logic
Real-time attack signature logic
Model checking
Intrusion detection