Information Technology Reference
In-Depth Information
Formal digital forensic investigation has interested few works that differ ac-
cording to the techniques and methodologies they used. [2] used Colored Petri
Nets to model digital postmortems investigation as a time-line of events. It fo-
cused on determining the set of causes that enabled the security incident to suc-
cess, so that the appropriate countermeasures can be foreseen. Nevertheless, the
methodology does not model incident effects, and does not support hypotheses
formulation when details are missing. [3] presented an automated diagnosis sys-
tem that generates possible attacks sequences using a plan recognition technique,
simulates them on the victim model, and performs pattern matching recognition
between their side effects and log files entries. This technique assumes that attack
activity is logged, which is in contradiction with the fact that complex attack
scenarios may subvert logging daemon and alter logs before hackers leave the
system. [4] used an expert system with a decision tree to search through evi-
dences for potential violations of invariant relationship between digital objects.
The methodology is useful in reducing the amount of data to be analyzed. Nev-
ertheless, it roughly depends on the system time granularity and the degree of
preciseness that the system uses to record time on objects.
This paper extends the work of [5]. First, it brings out a new logic-based
language, entitled S-TLA
+
.
Using a temporal logic of security actions, it offers a
important enhancement of the formal specification language TLA
+
[6]. S-TLA
+
is founded on a logic formalism that let adding forward hypotheses whenever
there is lack of details (information may be corrupted by hackers) to understand
the system. Second, the proposal is completed with an automated verification
tool, called S-TLC, to prove the correctness of S-TLA
+
specifications. The tool
is based on the enhancement of the TLC model checker [6, 7]. It is fitted to the
automated diagnosis of digital security incidents.
Our contribution is straightforward. First, the proposed approach is com-
pletely independent from any computer security technology or incident. It al-
lows arguing about sophisticated hacking scenarios as it tolerates potential lack
of details. Second, S-TLA
+
takes advantage from the richness of the formal
specification language TLA
+
to support advanced description of scenarios and
evidences, namely using temporal modalities.
The remaining of this paper is organized as follows: First, the forensic investi-
gation model is defined in Section 2. Next, Section 3 defines the novel S-TLA logic
and emphasizes on the new concepts and modifications added to TLA. In Section
4, the formal specification language S-TLA
+
is defined and demonstrated how
it can be used within forensic investigation. Section 5 presents S-TLC, explains
how it represents states, and describes how hacking scenarios are inferred both
using forward and backward chaining. In Section 6, the proposal is exemplified
by a case study. Finally, the work is concluded in Section 7.
2
The Computer Forensic Investigation Model
Given a set of evidences collected further to the occurrence of a security inci-
dents, the proposal aims to first reconstruct to potential hacking scenarios where
