A Temporal Logic-Based Model for Forensic Investigation in Networked System Security - Computer Network Security - page 325

A Temporal Logic-Based Model for Forensic
Investigation in Networked System Security

Slim Rekhis and Noureddine Boudriga

CN&S Research Lab., University of the 7th Of November at Carthage, Tunisia
[e-mail]
[e-mail]

Abstract. Research in computer and network forensic investigation has
recently addressed the development of procedural guidelines, technical
documents, and semi-automation tools. It has however omitted the need
of formal proof. This work provides a novel approach that formalizes and
automates the proof in digital forensic investigation. First, it brings out
a formal logic-based language, called S-TLA + , to enable reasoning on
systems with uncertainty, by adding forward hypotheses to fulfill poten-
tial lack of details. S-TLA + is suitable for the description of evidences,
as well as elementary scenarios fragments representing the investigators
knowledge. Secondly, the proposal provides an automated verification
tool, S-TLC, to prove the correctness of S-TLA + specifications. It checks
whether there are possible hacking scenarios that meet the available dig-
ital evidences, and explores additional evidences. To demonstrate its ef-
fectiveness, the formalized analysis is applied on a compromised host.

1 Introduction

The growth of the number of digital security incidents and the sophistication
of the intrusions techniques made it impossible to completely prevent attacks.
Therefore, it becomes necessary to react e ciently to security incidents. Com-
puter forensic investigation, defined as “preservation, identification, extraction,
documentation and interpretation of computer data” [1], enables achieving these
objectives while performing a post-incident examination: a) evidence collection;
b) attack scenarios and relating security weakness determination; and c) result
argumentation with methods and techniques that are well-tested and proved.
During the recent years, the literature has addressed two main themes: a)
contribution to the development of technical documents specific to the inves-
tigation of various operating systems and b) writing of procedural guidelines
for forensic investigation. It has omitted any need of formalization and proof au-
tomation in digital forensic investigation, reducing consequently the results accu-
racy, and analysis practicality. Formalization allows an explicit and unambiguous
representation of forensic investigator's knowledge and observations. The proof
automation makes the generated investigation deductions relevant even with a
huge amount of data. It lets investigators argue about complex scenarios without
a need for advanced skills, nor a priori knowledge about the incident causes.

V. Gorodetsky, I. Kotenko, and V. Skormin (Eds.): MMM-ACNS 2005, LNCS 3685, pp. 325-338, 2005.
c