# A Novel Algorithm for Intrusion Detection Based on RASL Model Checking

Authors: Weijun Zhu; Qinglei Zhou; Weidong Yang; Haibin Zhang
Journal: Mathematical Problems in Engineering
 (2013)

---

## Abstract

The interval temporal logic (ITL) model checking (MC) technique enhances the power of intrusion detection systems (IDSs) to detect concurrent attacks due to the strong expressive power of ITL. However, an ITL formula suffers from difficulty in the description of the time constraints between different actions in the same attack. To address this problem, we formalize a novel real-time interval temporal logic—real-time attack signature logic (RASL). Based on such a new logic, we put forward a RASL model checking algorithm. Furthermore, we use RASL formulas to describe attack signatures and employ discrete timed automata to create an audit log. As a result, RASL model checking algorithm can be used to automatically verify whether the automata satisfy the formulas, that is, whether the audit log coincides with the attack signatures. The simulation experiments show that the new approach effectively enhances the detection power of the MC-based intrusion detection methods for a number of telnet attacks, p-trace attacks, and the other sixteen types of attacks. And these experiments indicate that the new algorithm can find several types of real-time attacks, whereas the existing MC-based intrusion detection approaches cannot do that.


---

## Body

## 1. Introduction

Intrusion detection (ID) is an important network security technique. ID can be divided into anomaly intrusion detection and misuse intrusion detection in terms of the different principles of ID. The former can find unknown types of attacks. However, false positives rate of anomaly intrusion detection is often very high. In contrast, a misuse intrusion detection system has a comparatively low false positives rate with regard to known types of attacks. This is due to the principle of misuse intrusion detection: IDS developers predefine their known types of attacks, use appropriate language to describe these types, and establish libraries of attack patterns (called misuse signatures). The system will monitor the audit log. Once a data stream in the log is found to match with certain attack type, it means that an attack is found.However, such a class of detection methods based on pattern matching (PM) suffers from their inherent problems. First, affected by intruders’ subjective wishes or other random factors, the logical relationship among its atomic actions associated with attacks of the same pattern launched by different intruders may present different features [1, 2], where an atomic action means a minimum operation step in an attack. It is hard to depict precisely so vastly different attacks with a relatively small-scale attack pattern library. Second, a large-scale coordinated attack requires an intrusion detection algorithm to handle a large volume of network data in a short period of time. To address these issues, a series of intrusion detection methods based on model checking have been developed.A relatively comprehensive algorithm has been presented, and it is based on linear temporal logic (LTL) model checking [1]. Its basic principle can be formulated as follows: (1) use an LTL formula to describe an attack pattern as well as an automaton to record what happened in the audit log, and (2) use a model checking algorithm to check whether the automaton satisfies the formula (i.e., whether the records in log match the attack pattern). Since current model checking algorithms have been able to check up to 10120 states, they are particularly suitable for the large-scale attack detection [3], and the operators in LTL formulas can flexibly describe various logical relationships between atomic attack actions.Compared with the PM-based approaches, the MC-based ones can effectively portray the ever-changing attack patterns [1, 3]. Furthermore, the MC-based approaches have an important advantage for intrusion detection over the PM-based ones. Pattern matching is usually applicable to detect inconsistencies between data while automata, temporal logic formulas, and model checking techniques are applicable to detect inconsistencies of behaviors. Thus, the MC-based methods can do something more than the PM-based ones since intrusion attacks involve complex behaviors besides the comparatively simple data.However, the algorithm in [1] can realize the automatic detection for neither concurrent attacks nor real-time (i.e., time constraint relation) attacks because LTL formulas cannot be used to describe multiprocess activities or time constraint relationships between attack actions or attack action sequences. As the first attempt to address these issues, a method based on ITL model checking was presented in [2], and it can describe and detect concurrent attacks, since ITL has more power than LTL. However, ITL-model-checking-based methods still cannot describe and detect real-time attacks. For example, there are a large number of attacks with the following characteristic in a real network intrusion: No more than n seconds after action (sequence/process) A occurs, action (sequence/process) B occurs. Here, the condition “no more than” can be replaced by more than, less than, no less than, or equal to. The existing MC-based algorithms cannot find these attacks.Therefore, motivated by addressing both concurrent attacks and real-time attacks simultaneously, we, in this paper, present a new interval temporal logic to describe conveniently the real-time attack signatures and also put forward a new MC-based approach to automatically detect the various changing modes of real-time attacks.We conducted some simulation experiments and a benchmark test (see Section7). The detection of several groups of attacks, such as telnet attacks and p-trace attacks, is simulated on MATLAB. The experiment results verify that (1) the new algorithm finds more attacks than the existing MC-based algorithms; (2) the new algorithm finds real-time attacks. This is the main contribution of this paper.The remainder of this paper is organized as follows. Section2 illustrates some related works and compares them with the new approach. Section 3 defines a new logic, RASL, and gives its formal syntax and semantics. Section 4 uses RASL formulas to establish some models for attack patterns. Several examples of models are given in Section 5. Section 6 formalizes a RASL model checking algorithm based on a new data structure called timed normal form graph (TNFG), and a misuse intrusion detection algorithm is presented. Section 7 presents several groups of experiments and compares the new algorithm with the existing ones with regard to the description capabilities and detection capabilities for intrusion attacks. Section 8 draws the conclusions of this paper.


## 2. Related Works

### 2.1. Detect Various Attack Types Using Model Checking Linear Temporal Logics

A tool called ORCHIDS was developed [3], which fulfilled the LTL-model-checking-based method for intrusion detection in reality [1]. In one experiment, ORCHIDS found some p-trace attacks [4] which usually exploit the flaws in process calls to inject malicious code. It is difficult for traditional intrusion detection systems to find this type of attacks because they only match individual events [4]. The ORCHIDS was improved in [5]. In a real environment, it successfully detected a series of wireless network attacks [5], including deauthentication flooding, rogue access points, and Chop-Chop. This is the first IDS to successfully detect Chop-Chop attacks [5]. Furthermore, to avoid repeated verifications needed by the algorithm in [1], an improved algorithm was put forward in [6], which is able to compute the number of guesses in password attacks.Compared with the methods mentioned above, the new algorithm can be used to detect complex concurrent attacks and real-time attacks (See Section7).


### 2.2. Detect Various Attack Types Using Model Checking Interval Temporal Logics

ITL was put forward in [7]. With its successful and broader adoption and adaptation [8–11], ITL is becoming a class of logics, including some non-real-time interval logics [7] and some real-time interval logics [12–14]. Figure 1(a) illustrates the relationships between some temporal logics.(a) Some temporal logics and their classification. (b) Some logics and their expressive power.
(a)
(b)There are some studies that use interval temporal logics to describe attack patterns so that more intrusion behaviors can be expressed [15–17]. However, these papers do not mention how to detect these attacks automatically. The method presented in [2] can do it automatically, but it can only find concurrent attacks rather than real-time attacks. In contrast, as a real-time interval logic, RASL has more expressive power (see Figure 1(b)), which can be used to describe the time relationships among attack activities, and our model checking algorithm can find real-time intrusion attacks in a fully automatic manner (See Section 7).


## 2.1. Detect Various Attack Types Using Model Checking Linear Temporal Logics

A tool called ORCHIDS was developed [3], which fulfilled the LTL-model-checking-based method for intrusion detection in reality [1]. In one experiment, ORCHIDS found some p-trace attacks [4] which usually exploit the flaws in process calls to inject malicious code. It is difficult for traditional intrusion detection systems to find this type of attacks because they only match individual events [4]. The ORCHIDS was improved in [5]. In a real environment, it successfully detected a series of wireless network attacks [5], including deauthentication flooding, rogue access points, and Chop-Chop. This is the first IDS to successfully detect Chop-Chop attacks [5]. Furthermore, to avoid repeated verifications needed by the algorithm in [1], an improved algorithm was put forward in [6], which is able to compute the number of guesses in password attacks.Compared with the methods mentioned above, the new algorithm can be used to detect complex concurrent attacks and real-time attacks (See Section7).


## 2.2. Detect Various Attack Types Using Model Checking Interval Temporal Logics

ITL was put forward in [7]. With its successful and broader adoption and adaptation [8–11], ITL is becoming a class of logics, including some non-real-time interval logics [7] and some real-time interval logics [12–14]. Figure 1(a) illustrates the relationships between some temporal logics.(a) Some temporal logics and their classification. (b) Some logics and their expressive power.
(a)
(b)There are some studies that use interval temporal logics to describe attack patterns so that more intrusion behaviors can be expressed [15–17]. However, these papers do not mention how to detect these attacks automatically. The method presented in [2] can do it automatically, but it can only find concurrent attacks rather than real-time attacks. In contrast, as a real-time interval logic, RASL has more expressive power (see Figure 1(b)), which can be used to describe the time relationships among attack activities, and our model checking algorithm can find real-time intrusion attacks in a fully automatic manner (See Section 7).


## 3. RASL

Definitions1 and 2 give the formal description of the syntax of RASL, whereas the other definitions present its semantics. Compared with ITL [11, 18, 19], the additional operator denoted as “;I”  in RASL is appended for the description of time constraints between intervals.Definition 1.
RASL formulas have the following syntax given in the Backus-Naur form:(1)
termst::=T∣Tf,(2)
constraint formulasδ::=Tf≤c∣Tf<c∣Tf>c∣Tf≥c∣δ1∧δ2,(3)
interval formulasφ::=p∣skip∣(φ1,…,φm)prjφ0∣(φ1,…,(φi,…,φj)Θ,…,φm)prjφ0∣φ1;φ2∣φ*∣φ1∨φ2∣φ1∧φ2∣φ1||φ2,(4)
timed formulasψ::=φ∣δ∣ψ1∧ψ2∣ψ1∨ψ2∣ψ1;ψ2Definition 2.
The derived formulas are defined as follows:
(
1
)
◯
p
:
:
=
s
k
i
p
;
p, (2)more::=◯true, (3)empty::=◯false, (4)p;Iq::=(p∧Tf∈I);qDefinition 3.
A states is a tuple (a,t), where a={x∣x∈AP∧x=true} and t:T→N denotes the absolute time of the current state.Definition 4.
A timed sequence of states is defined and also denoted asσ=〈s0,s1,…,si,…〉, where si is a state.Definition 5.
An interpretation is a quadrupleI=(σ,i,k,j), where σ is a timed sequence of states over 〈si,…,sk,…,sj〉, i,k,j∈N,andsk is the current state. We use the notation len(σ)=|σ|=j-i for the number of states in interval and lent(σ)=st(j)-st(i) for the time distance between the endpoints in interval, where st(i) is the absolute time of state si.Definition 6.
Letσ=〈s0,s1,…,s|σ|〉 an interval, r1,…,rh be integers, and 0≤r1≤r2≤⋯≤rh≤|σ|. We use notation σ↓(r1,…,rh)=〈st1,st2,…,stl〉 to denote a projection from σ to r1,…,rh, where  t1,…,tl is obtained by deleting the duplicate numbers from r1,…,rh.Definition 7.
Letc∈N and sp(k) be the true value of p∈AP in state sk. The satisfaction relation is inductively defined as follows:(1)
T=st(k),(2)
Tf=st(j)-st(k),(3)
I⊨Tf≤C if and only if st(j)-st(k)≤C,(4)
I⊨Tf≥C if and only if st(j)-st(k)≥C,(5)
I⊨Tf<C if and only if st(j)-st(k)<C,(6)
I⊨Tf>C if and only if st(j)-st(k)>C,(7)
I⊨δ1∧δ2 if and only if I⊨δ1 and I⊨δ2,(8)
I⊨p if and only if sp(k)=  true,(9)
I⊨φ1∧φ2 if and only if I⊨φ1 and I⊨φ2,(10)
I⊨φ1∨φ2 if and only if I⊨φ1 or I⊨φ2,(11)
I⊨φ1;φ2 if and only if ∃r,k≤r≤j, such that (σ,i,k,r)⊨φ1 and (σ,i,k,r)⊨φ2,(12)
I⊨skip if and only if len(σ)=1,(13)
I⊨φ1||φ2 if and only if φ1∧(φ2;true)∨φ2∧(φ1;true),(14)
I⊨φ* if and only if (i) there exist finite many r0,…,rn∈Nω, such that k=r0≤r1≤⋯≤rn-1≤rn=j,(σ,i,k,r0)⊨φ, and for every 1≤l≤n,(σ,rl-1,rl-1,rl)⊨φ0 (ii) or k=j,(15)
I-prj:I⊨(φ1,…,φm)prjψ, if and only if there exist integers k=r0≤r1≤⋯≤rm≤j and (σ,i,k,r1)⊨φ1,…,(σ,rn-1,rn-1,rn)⊨φn, where 1<n≤m,  such that for σ′ in the two cases mentioned below, we have (σ′,0,0,|σ′|)⊨ψ—(i) rm<j and σ′=σ↓(r0,…,rm)·σ(rm+1,…,j), (ii) rm=j and σ′=σ↓(r0,…,rh),0≤h≤m,(16)
I⊨(φ1,…,(φi,…,φj)Θ,…,φm)prjφ0 if and only if there exists n∈N0, such that I⊨(φ1,…,(φi,…,φj)n,…,φm)prjφ0,(17)
I⊨ψ1∧ψ2 if and only if I⊨ψ1 and I⊨ψ2,(18)
I⊨ψ1∨ψ2 if and only if I⊨ψ1 or I⊨ψ2,(19)
I⊨ψ1;ψ2 if and only if ∃r,k≤r≤j, such that (σ,i,k,r)⊨ψ1 and (σ,i,k,r)⊨ψ2,


## 4. Construct Signatures with RASL Formulas

We can use RASL formulas to construct signatures, that is, specifications of attack patterns. Compared with linear temporal logic, RASL has been additionally equipped with interval semantics. So, a phase, that is, a sequence of atomic actions, in an attack can be described with an interval in a RASL formula, while various steps in the phase can be described with various points in the interval [2]. Temporal relationship between steps in an attack can be described with temporal operators. Logical relationship between various phases can be described with operator “;” [2]. And a concurrent attack can be described with a formula with the operator “∥”. Compared with ITL, RASL can express more. Particularly, repeated attacks can be described with operator “*” or “prjΘ”, and a time constraint between phases or steps in an attack can be described with operator “;I”.Table1 presents how to construct formal models for intrusion attacks with RASL formulas. And Figure 2 illustrates sequential relationships, concurrent relationships, and time relationships between behaviors in an attack.Table 1
The way of constructing models for attacks: behaviors and their RASL formulas.
Attack behaviors
RASL formulas defined for description of behaviors
a
j means an atomic action
A state formulawj
A
i
=
a
1
,
…
,
a
m means a phase in an attack
φ
i
=
(
(
w
1
∧
s
k
i
p
)
;
t
r
u
e
)
;
…
;
(
(
w
m
∧
s
k
i
p
)
;
t
r
u
e
)
a
=
A
1
,
…
,
A
n means an attack
φ
=
(
φ
1
∧
s
k
i
p
)
;
t
r
u
e
;
…
;
(
φ
n
∧
s
k
i
p
)
;
t
r
u
e
a
j is repeated k times
φ
=
l
e
n
(
k
)
∧
(
w
j
∧
s
k
i
p
)
*
A
i is repeated k times
φ
=
(
(
φ
i
∧
s
k
i
p
)
Θ
,
b
)
p
r
j
(
(
(
t
r
u
e
∧
s
k
i
p
)
*
∧
l
e
n
(
k
+
1
)
;
c
)
)
∧
□
(
b
↔
c
)
Result ofaj is tfj, tfj∈{fail,success}
φ
=
(
w
j
∧
e
m
p
t
y
)
p
r
j
t
f
j
a
=
A
1
,
…
,
A
n, where result of Ai is tfi
φ
=
(
(
φ
1
∧
s
k
i
p
)
;
t
r
u
e
,
…
,
(
φ
n
∧
s
k
i
p
)
;
t
r
u
e
)
p
r
j
(
t
f
1
∧
◯
t
f
2
∧
…
∧
◯
n
-
1
t
f
n
)
a
=
A
1
|
…
|
A
n
φ
=
φ
1
∥
…
∥
φ
n
A
1 and A2 are two ways of the attack
φ
=
φ
1
∨
φ
2
Time constraint betweenAi and Ai+1 is Ii
φ
=
φ
1
;
I
1
…
;
I
n
-
1
φ
nDifferent relationship between behaviors in an attacka.
(a)
Sequential relationa=A1,A2
(b)
Concurrent relationa=A1∣A2
(c)
Time relationDefinition 8 (See [1]).
A record in a log library is modeled by a finite state automatonA.Theorem 9.
A record of a log can be modeled by a timed automatonA′.Proof.
According to Definition8, we know that a record of a log can be modeled by a finite state automaton A. For every transition e of A, we add time constraint “true”. For every state s of A, we extend s to (s,t), where t denotes absolute time. So, finite state automaton A is turned to timed automaton A′. The theorem holds.


## 5. A Case Study

As a case study, we discuss several examples to show the expressive capability of the above proposed models.Example 10.
Password cracking inconsecutive attack: failure. The RASL formula is(1)((connect∧emptyprjfail);true)*,
where connect means that an intruder is trying to connect. The intruder could launch another concurrent process before the end of current connection process. Thus, the subinterval that describes current execution of the concurrent connection process is over, and it can be described with operators beforeprj. The sub-interval that describes the result is over while this connection process fails, and it can be described with the operator failafterprj. The intruder repeatedly tries connection, and it can be described with “*”. Inconsecutive phenomenon between connections can be described with “;true”.Example 11.
Password cracking inconsecutive attack: success after connection failedk-1 times.
At first, one time failure in connection can be described asφf:=(connect∧emptyprjfail);true. And, then, a successful trial can be described as φs:=connect∧emptyprjsuccess.
The formula that describesk-1 times failures in connections can be defined as φf′:=(φfΘ,b)prj((true;skip);((fail∧skip)*∧(len(k-1));c))∧□(b↔c).
The formula that describes the attack can be defined as(2)φ:=(φf′∧skip);φs.As shown in Figure3, the definition of φf′ is illustrated, where k=4, that is,  φf′ denotes three times failures in connections. As shown in (a), (b), and (c) of Figure 3, there are three cases on the length of interval (φ1,φ2,φ3)prjφ0 in RASL formula. In each of the k-1 failures in connections, there exists a one-to-one map between attack actions and their results. That is to say, the number of φfs which describe attack actions is equal to the number of (fail)s that describe their results. This number is three, so only (c) of Figure 3 is correct. To this end, we can append atomic proposition b to the formula, and let b follow φfΘ. Furthermore, we can append atomic proposition c to the formula when subinterval fail* is over. The number of φfs is equal to the number of (fail)s if □(b↔c) holds, as shown in (c) of Figure 3.Three cases on different length of projection.
(a)
(b)
(c)Subintervalfail* is executed repeatedly k-1 times to guarantee k-1 times cycles of φf, as shown in Figure 4. We need two states in current subinterval fail to make sure that the first state of the next subinterval fail is the next state of the final state of the current subinterval. So, we replace fail* with (fail∧skip)*.Figure 4
Success after connection failed three times.Example 12.
Phases of a telnet attack are observed as follows.Phase 1: the telnet service is started, and it is described as atomic formulaq.Phase 2: the intruder closes firewall. There are three steps in this phase. At first, the intruder accesses C:∖windows in order to find program aproman. It is described as RASL atomic formula s1. And, then, the intruder executes command aproman-a[PID] and monitors all processes in order to find PID of firewall process. It is described as RASL atomic formula s2. At last, the intruder executes command aproman-t[PID] to close firewall. It is described as RASL atomic formula s3. The intruder performs the three steps of this phase in sequence with a gap between each step. Each of the two delays is less than n seconds, and it is described as ;I1∈[0,n).Phase 3: in order to login the system again in the future, the intruder makes a backdoor. There are two steps in this phase. The first step is to access directory in which fileinstsrv.exe exists, and step 2 is to execute command instsrv.exeSYSHE-ALTHC:∖windows∖SYSTEM32∖tlntsvr.exe in order to setup SYSHEAHTH service which is a backdoor. The former can be denoted as a RASL atomic formula t1, and the later can be denoted as a RASL atomic formula t2. The intruder performs the two steps of this phase in sequence with a gap between each step. The delay is less than m seconds, and it is described as ;I2∈[0,m).
In summary, the timed formula for the telnet attack is formulized as follows:(3)(((q∧empty);true);((((s1∧empty);true);I1∈[0,n),((s2∧empty);true);I1∈[0,n)((s3∧empty);true))∥,(((t1∧empty);true);I2∈[0,m)((t2∧empty);true)))).
In Formula (3), “;” is used to express a piecewise action, “∥” is used to express a concurrent action, and  “;I” is used to express a time constraint relationship.


## 6. RASL Model Checking Algorithm and Intrusion Detection Algorithm

We can give a subset of RASL called ASL, which is obtained by deleting all of the time constraints in RASL. Reference [18] gives a data structure called normal form graph (NFG) as well as a procedure called PRO(P) to construct the NFG model denoted as GP for an ASL formula P. Thus, an ASL model checking algorithm was obtained in [18]. Based on this work, we can obtain a RASL model checking algorithm and its intrusion detection algorithm.First, Definition13 presents a data structure called TNFG, which is a timed version of NFG.Definition 13.
For a formulaP∈LRASL, the TNFG of P is defined as a tuple G=(CL(P),EL(P),C), where C is a finite clock set, and the set CL(P) of nodes and the set EL(P) of edges are inductively defined as follows:(1)
Untime(P)∈CL(P), where Untime(P) is an ASL formula in which all CHOPIs in P are replaced by CHOP,(2)
for everyQ∈CL(P)∖{ε,false}, if Q≡Qe∧empty∨Vi=1r(Qi∧◯Qi′), ε∈CL(P), (Q,Qe,ε,δ,λ)∈EL(P), and for every i,  1≤i≤r, we have Qi′∈CL(P), (Q,Qi,Qi′,δ,λ)∈EL(P), where set λ gives the clocks to be reset and δ is a clock constraint,(3)
CL(P) and EL(P) are produced by (1) and(or) (2) only.
Second, Algorithm1 constructs TNFG models for RASL formulas. Some notations presented in the algorithm are explained in Table 2.
Third, if we append accepted conditions to TNFGs, we will obtain discrete timed automata models of RASL formulas. It is illustrated by Algorithm2.
Algorithm2 gives a procedure to compute discrete timed automaton A, that is, the model of RASL formula P. The model of P is the formal language accepted by the automaton.
Last, we can useA to describe an attack signature and another discrete timed automaton B to a record of the audit log. If ¬A∩B=ϕ, the result of model checking algorithm is that B satisfies P, else the result is that B does not satisfy P. We can surely say that IDS finds an attack if B satisfies P. Thus, the intrusion detection algorithm is obtained, as shown in Figure 5.
The inherent complexity of interval temporal logic model checking problem is nonelementary. The number of exponential order is proportional to the number of embedded not operators. The approach based on an NFG or TNFG reaches the lower bound of this problem [14, 19]. There is only one occurrence of the operator not in the new model checking algorithm. So, both the inherent complexity of the intrusion detection problem based on RASL model checking and the complexity of our algorithm, in the worst case, are exponential.Table 2
Some notations presented in Algorithm1.
Notations
Semantics
U
n
e
x
t
(
P
)
The set of all subformulas which do not occur in the domain of any operator next of normal form ofP∈LRASL
pre(N)
All the nodes which are parents ofN in G, where G is a TNFG and N is a node of G
S
u
b
(
P
)
The set of all subformulas ofP∈LRASL
U
n
c
h
o
p
(
P
)
A Boolean variable andUnchop(P)=true if and only if there exists no subinterval in P∈LRASLAlgorithm 1:Translation from a RASL formula to a TNFG.
TNFG(P)
Begin
PRO(Untime(P)); CL(P):= CL(Untime(P)); EL(P):= EL(Untime(P));
/* produce the NFG in which no clock constraint exists, where CL(Untime(P)) is the set of nodes
of the NFG of ASL formulaUntime(P), and EL(Untime(P)) is the set of edges of the NFG of ASL
formulaUntime(P)
T:=ϕ/*T is defined as a set, and it consists of all the nodes which have been converted from NFG to TNFG.
for allQs of CL(P) in the order of building NFG’s nodes, do the following:
T:=T∪{Q}
for allM;N∈Unext(Q) and Unchop(M) and M;N∉Sub(t∈T)
andM;IN∈Sub(P), do /* for all the clock constraints holding the conditions
new(x); /* allocate a new clock
for allEL(Q)=(Q,Qe,ε), do EL(Q):=(Q,Qe,ε,Ix=0,{x})
/*Ix=0 means that constraint I is satisfied when x=0, where I=δ
for allEL(Q)=(Q,Qi,Qi′), do EL(Q):=(Q,Qi,Qi′,true,{x})
/* the edges of NFG is converted to the ones of TNFG
for allEL(pre(w∧N)) do /* the current interval is over, where w is a state formula which may be
empty or not.
ifEL(pre(w∧N))=(R,Ri,Ri′) then EL(pre(w∧N)):=(R,Ri,Ri′,Ix,{x})
/* in the TNFG, the clock constraint is appended if it is satisfied.
end for
end for
end for
for all ofe in EL(P) do /* for all the converts which deal with no clock constraint
if e=(Q,Qi,Qi′), e:=(Q,Qi,Qi′,true,ϕ)/* the edges of NFG is converted to the ones of TNFG
end for
end TNFGAlgorithm 2:Constructing discrete timed automata for RASL formula.
function CONSTRUCT (G)
/* pre-condition:G = (CL(P), EL(P), X) is an TNFG of RASL formula P*/
/* post-condition: CONSTRUCT constructs a timed automaton from TNFG of formulaP*/
begin function
S:={P};S0:={P};Σ:=ϕ;E:=ϕ;
CL:=CL(P)/* CL denotes acceptance state set */
For allQ∈CL(P) do If Q is labeled F then CL:=CL/{Q}/*Acceptance state set doesn’t contain the circulate
nodes passed by finite times */
CL:=CL/{ε}/*Acceptance state set doesn’t contain the final states */
while  ∃el=(Q,Qci,Qni,δ,λ)∈EL(P)/*for every non-terminal edge of TNFG*/
do  s:=Q;s′:=Qni;a:=Qci;e:=(s,s′,a,δ,λ);E:=E∪{e}; /*add transition rules to timed automaton*/
S:=S∪{s,s′};Σ:=Σ∪{a}; /*add state and input alphabet to timed automaton
end while
while  ∃el=(Q,Qe,ε,δ,λ)∈EL(P) /*for every terminal edge of TNFG*/
do  s:=Q;s′:=ε;a:=Qe;e:=(s,s′,a,δ,λ);E:=E∪{e}; /*add transition rule to timed automaton*/
S:=S∪{s,s′};Σ:=Σ∪{a}; /*add state and input alphabet to timed automaton*/
end while
F:={ε};AC:=CL;/*set of final states and set of acceptance states*/
return  A=(Σ,S,S0,E,X,F,AC);
end function
Construction Procedure (P)
(1) Build the TNFG of P, G = (CL(P); EL(P), X), by algorithm TNFG(P);
(2) Obtain the timed automaton, A=(Σ,S,S0,E,X,F,AC), by algorithm CONSTRUCT(G′).Figure 5
Algorithm for intrusion detection based on RASL model checking (the main idea of this paper).


## 7. Simulation Experiments

In order to compare the existing approaches with our new algorithm, we conducted experiments by simulating and detecting telnet attacks and password attacks mentioned above as well as other types of attacks. The platform used is a PC with Dual core 3.2 GHz, 8 GB, and Windows XP SP3, along with MATLAB 2010. The results on detection ability are shown in Tables3, 4, and 5. The different results are due to the different expressive powers of the different logics.Table 3
A comparison of different MC-based approaches for detecting telnet attacks.
Attack actions∖detection results (if attacks are found)
ITL [2]
RASL
LTL [1]
Make a backdoor after/before/while close firewall
Yes
Yes
No
There exists an/no overlap timed interval between two actions
Yes
Yes
No
The time distance between two actions is less thann seconds
No
Yes
NoTable 4
Another comparison of different MC-based approaches for detecting telnet attacks.
Attack actions∖detection results (if  attacks are found)
ITL [2]
RASL
LTL [1]
Two attacks are launched at the same time point
Yes
Yes
No
The same attack is launched repeatedlyn times (n is a variable)
Yes
Yes
No
The same attack is launched repeatedlyk times (k is a given large constant)
Yes
Yes
No
The time distance between two actions is less thanm seconds
No
Yes
NoTable 5
Comparison of different MC-based approaches for detecting password attacks.
Attack actions∖detection results (if attacksare found)
ITL [2]
RASL
LTL [1]
Consecutive/inconsecutive attack: success after connection failedk-1 times (k is a given large constant)
Yes
Yes
No
Every time distance betweenm attacks is less than n seconds (k is a given small constant)
No
Yes
NoIn order to compare the LTL-model-checking-based approaches in [1, 3, 5] with our RASL-model-checking-based algorithm, we simulate and detect some telnet attacks by using MATLAB. We randomly produce 25 kinds of telnet attacks and repeat 80 times for every of these attacks. On average, less than 5 kinds of attacks are reported by the LTL-based simulator, whereas almost 100 percent of these attacks are found by the RASL-based simulator, as shown in Figure 6(a). The simulation results indicate that the model checking technique itself cannot make an IDS stronger, but this technique, when employing a stronger temporal logic, such as RASL, to describe attacks, can.Comparisons of average number of attacks found by different MC-based approaches (x: the number of kinds of simulation attacks and y: the different number of kinds of attacks found by the different simulators). (a) For telnet attacks. (b) For p-trace attacks.
(a)
(b)We simulate and detect some p-trace attacks by using MATLAB. We randomly produce 30 kinds of p-trace attacks, and repeat 100 times for each of these attacks. On average, less than 10 kinds of attacks are reported by the LTL-based simulator, whereas almost 100 percent of kinds of attacks are found by the RASL-based simulator, as shown in Figure6(b). The results indicate that the RASL-based algorithm enhances the detection power for p-trace attacks, compared with the LTL-based algorithm. Clearly, this is due to the stronger expressive power of RASL.Suppose that the standard time unit is a second; Figure7 illustrates a comparison between the ITL-model-checking-based approach in [2] and our RASL-model-checking-based algorithm. We randomly produce some attacks including real-time attacks and non-real-time attacks. Compared with the ITL-based simulator, the RASL-based simulator raises the average number of detected attacks by as high as 400%, where the average time distance (or time constraints) between two atomic actions in the same real-time attack is only five seconds. The average number will still be raised by 15% even in the worst case, that is, the time distance is more than three thousand seconds. These results indicate that the RASL-based algorithm further raises the power of detection for p-trace attacks, compared with the ITL-based algorithm, again, due to the stronger expressive power of RASL.Figure 7
A comparison of detection ability for p-trace attacks using different MC-based approaches (x: the average time distance between atomic attack actions and y: the average number of attacks found by ITL simulator/average number of attacks found by RASL simulator).In order to give a comparison of the detection ability for more types of attacks between the ITL-model-checking-based approach [2] and the RASL-model-checking-based one, we tried to conduct a Benchmark test on KDD CUP 99 [20]. We used a behavior version of a sample subset of this standard benchmark set [20] to evaluate our research in intrusion detection. Attacks fall into four main categories [20], that is, DOS, R2L, U2R, and Probe, including totally twenty-two types of attacks, as shown in Figures 8, 9, 10, and 11. In each of these four figures, the y-axis means the ratio between the number of attacks found by ITL-based simulator and the number of attacks found by RASL-based simulator, whereas the x-axis means different types of attacks.Figure 8
Comparison for DOS attacks.Figure 9
Comparison for U2R attacks.Figure 10
Comparison for R2L attacks.Figure 11
Comparison for Probe attacks.As shown in the figures, all of the ratios range between 0 and 1. For some types of attacks, such as perl and ftp write, et al. the ITL-based simulator finds equal number of attacks when the new simulator does. And for other types of attacks, such as back, Neptune, and smurf, et al., the ITL-based simulator almost does nothing, whereas the RASL-based one does more. This is due to the strong expressive power of RASL again.


## 8. Conclusions

This paper defined a new real-time interval temporal logic—RASL. Based on it, we presented a RASL model checking algorithm and its intrusion detection algorithm. This enables us to employee MC-based approaches for detecting real-time attacks. P-trace attacks especially are hard to be detected by the existing IDS [4] except the LTL-based algorithm [1, 3], the ITL-based algorithm [2], and the new RASL algorithm. The new algorithm has detected some real-time p-trace attacks in our simulation experiments. To the best of our knowledge, this is the only method to report this type of attacks. It is the benefit of using the new approach.



---

*Source: 621203-2013-03-30.xml*