digital investigation 4S (2007) S82–S91

available at www.sciencedirect.com

journal homepage: www.elsevier.com/locate/diin

Analyzing multiple logs for forensic evidence5

Ali Reza Arasteh, Mourad Debbabi*, Assaad Sakha, Mohamed Saleh

Computer Security Laboratory, Concordia Institute for Information Systems Engineering, Concordia University,
Montreal, Quebec, Canada

abstract

Keywords: Information stored in logs of a computer system is of crucial importance to gather forensic
Forensic analysis evidence of investigated actions or attacks. Analysis of this information should be rigorous
Log analysis and credible, hence it lends itself to formal methods. We propose a model checking ap-
Formal methods proach to the formalization of the forensic analysis of logs. A set of logs is modeled as
Model checking a tree whose labels are events extracted from the logs. In order to provide a structure to
Logging systems these events, we express each event as a term of algebra. The signature of the algebra is
Log correlation carefully chosen to include all relevant information necessary to conduct the analysis.
Properties of the model, attack scenarios, and event sequences are expressed as formulas
of a logic having dynamic, linear, temporal, and modal characteristics. Moreover, we pro-
vide a tableau-based proof system for this logic upon which a model checking algorithm
can be developed. We use our model in a case study to demonstrate how events leading
to an SYN attack can be reconstructed from a number of system logs.
ª 2007 DFRWS. Published by Elsevier Ltd. All rights reserved.

1. Introduction and motivation the digital forensic science. In many cases, the forensic proce-
dures employed are constructed in an ad hoc manner that im-
Attacks on IT systems are increasing in number, and sophisti- pedes the effectiveness or the integrity of the investigation. In
cation at an alarming rate. These systems now range from this paper, we contribute with an automatic and formal ap-
servers to mobile devices and the damage from such attacks proach to the problem of analyzing logs with the purpose of
is estimated in billions of dollars. However, due to the border- gathering forensic evidence.
less nature of cyber attacks, many criminals/offenders have One of the most common sources of evidence that an inves-
been able to evade responsibility due to the lack of supporting tigator should analyze is logged events from the activities of
evidence to convict them. In this context, cyber forensics the system that is related to the incident in question. Indeed,
plays a major role by providing scientifically proven methods having the logs from all system events during the incident
to gather, process, interpret, and use digital evidence to bring will reduce the process of forensics analysis to event recon-
a conclusive description of cyber crime activities. The devel- struction. However, log analysis depends largely on the analy-
opment of forensics IT solutions for law enforcement has st’s skills and experience to effectively decipher complex log
been limited. Although outstanding results have been patterns and determine what information is pertinent and
achieved for forensically sound evidence gathering, little has useful to support the case at hand. Despite the paramount im-
been done on the automatic analysis of the acquired evidence. portance of this aspect, not much research effort has been ded-
Furthermore, limited efforts have been made into formalizing icated to the automation of forensic log analysis. The main

5
The research reported in this paper is the result of a fruitful collaboration with Bell Canada under the PROMPT Quebec research part-
nership program.
* Corresponding author.
E-mail addresses: [email protected] (A.R. Arasteh), [email protected] (M. Debbabi), [email protected]
(A. Sakha), [email protected] (M. Saleh).
1742-2876/$ – see front matter ª 2007 DFRWS. Published by Elsevier Ltd. All rights reserved.
doi:10.1016/j.diin.2007.06.013
 digital investigation 4S (2007) S82–S91 S83

intent of this paper is to introduce a formal and automatic log  Pre-/post-condition based approaches (Cuppens and Miege,
analysis technique. The advocated approach caters for: 2003; Ning et al., 2002; Templeton and Levitt, 2000) that
match the post-condition of an attack to the pre-conditions
 Modeling of log events and logical representation of proper- of another attack.
ties that should be satisfied by the traces of system events.  The multiple information sources based approaches (Morin
 Formal and automatic analysis of the logs looking for a spe- et al., 2002; Porras et al., 2002; Yegneswaran et al., 2004) that
cific pattern of events or verifying a particular forensic are concerned with distributed attack discovery.
hypothesis.
However, these approaches are mainly concerned with cor-
In spite of the few research results on formal and auto- relation, and intrusion detection, while formal log analysis and
matic analysis of forensic and digital evidence, there are hypothesis verification is of paramount importance to forensic
some important proposals that we detail hereafter. science. As an example, invariant properties of the system can-
Current research efforts on cyber forensic analysis can be not be modeled and analyzed through the above approaches.
categorized into baseline analysis, root cause analysis, com- The absence of a satisfactory and a general methodology for fo-
mon vulnerability analysis, timeline analysis, and semantic rensic log analysis has resulted in ad hoc analysis techniques
integrity check analysis. The baseline analysis, proposed in such as log analysis (Peikari and Chuvakin, 2004) and operating
Monroe and Bailey (2003), uses an automated tool that checks system-specific analysis (Kruse and Heiser, 2002).
for differences between a baseline of the safe state of the sys- In this paper, we propose a new approach for log analysis
tem and the state during the incident. The work presented in that is based on computational logic and formal automatic
Stephenson (2003) proposes an approach to post-incident root verification. We start by developing a model of logs based on
cause analysis of digital incidents through a separation of the traces of events. Each event is actually an abstract view of
information system into different security domains and mod- a piece of information stored in the log. The structure of an
eling the transactions between these domains. Common vul- event is carefully chosen to convey the necessary information
nerability analysis (Tenable Network Security, 2007) involves needed for the analysis. To this end, events are represented as
searching through a database of common vulnerabilities and terms of a multi-sorted term algebra whose operation
investigating the case according to the related past and known symbols are chosen such that they faithfully convey the infor-
vulnerabilities. The timeline analysis approach (Hosmer, 1998) mation stored in the actual events stored in the log. For
consists of analyzing logs, scheduling information, and mem- instance the term DeleteFile(F, U ) with operation DeleteFile :
ory to develop a timeline of the events that led to the incident. File  User/Bool represents the deletion of file F by a user
Finally, the semantic integrity checking approach (Stallard U. Using this approach, we can reason about log events irre-
and Levitt, 2003) uses a decision engine that is endowed spective of the specific syntax of the log, which is usually dif-
with a tree to detect semantic incongruities. The decision ferent for different systems. Each log in the system is thus
tree reflects pre-determined invariant relationships between modeled as a trace of terms. Moreover, in the presence of
redundant digital objects. several logs to which information is written concurrently,
Gladyshev and Patel (2004) proposed a formalization of dig- the whole logging system is modeled as a tree that represents
ital evidence and event reconstruction based on finite state possible different interleavings of events from the logs.
machines. In his work, the behavior of the system is modeled To express properties of the model, we resort to a temporal,
as a state machine and a recursive model checking procedure dynamic, modal and linear logic. This logic is an accommo-
is proposed to verify the admissibility of a forensic hypothesis. dated version of ADM logic that has been initially proposed
However, in the real world, modeling the behavior of a com- in Adi et al. (2003). The motivation behind this choice is that
plex system such as an operating system as a state machine ADM comes with many features and attributes that make it
diagram is burdensome and sometimes impossible to achieve very suitable for what we intend to achieve since it deals
because of complexity issues. Other research on formalized with properties of traces. The modified version that we pres-
forensic analysis include the formalization of event time bind- ent in this paper deals with properties of terms and trees.
ing in digital investigation (Gladyshev and Patel, 2005; Leig- Also, ADM is very compact in its syntax, elegant and formal
land and Krings, 2004), which proposes an approach to in its semantics and high in terms of expressiveness. Actually,
constructing formalized forensic procedures. Nevertheless, it is temporal (through the use of modal operators), dynamic
the science of digital forensics still lacks a formalized ap- (through the use of patterns as arguments in the modalities)
proach to log analysis. and linear (by allowing model modifications in the logic se-
As for log analysis and correlation, some research has been mantics). Besides, it comes with fixpoint operators à la modal
done on alert correlation, which can be classified into four cat- m-calculus, which allows for the specification of properties
egories (Xu, 2007): that are finite encodings of infinite logical formulas. All this
expressiveness is extremely useful in capturing forensic prop-
 Similarity based approaches (Cuppens, 2001; Julisch, 2003; erties, hypotheses and system invariants. Moreover, we pres-
Staniford et al., 2002; Valdes and Skinner, 2001), which group ent a tableau-based proof system that defines a compositional
the alerts according to the similarity between alert attributes. model checking algorithm. All these features provide a rigor-
 Predefined attack scenario based approaches (Debar and ous and provable logical support, which is a necessity for an
Wespi, 2001; Morin and Debar, 2003), which detect attacks investigation to be admitted in courts of law.
according to well-defined attack scenarios. However, they This paper is organized in five sections. In Section 2, we
cannot discover novel attack scenarios. present our approach to the formal modeling of logs. Section 3
S84 digital investigation 4S (2007) S82–S91

is devoted to the logic used to express properties of the model. terms. A substitution is generally extended to a homomor-
Section 4 contains an example of how logs can be modeled and phism in the following way:
their properties expressed in our framework. Section 5 pres-
qx : XS /TS ðS; XÞ is extended to
ents a case study dealing with an SYN attack. Finally, conclu- ~qx : TS ðS; XÞ/TS ðS; XÞ
sions and future work are discussed in Section 6. ~qx ðcÞ ¼ c where c is a constant
 
~qx ðf ðt1 ; t2 ; .; tn ÞÞ ¼ f ~qx ðt1 Þ; ~qx ðt2 Þ; .; ~qx ðtn Þ

2. Model for logs Usually we write qx for ~qx .

We view a log as a sequence of log entries, each entry con-
In this section, we describe our model for system logs which is sists of a certain term t of a term algebra T S . The signature S is
a tree of algebraic terms. First, we briefly recall concepts fro- chosen such that each event monitored by the logging system
m universal algebra (Wechler, 1992) then we present the can be represented as a term t˛TS . We define the log model L
model. as a finite sequence over TS , i.e., L˛TS . In other words, the log
A multi-sorted signature S is a pair CS; FD, where S is a set of model is a sequence that represents logged events in the sys-
sorts and F is a set of operator symbols. For each operator tem ordered temporally. Graphically, the log model is a trace
symbol f, the function arity : F/N maps f to a natural number whose edges are labeled by terms of TS . However, many sys-
called the arity of f. Moreover, for any operator symbol f ˛F of tems may have more than one log, where each log is dedicated
arity n, we have the functions domðf Þ˛Sn and codðf Þ˛S, where to a certain category of events. Moreover, we may be faced by
S0 ¼ Ø, S1 ¼ S, and Snþ1 ¼ S  Sn . For an operator symbol f, situations where it is necessary to inspect logs from different
where dom( f ) ¼ S1  S2 / Sn, and cod( f ) ¼ S, f is called an machines, e.g., in the case of a network. In order to model a log
operator of sort S and we write f : S1  S2  /  Sn /S. In the system consisting of more than one log, and in the presence of
case where arity( f ) ¼ 0, and cod( f ) ¼ S, f is called a constant concurrent actions in the logs, the model becomes a tree. To
symbol of sort S, the set of constants of sort S is written CS . illustrate this, assume we have a sequence of actions a$b in
Also, for each sort S, we define an infinite set XS of countable log L1 and another sequence c$d in log L2. Temporally, we as-
elements called variables of sort S, such that XS XCS ¼ Ø. For sume that a occurred first then c, then b and d occurred at
a certain signature S, we define the set TP ðS; XÞ of free terms the same time. The combined trace of the two logs will be
of sort S inductively as follows (the symbol ‘0’ is for logic im- a tree L, which is the following set of traces L ¼ {a, a$c, a$c$b,
plication): a$c$d, a$c$b$d, a$c$d$b}, i.e., we considered the two possible in-
terleavings of the concurrent events b and d. The same basic
ðXS WCS Þ4TS ðS; XÞ
idea is used to construct synchronization trees of process cal-
f : S1  S2  /  Sn /S0f ðt1 ; .; tn Þ˛TS ðS; XÞ culi. We define the interleaving of two logs L1 and L2 to be
where each ti is a term of sort Si L1 kL2 4ðTS1 WTS2 Þ which represents all possible interleavings
of concurrent events from both logs. Here, we assumed that
The set TP ðXÞ of free terms over the signature S is defined as
each log has its own signature. The definition can be easily
Ws˛S TP ðS; XÞ. The set of ground terms TP 4TP ðXÞ includes all
generalized in the case of a finite number of logs. Defined
terms that do not contain any variables.
this way, a log system of more than one log is graphically rep-
An algebra A of a signature S (called a S-algebra) is a pair
resented as a tree whose branches are labeled by terms of
CA; FA D. The S-algebra A assigns to each sort S in the signature
term algebras. Our model consists of this log tree along with
S a set AS called the carrier of sort S, where A ¼ WS˛S AS . Also
a mapping orig that maps terms to their respective logs. For
for each operator symbol f : S1  S2  /  Sn /S, A assigns a
instance, in the example above, we have orig(a) ¼ L1. For a se-
function fA : AS1  AS2  .  ASn /AS , FA is the set of all func-
quence s ˛ L, we define s^P, where P is a set of individual logs,
tions fA . A homomorphism is a function between S-algebras
to be the sequence obtained from s by removing any terms t,
that reserves their structure. If A and B are two S-algebras
such that origðtÞ;P. We overload the ^ operator by defining
having the same signature, h : A/B is a called a S-homomor-
L^P to be the set fs^Pjs˛Lg. In the example above, we have:
phism iff:
  L ^ L1 ¼ {a, a$b}, L ^ L2 ¼ {c, c$d}, and L ^ {L1, L2} ¼ L. We note
cf ˛F$h fA ða1 ; a2 ; .; an Þ ¼ fB ðhða1 Þ; hða2 Þ; .; hðan ÞÞ here that L^P is also a tree.
A S-algebra provides an interpretation for a certain signature,
where each sort is interpreted as a set and each operator
symbol as a function. The free term algebra T S ðXÞ associated
3. Logic for log properties
with a signature S is a special kind of S-algebra in which
In this section, we present a new logic for the specification of
each carrier set AS of the sort S and each function fT S ðXÞ : AS1 
properties of the log model. The logic is based on ideas from
AS2  /  ASn /AS are defined as:
the ADM logic (Adi et al., 2003), with some basic differences.
ct$t˛TS ðS; XÞ5t˛AS First, ADM is trace-based while the logic we present is tree-
based, therefore we can quantify existentially and universally
fT S ðXÞ ðt1 ; t2 ; .; tn Þ ¼ f ðt1 ; t2 ; .; tn Þ where ti ˛ASi
over traces. Moreover, this gives us the opportunity to express
The term algebra T S can be obtained from T S ðXÞ by removing branching-time properties. Second, we add a ‘‘sub-tree’’ oper-
any terms that contain variables. A substitution ator that will allow us to quantify with respect to individual
qx : XS /TS ðS; XÞ is a mapping from variables to terms of the logs, e.g., all sequences of the tree that contain events from
same sort. A ground substitution maps variables to ground logs L1 and L2 only. Third, the actions in ADM are atomic
 digital investigation 4S (2007) S82–S91 S85

symbols whereas the actions in our logic have a structure The first condition above means that r2 is obtained from r1
since they are terms of a term algebra. The choice of ADM in by replacing some of the terms of r1 by the dummy symbol ;,
the first place is motivated by the fact that is based on modal where q(;) ¼ ;, i.e., sequence variables of r1 and r2 are the
m-calculus with its known expressive power. Most impor- same. This condition is necessary to ensure that r1q and r2q
tantly, the properties we would like to express are over traces have the same length. Hence, in a tree model L, if r1q ˛ L, we
of the log tree model, ADM deals with traces and has all the ex- can replace r1q by r2q and still get a tree, which is written
pressive power we need for this task including some counting L0 ¼ L[r2q/r1q]. The second condition is necessary for the se-
properties (Adi et al., 2003). mantic interpretation function as will be explained in the se-
mantics section.
3.1. Syntax Intuitively, a log tree model L satisfies the formula
[r1 I r2]4 if for all sequences s ˛ L that matches r1, i.e.,
Before presenting the syntax of formulas, we present the con- r1q ¼ s, when s is modified to match r2 (by removing some of
cept of a sequence pattern r. A sequence pattern has the fol- its terms) then s0 ¼ r2q satisfies 4. The model L satisfies
lowing syntax: CCLDD4, where L is a set of logs, if L^L satisfies 4. The rest of
r T ¼ eja$rjxr $r aT ¼ tjQtS (1) the formulas have their usual meanings in modal m-calculus
(Cleaveland, 1990).
Here a represents a term in TS ðXÞ and has the form t or QtS.
Intuitively, a represents a term in the log tree model, where
this term is either t or a term containing tðQtSÞ. The term QtS is
defined as t or f(t1, t2,.,tn) such that dti $ti ¼ QtS. Here f ˛ S is 3.2. Semantics
any function symbol in the signature of the algebra. The se-
quence variable xr represents a sequence of terms of zero or A formula in the logic is interpreted over a log tree. Given a cer-
any finite length, the subscript r is added to avoid confusion tain log tree L, and an environment e that maps formulae vari-
L
with term variables x of the message algebra. The sets of se- ables to sequences in L, the semantic function E4Fe maps
quence variables and terms in r are written var(r) and trm(r), a formula 4 to a set of sequences S 4 L that satisfy this for-
respectively. Moreover, for any pattern r, the symbol rji repre- mula.
sents the variable or move at position i of r, where i ˛ {1,.,n}. L
EZFe ¼ eðZÞ
We define the substitution qr : varðrÞ/TS that maps vari- L
E:4Fe ¼ LyE4Fe
L

ables xr in a sequence pattern to sequences of terms, this is L L L

E41 ^42 Fe ¼ E41nFe XE42 Fe o
not to be confused with the substitution qx that maps variables L L0
E½r1 Ir2 4Fe ¼ s˛Ljcq$matchðs; r1 ; qÞ0s0 ˛E4Fe ; (3)
inside messages into terms of TS(X ).
where s0 ¼ r2 q and L0 ¼ L½r2 q=r1 q
We define the predicate match(s, r, qm, qr), which is true L
ECCLDD4Fe ¼ ðL^LÞXE4F
L
n e o
when a sequence s ¼ s1$s2.sn in the log tree matches a pattern L L
EnZ$4Fe ¼ W S4LjS4E4Fe½Z1S
r, e is the empty sequence:
matchðe; e; qm ; qr Þ ¼ true From the semantic equations above it can be seen that the
matchðs; e; qm ; qr Þ ¼ false if sse meaning of the recursive formula nZ$4 is taken to be the great-
L
matchðs; a$r; qm ; qr Þ ¼ ðs
 1 ¼ aqm Þ ^ matchðs2 .s
 n ; r; qm ; qr Þ est fixpoint of a function f : 2L /2L , where f ðSÞ ¼ E4Fe½Z1S . The
matchðs; xr $r; qm ; qr Þ ¼ dj  n$ xr qr ¼ s1 .sj  function f is defined over the lattice ð2 ; 4; W; XÞ, the syntactic
L
^ match sjþ1 .sn ; r; qm ; qr
condition on 4 (X appears under the scope of an even number
A substitution q : R/TS from patterns to sequences of terms, of negations) ensures that f(S ) is monotone (Cleaveland, 1990)
where q ¼ qm W qr, is defined as follows: and hence has a greatest fixpoint.
We use the following shorthand notations:
qðeÞ ¼ e
qða$rÞ ¼ qm ðaÞ$qðrÞ :ð:41 ^:42 Þh41 n42
qðxr $rÞ ¼ qr ðxr Þ$qðrÞ :41 n42 h41 042
:½r1 Ir2 :4hCr1 Ir2 D4
We will follow the usual notation for substitutions and write :nZ$:4½:Z=ZhmZ$4
rq for q(r). From the definitions of the predicate match and
L
the substitution q above, we notice that the condition for We also define nZ$Z to be tt, where EttFe ¼ L and mZ$Z to be
L
a match between a pattern and a sequence is the existence ff, where EffFe ¼ Ø. In the following, we prove some impor-
of one or more substitutions q, we can therefore write the tant results regarding the logic.
predicate as match(s, r, q).
The syntax of a formula f is expressed by the following Lemma 3.1.
grammar: L L
E4½j=ZFe ¼ E4Fe½Z1EjFLe 
4 T ¼ Zj:4j41 ^42 j½r1 Ir2 4jCCLDD4jnZ$4 (2)

We require the following two syntactic conditions:

Proof. The proof is done by structural induction over 4. Base
 In [r1 I r2]: ci$(r1ji ˛ var(r1) 5 r1ji ¼ r2ji) ^ (r1ji ˛ trm(r1) 5 case: 4 ¼ Z
r1ji ¼ r2ji n r2ji ¼ ;). L L
Ej=ZFe ¼ EjFe
 In nZ$4, any free Z in 4 appears under the scope of an even
L L L
number of negations. But: EZFe ¼ eðZÞ, so Ej=ZFe ¼ EZFe½Z1EjFLe  .
S86 digital investigation 4S (2007) S82–S91

We demonstrate two cases and the other cases can be eas- We also used the fact that for any set of sequences S,
ily proved: S X (L\S ) ¼ Ø. It is worth noting here that the semantics of
Cr1 I r2D4 is consistent with the definition of the modality CD
from modal m-calculus.
Case 1. 4 ¼ nZ$40 and X is free in 4
n  o
L  L 3.3. Tableau-based proof system
E4½j=XFe ¼ W S4LS4E40 ½j=XFe½Z1S

By induction hypothesis: Before we present the rules of the tableau, we define the im-
n  o mediate subformula relation (Cleaveland, 1990) 3I as:
L  L
E4½j=XFe ¼ W S4LS4E40 Fe½Z1S ½X1EjFLe½Z1S 
43I :4 43I ½r1 Ir2 4
Since j does not contain Z as free variable, which can be as- 4i 3I 41 ^42 i˛f1; 2g 43I nZ$4
sured by renaming of the bound variable Z, we have: We define 3 to be the transitive closure of 3I and 6 to be
n o
L L
E4½j=XFe ¼ W S4LjS4E40 ½j=XFe½Z1S½X1EjFLe  its transitive and reflexive closure. A tableau-based proof
system starts from the formula to be proved as the root of a
L L proof tree and proceeds in a top down fashion. In every rule
E4½j=XFe ¼ E4Fe½X1EjFLe 
of the tableau, the conclusion is above the premises. Each
conclusion of a certain rule represents a node in the proof
Case 2. 4 ¼ [r1 I r2]40 tree, whereas the premises represent the children to this
n o node. In our case, the proof system proves sequents of the
L L0
E4½j=ZFe ¼ s˛Ljcq$match ðs; r1 ; qÞ0s0 ˛E40 ½j=ZFe form H, bw s ˛ 4, which means that under a set H of hypoth-
eses and the symbol b, then the sequence s satisfies the prop-
By induction hypothesis:
erty 4. The set H contains elements of the form s: nZ$4 and is
n o
L L0
E4½j=ZFe ¼ s˛Ljcq$matchðs; r1 ; qÞ0s0 ˛E40 Fe½Z1EjFLe  needed for recursive formulas. Roughly, the use of H is to say
that in order to prove that a sequence s satisfies a recursive
L L formula 4rec, we must prove the following: Under the hypoth-
E4½j=ZFe ¼ E4Fe½Z1EjFLe  ,
esis that s satisfies 4rec, then s also satisfies the unfolding of
4rec. We also define the set H l nZ$4 ¼ {s ˛ Ljs:nZ$4 ˛ H}. The
use of H, and b will be apparent after we state the rules of
L L
As a result, we have EvZ$4Fe ¼ E4½vZ$4=ZFe . This follows the proof system:
L L
from the o fact that EvZ$4Fe ¼ E4Fe½Z1T , where T ¼ WfS4LjS4 H; bws˛:4
L L
E4Fe½Z1S ¼ EvZ$4Fe . R:
H; :bws˛4
We can now prove that the semantics of the expression
mZ$4 defined earlier as :nZ$:4[:Z/Z] is the least fixpoint of H; b; ws˛41 ^42
L R^ b1  b2 ¼ b
the function f ðSÞ ¼ E4Fe½Z1S . H; b1 ws˛41 H; b2 ws˛42
n o
L L
E:nZ$:4½:Z=ZFe ¼ LyW S4LjS4E:4½:Z=ZFe½Z1S H; bws˛nZ$4
n  o Rn s : nZ$4;=H
 L H0 Wfs : nZ$4g; bws˛4½nZ$4=Z
¼ LyW S4LS4LyE4Fe½Z1E:ZFLe½Z1S 
n  o
 L
¼ LyW S4LS4LyE4Fe½Z1LyS H; bws˛½r1 Ir2 4
R½  condition
x1 x2 /xn
For any set of sequences S 4 L, let Sc ¼ L\S. By De Morgan laws,
for any two sets A and B: (A X B)c ¼ Ac W Bc, (A W B)c ¼ Ac X Bc, H; bws˛CCLDD4
A 4 B 0 Bc 4 Ac. RCCDD
H; bws^L˛4
  c c
L L
E:nZ$:4½:Z=ZFe ¼ WfLySc 4LjS4 E4Fe½Z1Sc  g where
 c
L
¼ WfLySc 4LjE4Fe½Z1Sc  4Sc g H0 ¼ Hyfs0 : GjnZ$43Gg
n oc
L
¼ X LySc 4LjE4Fe½Z1Sc  4Sc xi ¼ H; bi wr2 qi ˛4
n o
L
¼ X Sc 4LjE4Fe½Z1Sc  4Sc 8
< cqi $matchðs; r1 ; qi Þ
Moreover, we investigate the semantics of the expression condition ¼ ^ b1  b2  /  bn ¼ b
:
Cr1 I r2D4 as defined above: ^ n>0

L
ECr1 Ir2 D4Fe ¼ E:½r
L The first rule concerns negation of formulas where b ˛ {e, :}
n 1 Ir2 :4Fe o
¼ s˛Lj:cq$matchðs; r1 ; qÞ0s 0 L0
˛LyE4Fe serves as a ‘‘memory’’ to remember negations, in this case
n o e4 ¼ 4. We define ee ¼ e, e: ¼ :e ¼ :, and :: ¼ e. Moreover, we
L0
¼ s˛Lj:cq$matchðs; r1 ; qÞ0:s0 ˛E4Fe
n  o define e  e ¼ e, e  : ¼ :  e ¼ :, and :  : ¼ :. The second
L0 ;q
¼ s˛Lj:cq$: matchðs; r1 ; qÞ^s0 ˛E4Fe rule says that in order to prove the conjunction, we have to
n  o
L0 ;q prove both conjuncts. The third rule concerns proving a recur-
¼ s˛Ljdq0 $ matchðs; r1 ; qÞ^s0 ˛E4Fe
sive formulas, where the construction of the set H, via H0 , en-
In the derivation above we used the sequent j 0 :4 w sures that the validity of the sequent H, bw s ˛ nZ$4 is
:(j ^ 4), which can be easily proved by propositional calculus. determined only by subformulas of 4 (Cleaveland, 1990). The
 digital investigation 4S (2007) S82–S91 S87

L;H
fourth rule takes care of formulas matching sequences to pat- Theorem 3.3. Completeness. If for a sequence s ˛ L, s˛E4Fe , then
terns. Finally, the fifth rule deals with formulas dealing with the sequent H, bw s ˛ 4 has a successful tableau.The proof relies
subtrees of the model tree L. Starting from the formula to be on showing that we cannot have two successful tableaux for
proved at the root of the proof tree, the tree grows downwards the sequents H, bw s ˛ 4 and H, bw s ˛ :4.
until we hit a node where the tree cannot be extended any-
more, i.e., a leaf node. A formula is proved if it has a successful
tableau, where a successful tableau is one whose all leaves are
successful. A successful leaf meets one of the following
conditions:
4. Example of logs and properties

L In this section we give an example of constructing a model of

 H, e w s ˛ Z and s˛EZFe .
L actual log systems and expressing some general properties.
 H, : w s ˛ Z and s;EZFe .
The methodology we apply here can be easily adapted to
 H, e w s ˛ nZ.4 and s:nZ.4 ˛ H.
various systems of logs. We begin by listing the signature of
 H, e w s ˛ [r1 I r2]4 and {s ˛ Ljdq$match(s, r1, q)} ¼ Ø.
our algebra and the notation used for constants and variables.
The sorts of the signature are given in Table 1, whereas the op-
In the next section, we list the most important properties of
erations are given in Sections 4.1 and 4.2. These operations are
the tableau-based proof system.
categorized based on the context to which they are related. In
most cases, the notation we use for the names of operations
and sorts reveals their intended meaning and in case of ambi-
3.4. Properties of tableau system guity we will provide explanation. So, in order to model a sin-
gle log, a parser can be developed that will parse the log and
We would like to prove three main properties, namely the fi- construct its model as a sequence of algebraic terms, where
niteness of the tableau for finite models, the soundness, and each term corresponds to a certain log event. The model for
the completeness. Soundness and completeness are proved a system of several logs will be a tree whose labels are terms
with respect to a relativized semantics that takes into account as explained in Section 2. Once the model is constructed, the
the set H of hypotheses. The new semantics is the same as the desired properties can be expressed as formulas of the logic
one provided above for all formulas except for recursive for- we presented. The model and logic can then be submitted to
mulas where is it defined as: a model checker that will check if the model satisfies the for-
  mula. The presence of a tableau-based proof system for the
L;H L;H
EnZ$4Fe ¼ nE4Fe½Z1SWS0  WS0 where S0 ¼ HlnZ$4 logic serves as a starting point for the implementation of
a model checking algorithm. Such a framework can be used
In the equation, the greatest fixpoint operator is applied
L;q in event reconstruction based on expressing scenarios and hy-
to a function f ðSÞ ¼ E4Fe½Z1S whose argument is S W S0 .
potheses as properties, and then verify their validity, this will
Since the function is monotone over a complete lattice, as
be explained in Table 1.
mentioned earlier, then the existence of a greatest fixpoint
is guaranteed. We now list some results regarding the proof
system. The detailed proofs are not provided due to space
limitation.
Table 1 – Sorts of the algebra

Theorem 3.1. Finiteness. For any sequent H, bw s ˛ 4 there exists Sorts Constants Variables
a finite number of finite tableaux.The idea of the proof is that for File f1, f2, ., fn fx, fy, fz, .
any formula at the root of the proof tree we begin applying the User u1, u2, ., un ux, uy, uz, .
rules R:, R^, R[], RCCDD , and Rn. The application of the first four Object o1, o2, ., on ox, oy, oz, .
rules results in shorter formulas, while the application of objectedID oID1, oID2, ., oIDn oIDx, oIDy, oIDz, .
Process p1, p2, ., pn px, py, pz, .
the Rn rule results in larger hypothesis sets H. The proof shows
Service s1, s2, ., sn sx, sy, sz, .
that shortening a formula and increasing the size of H cannot
service_type st1, st2, ., stn stx, sty, stz, .
continue infinitely. Hence no path in the tree will have infinite registry_key r1, r2, ., rn rx, ry, rz, .
length. Branching happens in the proof tree whenever we Operation opREAD, opWRITE opx, opy, opz, .
have an expression of the form 41 ^ 42 or [r1 I r2]4. Finite Executable e1, e2, ., en ex, ey, ez, .
branching is guaranteed in the first case by the finite length Privilege pvADMIN pvx, pvy, pvz, .
of any expression and in the second case by the finiteness of Access acN Allowed ; acALLOWED acx, acy, acz, .
Port ptPORT NO ptx, pty, ptz, .
the model.
Protocol procUDP, procTCP, ., un procx, procy, procz, .
ipAddress ip1, ip2, ., ipn ipx, ipy, ipz, .
dateTime dt1, dt2, ., dtn dtx, dty, dtz, .
Theorem 3.2. Soundness. For any sequent H, bws ˛ 4 with a suc- logonType ltINTERACTIVE, ltREMOTE, . ltx, lty, ltz, .
L;H
cessful tableau, s˛E4Fe logonID lID1, lID2, ., lID3 lIDx, lIDy, lIDz, .
Size/type s_tPOD . s_tx, s_ty, s_tz, .
The idea behind the proof is to show that all the successful args a1, a2, ., an ax, ay, az, .
error er1, er2, ., ern erx, ery, erz, .
leaves described above are valid and that the application of
bool Tr, Fl bx, by, bZ , .
the rules of the tableau reserves semantic validity.
S88 digital investigation 4S (2007) S82–S91

4.1. Machine events logs 4.2.1. Intrusion detection system

Here we use SNORT (Snort, 2007) as an example for our mod-
In this section, we discuss logs of events related to a single eling. The SID shown below is the attack ID used by SNORT to
machine. This machine could be a stand alone system or detect a known signature.
a node in a network, however, the events we consider here Attack : dateTime  SID  sourceIP  destIP/bool
are internal events related to a specific machine. It is not our
intention to give an exhaustive list of all possible events but
to demonstrate the use of our model using various categories
4.2.2. Web server
of events. Each type of log events is modeled by an operation
of the algebra as will be demonstrated below.
GetError : dateTime  error  ipAddress/bool
PostError : dateTime  error/bool
4.1.1. Process related actions
Get : dateTime  args  ipAddress/bool
These are the events related to the creation and destruction of Post : dateTime  args  ipAddress/bool
a process. UUCP : dateTime  ipAddress/bool
ProcessBegin : process  user  caller  privilege Here args is the sort of arguments for the Post and Get
executable/bool
actions.
ProcessExit : process  user/bool

For instance, the term ProcessExit( px, ux) models an actual log 4.3. Properties and scenarios
event in which any user (ux) terminated any process ( px), since
ux and px are variables. On the other hand, the term ProcessExit An important use of the logic is the ability to express an attack
( px, u1) models an actual log event in which a certain user (u1) or a certain scenario of events using a pattern based on the
terminated any process ( px). Table 1 presents our notation for general characterizations of this attack or scenario. In other
variables and constants. words, an investigator can express the attack or the events
he is looking for as a pattern in a logic formula using the syn-
4.1.2. Object related actions tax of the logic described above. Then, using a model checker,
In a Windows system, an object is either a file or a registry key. he can search the log model for such an attack or scenario of
The events which are related to objects are opening, modify- events in order to reconstruct the sequence of events that lead
ing and closing the objects. These events are modeled as to the incidence under investigation. To further illustrate how
actions as follows: this can be used, we have defined a general attack scenario
ObjectOpen : object  process  processName  type which is divided into four phases. Under each phase we
logonID/bool have grouped the possible events that an investigator would
ObjectClose : object/bool want to search for. The general attack scenario is as follows:
ObjectOperation : object  operation/bool
Intrusion/Compromise/Misuse/Withdrawal

4.1.3. User actions where each of Intrusion, Compromise, Misuse and Withdrawal is
These are actions related to creation, deletion, or modifica- a certain sequence of events. The Intrusion sequence consists
tions to user accounts and their rights as well as logons and of the events that are captured during the time the attacker
logoffs. breached the system using different techniques such as buffer
overflow, malicious codes, etc. Events in this category can be
Logon : user  userID  group  domain  process
extracted from the logs of an intrusion detection system.
logonType/bool
Logoff : username/bool Some patterns can be recognized as signs of intrusions such
as when a service executing with administrative privileges
4.1.4. Miscellaneous starts a command shell can allude to a buffer overflow attack.
Events that are not specific to any category are mentioned This pattern is demonstrated below, where we use e as a short-
here. hand for replacing single terms with ; and leaving sequence
variables xi as they are, to be consistent with syntax rules, also
ScheduleTask : user  process  caller  file
we use h for syntactic equality:
dateTime/bool
 
InstallService : service  file  service type Cx1 $ProcessBegin px ; ux ; py ; pvADMIN ; ex $x2 $ProcessBegin
username/bool  
UninstallService : service  user  dateTime/bool  pz ; uy ; px ; pvz ; e1 IeDtt;
DeactAntiVirus : user  dateTime/bool where e1 hcmd$exe
DeactFirewall : user  dateTime/bool
OpenConnection : process  port  protocol  user In the expression above the process px started with adminis-
access  dateTime/bool trative privileges and then it called pz which is the command
ClearLogs : user  dateTime/bool
shell.
The Compromise sequence consists of events pertaining to
4.2. Network events logs the preparation for malicious activity. During this phase the
attacker is setting up what is needed to carry out the intended
In this section we consider logs that monitor network events, attack. In addition, the attacker tries to provide himself with
i.e., related to more than one machine. convenient settings to return to the system at will. These
 digital investigation 4S (2007) S82–S91 S89

include but are not limited to: Creating a user, changing group
or password, installing or uninstalling a service, deactivating 5. Case study
antivirus and firewall software, changing important files or
registries, etc. These events can be constructed in different se- To better comprehend the power of our approach, we will
quences, one sequence can be: consider the following case: in an office environment using
Windows-based machines, there are several hosts connected
 
Cx1 $DeactFirewallðux ; dtx Þ$x2 $DeactAnitvirus ux ; dty $x3 IeDtt to a database server. An intrusion detection system is setup
as a security measure for the server. The server can be accessed
In the expression above the same user (ux) deactivated the
from outside the company so that the employees can connect
firewall followed by a deactivation of the antivirus, which is
to the server from client offices. Fig. 1 depicts the scenario.
suspicious. Of course, it is possible to elaborate more complex
The network administrator discovers that there was a de-
pattern but we are just using expressions for demonstrative
nial of service attack on the server. The intrusion detection
purposes.
system (IDS) SNORT determines an SYN attack which caused
The Misuse sequence represents the phase during which
the server to halt. An investigator is called upon to investigate
the attacker uses the compromised system for his own
this incident.
malicious purposes. The events considered for this phase
The investigator gathers the server network logs and starts
are: local or remote login using the created accounts in the pre-
searching for possible clues. Generally, when analyzing logs,
vious phases, opening a connection to the system, etc. As an
an investigator will either scan through the logs manually
example, consider the following property of a log sequence:
  using a simple editor which may provide some filtering capa-
Cx1 $OpenConnection px ; ptx ; procx ; ux ; acN ALLOWED ; dtx $x2 IeDtt bilities, or create a script to serve his purpose. Using our meth-
In the expression above, a user tried to open a connection that odology, the investigator only defines a pattern for a trace he
was refused, maybe because the user does not have the re- wants to look for, and since all logs are combined in a single
quired privilege. A repeated pattern like this indicates suspi- model, he does not need to consider logs separately. Moreover,
cious behavior of this particular user. if the investigator wishes to focus on a single log or a number of
The Withdrawal sequence represents the phase during logs, he can use the CCDD operator in the logic to do the job. In our
which the attacker tries to cover his tracks cleaning the sys- particular case, let us suppose the system administrator has
tem from his malicious activities. The events may be: deleting reported an SYN attack which is detected by SNORT and logged
files, uninstalling a service, clearing the log files, etc. An exam- with SID ¼ 1:526 (1). To locate the occurrence of this attack the
ple for how a withdrawal may be expressed: administrator uses the following trace from the SNORT logs:
 
Cx1 $UnistallServiceðsx ; ux ; dtx Þ$x2 $ClearLogs ux ; dty $x3 IeDtt CCSNORTDDCx1 $Attackðdtx ; sID1 ; sIPx ; dIPx Þ$x2IeDtt;
So far we have shown how an attack scenario can be where sID1 ¼ 1 : 526
expressed using our proposed approach. To further elaborate Once the investigator finds the event that logged the attack,
on the usefulness of this approach we demonstrate two types he examines it and realizes that this IP is within the same net-
of properties: work of the company. Knowing the date and time of the first
occurrence of the attack, the investigator looks for connec-
(A) Suspicious facts and invariant properties of a system tions opened on the same date and time from that host to
Suspicious facts are events that, when triggered, may be indi- the server. Until now, the events have been mostly gathered
cations of an attack; such as, a trusted executable being exe- from the IDS logs. The advantage and practicality of our model
cuted by an untrusted object. Invariant properties are
conditions that should be always satisfied. For example, for
every logon there should be a logoff:

 
nX$Cx1 $logon ux ; uIDx ; gx ; dx ; px ; ltx $x2 IeDttnCx1 $logoff
 
 ðuIDx Þ$x2 IeDtt0Cx1 $logon ux ; uIDx ; gx ; dx ; px ; ltx $x2 $logoff
 ðux Þ$x3 Ix1 $x2 $x3 DX

(B) Hypothesis properties

During the investigation, the investigator should be able
to verify the admissability of a claim, a hypothesis or a
speculation by expressing it in the form of a property and
submitting the logic expression to a model checker. An exam-
ple is the assumption that a file, when executed, will deacti-
vate the firewall and install a service which will be used as a
backdoor:

Cx1 $ProcessBeginðpx ; ux ; py ; pvx ; ex Þ$x2 $DeactFirewall

 
 ðux ; dtx Þ$x3 $InstallService sx ; fx ; stx ; ux ; dty $x4 IeDtt Fig. 1 – Case scenario.
S90 digital investigation 4S (2007) S82–S91

which correlates all logs into a tree are shown here since the registry key (objectOperation(o1, opSET)) and the username of the
Windows system, application, and security logs are correlated attacker, which may turn out to be different from the user mal
along with the network logs. The logs being correlated into the mentioned earlier. Such a situation is depicted by the follow-
same tree, we can define the patterns of traces that we are ing traces where, in terms, only the relevant arguments are
looking for using a logic formula and the model checker will listed:
search for them through the tree. However, to improve effi-
ciency, we can specify which log we want to examine thus re-
ducing the scope of our search. This can be done by adding
ILogSourceJ right before the corresponding pattern or trace.
LogSource in this case being SNORT (like in the pattern above),
SEC (security log), SYS (system log), or APP (application log). It
is possible to specify more then one log, e.g., ISYS, SECJ, or all
logs excluding one specific log, e.g., CCLySNORTDD.
Getting back to our case, the event reflecting opening a
connection can be found using:
CCSEC; SYS; APPDD Cx1 $OpenConnection
 
 px ; ptx ; procTCP ; uIDx ; ip1 acx ; dt1 $x2 IeDtt

where ip1 is the server’s IP address and dt1 is the time, these
two values can be obtained from SNORT logs as explained
above. Looking at the process that opened the connection
(the variable px), the investigator finds out that px is a certain
process p1. The investigator now wants to know information
about the launching of this process:
 
CCSECDD Cx1 $ProcessBegin p1 ; ux ; cpx ; pvx ; ex $x2 IeDtt

Assume the caller of p1, i.e., cpx, is p2. Using the same
formula as the one above but replacing p1 with p2 in the term
ProcessBegin(.), the investigator can find out the name and
executable file of p2. It turns out to be bo2k.exe, which is
the executable file of backOrifice2000; a backdoor. The next
step is to track down sessions in which the back door has
been executed which can be determined by the following:
  The figure above shows two traces, where we assumed the
CCSECDD Cx1 $Logon ux ; uIDx ; gx ; dx ; px ; ltx $x2 $ProcessBegin
    event a appeared concurrently with attack, hence the exis-
 px ; ux ; cpx ; pvx $e1 $x3 $Logoff ux IeD:Cx4 $ProcessBegin
tence of two branches. The idea we would like to express
 ðpy ; ux ; cpx ; pvx $e1 Þ$x5 $;$x6 IeDtt
here is that although the SYN attack may be coming from
where e1 hBo2k$exe the machine of the user uuser, a careful forensic analysis using
The formula above looks for all sessions (a session is our logic reveals that the registry key was modified by the user
bounded by a logon and a logoff) in which the malicious exe- uTechSupport, which is the real responsible.
cutable e1 is launched. Suppose in all of these sessions, at each
logon of a certain user mal to the system, the back door pro-
gram is executed, the investigator suspects that there is an en-
6. Conclusion and future research
try in one of the start-up registry keys for Bo2k.exe. The
following formula looks for the first session during which
In this paper we proposed a model checking approach to the
the run registry key has been modified before the first execu-
problem of formal analysis of logs. We model the log as
tion of the back door program.
a tree labeled by terms from a term algebra that represents
the different actions logged by the logging system. The proper-
  ties of such a log are expressed through the use of a logic that
CCSECDDCx1 $Logon ux ; uIDx ; gx ; dx ; px ; ltx $x2 $
  has temporal, modal, dynamic and computational character-
ProcessBegin px ; ux ; cpx ; pvx $e1 $x3 $Logoff ðux ÞIeD
istics. Moreover, the logic is provided by a sound and complete
ð:Cx4 $ProcessBeginðpy ; ux ; cpx ; pvx $e1 Þ$x5 $;$x6 IeDtt
tableau-based proof system that can be the basis for verifica-
^Cx6 $logonðuy ; uIDy ; gy ; dy ; py ; lty Þ$x7 $objectOpen
    tion algorithms. An example was given in which we presented
o1 ; pz ; pnz ; tpz ; lIDz $x8 $objectOperation o1 ; opSET $x9 $logoff ideas about properties of logs such as attack traces and invari-
ðuy Þ$x10 $;$x11 Ie > ttÞ ant properties. We also demonstrated how our system can be
where o1 hRUN REG used to reconstruct the sequence of events leading to SYN
attack. A future research direction may be the development
From this formula, the investigator will be able to know the of an efficient model checking algorithm based on our proof
session during which the malicious attacker has changed the system.
 digital investigation 4S (2007) S82–S91 S91

references Snort – sourcefire Inc., <http://www.snort.org> [Visited on May

22, 2007].
Tenable Network Security, <http://www.nessus.org/> [Visited on
May 22, 2007].
Adi K, Debbabi M, Mejri M. A new logic for electronic
Templeton S, Levitt K. A requires/provides model for computer
commerce protocols. Int J Theor Comput Sci, TCS 2003;
attacks. In: Proceedings of new security paradigms workshop,
291(3):223–83.
September 2000.
Cleaveland R. Tableau-based model checking in the propositional
Valdes A, Skinner K. Probabilistic alert correlation. In:
Mu-calculus. Acta Inform 1990;27(8):725–48.
Proceedings of the fourth international symposium on recent
Cuppens F. Managing alerts in a multi-intrusion detection
advances in intrusion detection (RAID 2001); 2001.
environment. In: Proceedings of the 17th annual computer
Wechler W. Universal algebra for computer scientists. Springer;
security applications conference, December 2001.
1992.
Cuppens F, Miege A. Alert correlation in a cooperative intrusion
Xu D. Alert correlation through triggering events and common
detection framework. In: Proceedings of the 2002 IEEE
resources, <http://citeseer.ist.psu.edu/742919.html> [Visited
symposium on security and privacy, May 2003.
on May 22, 2007].
Debar H, Wespi A. Aggregation and correlation of intrusion-
Yegneswaran V, Barford P, Jha S. Global intrusion detection in the
detection alerts. In: Recent advances in intrusion detection.
domino overlay system. In: Proceedings of the 11th annual
LNCS 2212; 2001.
network and distributed system security symposium
Gladyshev P, Patel A. Finite state machine approach to digital
(NDSS’04), Feburary 2004.
event reconstruction. Digit Investig J 2004;1(2).
Gladyshev P, Patel A. Formalising event time bounding in digital
Ali Reza Arasteh is a master student in the Department of Com-
investigations. Digit Investig J 2005;4(2).
puter Science at Concordia University. He holds B.Sc. degree
Hosmer C. Time lining computer evidence. Available from:
from Amirkabir University, Tehran, Iran. His main research inter-
<http://www.wetstonetech.com/f/timelining.pdf>; 1998
ests are forensics memory analysis, log analysis and intrusion de-
[Visited on May 22, 2007].
tection systems.
Julisch K. Clustering intrusion detection alarms to support root
cause analysis. ACM Trans Inform Syst Secur Nov 2003;6(4):
443–71. Mourad Debbabi is a Full Professor and the Associate Director of
Kruse W, Heiser J. Computer forensics: incident response essentials. the Concordia Institute for Information Systems Engineering at
Boston, MA: Addison-Wesley; 2002 [Visited on May 22, 2007]. Concordia University. He is also a Concordia Research Chair Tier
Leigland R, Krings AW. A formalization of digital forensics. Digit I in Information Systems Security. He holds Ph.D. and M.Sc. de-
Investig J 2004;3(2). grees in computer science from Paris-XI Orsay, University, France.
Monroe K, Bailey D. System base-lining: a forensic perspective. He published several research papers in international journals
Available from: <http://ftimes.sourceforge.net/Files/Papers/ and conferences on computer security, cyber forensics, formal
baselining.pdf>; 2003 [Visited on May 22, 2007]. semantics, mobile and embedded platforms, Java technology
Morin B, Debar H. Correlation of intrusion symptoms: an security and acceleration, cryptographic protocol specification,
application of chronicles. In Proceedings of the sixth design and analysis, malicious code detection, programming
international conference on recent advances in intrusion languages, type theory and specification and verification of
detection (RAID’03), September 2003. safety-critical systems. In the past, he served as Senior Scientist
Morin B, Me L, Debar H, Ducasse M. M2D2: a formal data model for at the Panasonic Information and Network Technologies Labora-
IDS alert correlation. In: Proceedings of the fifth international tory, Princeton, New Jersey, USA; Associate Professor at the
symposium on recent advances in intrusion detection (RAID Computer Science Department of Laval University, Quebec,
2002), 2002. Canada; Senior Scientist at General Electric Corporate Research
Ning P, Cui Y, Reeves DS. Constructing attack scenarios through Center, New York, USA; Research Associate at the Computer
correlation of intrusion alerts. In: Proceedings of the nineth Science Department of Stanford University, California, USA; and
ACM conference on computer and communications security, Permanent Researcher at the Bull Corporate Research Center,
Washington, DC, November 2002. p. 245–54. Paris, France.
Peikari C, Chuvakin A. Security warrior. O’Reilly; 2004.
Porras P, Fong M, Valdes A. A mission-impact-based approach to Assaad Sakha is a M.Sc. student at Concordia Institute of Informa-
INFOSEC alarm correlation. In: Proceedings of the fifth tion System Engineering, Concordia University working in the
international symposium on recent advances in intrusion field of Digital Forensics. The main area of his research is forensic
detection (RAID 2002); 2002. log analysis. He obtained his B.Sc. in Computer Information Sys-
Stallard T, Levitt K. Automated analysis for digital forensic tems at Notre Dame University, Lebanon. In addition he is a mem-
science: semantic integrity checking. In: 19th annual ber of the Information System Audit and Control Association
computer security applications conference, Las Vegas, NV, (ISACA).
USA, December 2003.
Staniford S, Hoagland J, McAlerney J. Practical automated Mohamed Saleh is a Ph.D. student at Concordia University work-
detection of stealthy portscans. J Comput Secur December ing in IT security. His main research interest is in the use of formal
2002;10(1/2):105–36. methods in the specification and verification of security protocols.
Stephenson P. Modeling of post-incident root cause analysis. Int He has also conducted some research work in application secu-
J Digit Evid 2003;2(2). rity, namely using Java.