What is the purpose of the reconstruction function in a forensics investigation?

The rapid growth of digital technology and its effect on human's routine life require some defensive and preventive techniques and methods. Besides the popular and well known techniques such as anti-viruses, anti-spams, intrusion detection systems, intrusion prevention systems, and firewalls, a new solution called digital forensic emerged in the late 1990s. Digital forensic is some kind of post mortem analysis. It tries to collect pieces of evidence from different digital media, reconstruct potential events using these data, and prepare accepted reports for the court (Soltani et al., 2019). Event reconstruction is a fundamental phase in digital forensic. It reveals approximately what has happened on a compromised system. Since reports are built on the findings of these analyses, providing rigorous and strict methods for reconstructing events is very important (Gladyshev and Patel, 2004). One way to reconstruct events rigorously is to use the formal mathematical methods. The intended system is modeled as a labelled transition graph and the desired property is specified using some logic such as temporal logic. Finally, a model checking algorithm is used to verify that the model meets the specified property.

Formal methods are used for different purposes. Formal methods are usually used in verification of hardware devices before mass production starts. It is a good design practice to spend some time and money on formal verification of new hardware devices. It prevents many system failures which impose huge costs on companies. For example the Pentium FDIV bug cost Intel $475 million to recall the chips (Pratt, 1995). Moreover, formal methods are used to verify software products. Nowadays, various companies such as Microsoft, Intel, Siemens, IBM, HP, AT&T and Motorola are using formal analysis tools in their designs (Aceto et al., 2007). Formal methods are also necessary in design of vital and critical systems. One small bug in a complicated system might crash the whole system. For example, the explosion of the $7 billion Ariane 5 rocket was due to the conversion of a 64-bit real number to a 16-bit integer (LIONS, 1996).

It should be noted that formal methods are also used for some purposes other than system verification. For example, model checking can be used to provide further insights into the effectiveness of treatment plans for cancer patients (Bowles and Silvina, 2016). For digital forensic investigations, formal methods might be used for the following reasons:

Legal issues: The digital investigator must provide admissible reports for the court. There are various methods and tools which analyze pieces of evidence and produce reports. However, most of them do not fulfill legal requirements. Rigorous formal methods are a good solution to this issue. These methods model the given system and specify the desired properties. For example, a digital forensic property might be whether there is a process which is hidden using some DKOM1 technique. Model checking methods explore the state space of the modeled system and check whether the desired property holds on the model. If the property does not hold, a counter example is generated. However, if no counter example is found, it is guaranteed that the model satisfies the property.

Reproducibility: It is necessary that the event reconstruction method be reproducible. The reproducibility allows independent bodies to reproduce the same events using the same set of evidence (Chabot et al., 2014). Formal methods provide this requirement.

Abstraction: Instead of working on real system, an abstract model of the system is captured. The model only considers the important properties of the system and ignores extra details.

Automation: It is desirable to automate the reconstruction of events. Model checking techniques provide algorithms which automatically check properties on the model.

Hypothesis-making: The collected evidence from digital medial usually lacks some information due to the volatile nature of digital data. Therefore, events might not be reconstructed perfectly. It is desirable to let the investigator propose some hypotheses about the missing information. Currently there is a trend towards extending formal methods to include some uncertain facts (Rekhis and Boudriga, 2012; Willassen, 2008a).

This study presents a formal event reconstruction framework. The proposed framework models the investigated system using a process algebra method. Moreover, it specifies the digital forensic properties using a rich temporal logic. Finally, it uses the model checking technique to check the satisfaction of the property on the model. The rest of the paper is organized as follows. Section 2 presents a review of the literature on the subject. Section 3 gives some background information about the temporal logic model checking and mCRL2 formal specification language. Section 4 proposes a formal event reconstruction framework. Modeling and specifying the FAT file system and an analysis of its state space are discussed in Section 5. A case study is reviewed in Section 6. Finally, Section 7 concludes the paper and proposes some future works.

Literature review

There have been several attempts to reconstruct digital events using various collected evidence. However, only a few of them are based on formal methods (Alrajeh et al., 2017; Arasteh et al., 2007; Carrier and Spafford, 2006; Chabot et al., 2014; Gladyshev and Patel, 2004; James et al., 2009; Rekhis and Boudriga, 2005a, 2005b; Willassen, 2008b). Gladyshev and Patel (2004) have modeled the hacked system as a finite state machine, which can be explored to determine all possible scenarios of the

Temporal logic model checking

There is a growing need for reliable methods of reconstructing events in digital forensic investigations. A good solution to this need is to apply formal mathematical methods in the process of event reconstruction. In this study, we will use temporal logic model checking (Clarke and Emerson, 1981) for verifying digital forensic properties on the systems. Temporal logic model checking is one of the most useful techniques for automated verification of systems. The basic idea is that the system is

A formal event reconstruction framework

In this section, we will propose a formal event reconstruction framework which is based on the model checking technique. The first component of the formal event reconstruction framework models the system under investigation. The second component formulates the digital forensic question by a temporal logic. Finally, the third component checks whether the required digital forensic property holds on the model using a model checking algorithm. Fig. 2 shows the components of the formal event

Modeling and specifying the FAT file system

In this section, the FAT file system will be modeled using mCRL2 process language. To this end, the process FatFileSystem is defined which has two arguments of sorts FatEntries and RootDirectoryEntries. The FatFileSystem process is shown in Fig. 3. Moreover, the full model of FAT file system is presented in Appendix A. FatEntries is a list of type FAT_ENTRY. FAT_ENTRY, itself is a structured sort. The FAT_ENTRY = struct fat_entry(index: Nat, next: Nat) says that any term of sort FAT_ENTRY can

Case study

In this section, we have applied the proposed event reconstruction framework to a case study presented in (Gladyshev and Patel, 2004). The following description, with some omissions, is taken from (Gladyshev and Patel, 2004). “The local area network at ACME Manufacturing consists of two personal computers and a networked printer. The cost of running the network is shared by its two users Alice (A) and Bob (B). Alice, however, claims that she never uses the printer and should not be paying for

Conclusion and future works

Digital forensic investigation includes collecting pieces of evidence from the system, reconstructing events using these data, and preparing reports for the court. The results should be verifiable and reproducible which necessitates using some formal mathematical methods for reconstructing events. This research has proposed a formal event reconstruction framework which is based on the model checking technique. It has modeled the system under investigation using a process algebra method.

Acknowledgements

We'd like to thank Prof. Jan Friso Groote and Thomas Neele for their help on working with mCRL2. Additionally, we wish to thank the reviewers for their helpful evaluation.

Cited by (12)

Recommended articles (6)