基于时序逻辑的3种网络攻击建模

Modeling for Three Kinds of Network Attacks Based on Temporal Logic

与其他检测方法相比,基于时序逻辑的入侵检测方法可以有效地检测许多复杂的网络攻击。然而,由于缺少网络攻击的时序逻辑公式,该方法不能检测出常见的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.