[attachment=5536]

---

This article is presented by:
xxxxSlim Rekhis and Noureddine Boudriga
Communication Networks and Security Research Lab. University of the 7th November at Carthage, Tunisia.xxxxxxxxxx

Formal Digital Investigation of Anti-forensic Attacks

ABSTRACT
One of the major interest perceived by research in digital forensic investigation is the development of theoretical and scientifically proven methods of incident analysis. However, two main problems, which remain unsolved by the literature, could lead the formal incident analysis to be inconclusive. The former is related to the absence of techniques to cope with anti-forensic attacks and reconstruction of scenarios when evidences are compromised by these attacks. The latter is related to lack of theoretical techniques, usable during the system preparation (a phase which precedes the occurrence of an incident) to assess whether the evidence to be generated would be sufficient to prove relevant events that occurred on the compromised system in the presence of anti-forensic attacks. The aim of this research is to develop a theoretical technique of digital investigation which copes with anti-forensic attacks. After developing a formal logic-based model which allows to describe complex investigated systems and generated evidences under different levels of abstractions, we extend the concept of Visibility to characterize situations where anti-forensic attacks would be provable and traces regarding actions hidden by these attacks would become identified. A methodology showing the use of Visibility properties during investigation of anti-forensic attacks is described, and a case study, which exemplifies the proposal, is provided.
INTRODUCTION
As security attacks are continuously growing in sophistication, severity, and speed of compromise, research in information security has taken interest over the past few years to digital forensic investigation. The latter aims to conduct a post-incident analysis on compromised systems and make inquiries about past events. To do so, digital information stored, generated, processed, or transmitted by networking systems are used as a source of evidence. The evidences are therefore analyzed to reconstruct information about past events which happened during the incident. Many problems could lead a security incident to remain unsolved, allowing attackers to evade responsibility due to lack of evidences to convict them. A first predominant problem is related to anti-forensic attacks which may happen during the incident to alter traces regarding occurred events. Once an attacker has succeeded in compromising a system, it executes an anti-forensic attack to reduce the quantity and quality of evidential data available after the incident. To do so, it tries to alter the evidence already generated by the deployed security solutions in order to mislead investigation, evade detection, and prevent the accurate reconstruction of provable attack scenarios. Another important problem, which makes digital investigation inconclusive, is related to preparation. While security administrator are motivated by deploying a large set of security mechanisms which support evidence collection, they do not take into consideration the need for assessing and verifying (before the incident occurrence) whether the evidences to be generated would be sufficient to: a) prove relevant events that had occurred on the compromised system; b) detect and demonstrate the occurrence of anti-forensic attacks; and c) mitigate the effect of these attacks on compromised evidences. A major interest perceived by research in digital forensic investigation is the development of theoretical and scientifically proven methods which validate the correctness of the techniques used to process and analyze evidences, provide a formal meaning to event reconstruction, and prove the conclusive descriptions regarding the hackers activities. In this context, some important frameworks have been proposed to base the process of digital investigation on formal theory. They can be categorized, based on the formalism they use to reason about attack scenarios, into: expert systems based modeling , finite state Machine (FSM)-based modeling , colored petri nets-based modeling, model checking-based modeling, state-based logic-based modeling, and Incident Response Probabilistic Cognitive Maps based modeling . However, none of these methods is able to cope with the two problems described in the last paragraph, i.e., they do not allow to prove occurred events if the conducted scenarios included anti-forensic attacks, not they allow characterizing provable events to mitigate the effect of these attacks.