A Hierarchical Visibility theory for formal digital investigation of anti-forensic attacks

Among the leading topics of research in digital forensic investigation is the development of theoretical and scientifically proven techniques of incident analysis. However, two main problems, which remain unsolved in the literature, could lead the use of formal approaches of attack scenarios reconstruction and incident analysis to be inconclusive. The former is related to the absence of techniques to model and characterize anti-forensic attacks, and cope with the reconstruction of attack scenarios based on evidences compromised by these attacks. The latter is related to the lack of theoretical techniques usable during the preparation of systems to forensic analysis (i.e., the first phase of a forensic process that precedes the occurrence of an incident and the collection of evidences). These techniques are expected to determine the optimal set of security solutions to deploy so that the evidences to be generated further to a security incident would be sufficient to prove a wide range of anti-forensic attacks.In this paper we propose a formal approach, based on a novel theory of Hierarchical Visibility, allowing to forensically investigate security incidents that are conducted over complex systems and integrate anti-forensic attacks. We develop a formal logic-based model useful for the representation of complex systems and scenarios of attacks under different levels of abstractions, and the description of the deployed security solutions together with the evidences they generated. The theory of Hierarchical Visibility that we provide in this paper allows reasoning on anti-forensic attacks over complex systems, characterize situations under which they are provable, and prove their occurrence starting from incomplete evidences. An extension of the forensic process showing the use of Hierarchical Visibility theory to increase the number of provable anti-forensic attacks, is described. We illustrate the proposal using a case study related to the investigation of a denial of service attack over an SSH service.