Formal Digital Investigation of Anti-forensic Attacks

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.