Automata Intersection to Test Possibility of Statements in Investigations

When conducting an investigation, many statements are given by witnesses and suspects. A “witness” could be considered as anything that provides information about the occurrence of an event. While a witness may traditionally be a human, a digital device – such as a computer or cell phone – could also help to provide information about an event. Once a witness provides a statement, the investigator needs to evaluate the level of trust he or she places in the validity of the statement. For example, a statement from a witness that is known to lie may be considered less trustworthy Similarly, in the digital realm, information gathered from a device may be less trustworthy if the device has been known to be compromised by a hacker or virus.

When an investigator gets statements from witnesses, the investigator can then begin to restrict possibilities of happened events based on the information. For example, if a trustworthy witness says she saw a specific suspect at a specific time, and the suspect claims to be out of the country at that time, these are conflicting statements. A witness statement may not be true for a number of reasons, but the statement may be highly probable. At a minimum when conflicting statements occur, these indicate that one or both statements should be investigated further to find either inculpatory or exculpatory evidence.

If an action happens that affects a computer system, observation of the affected data in the system could be used a evidence to reduce the possible states the system could have been in before it’s current state. Taking this further, if we create a complete model of a system then without any restriction on the model, any state of the system could possibly be reachable.

Computer systems can be modeled as finite state automata (FSA). In this model, each state of the system is represented as a state in the FSA. The set of all states is defined as Q. Each action that alters the state of the system can be represented as a symbol in the alphabet (Σ) of the automaton. Moving from one state to another is controlled by a transition function δ where δ: Q × Σ → Q.

In the case of an investigation of a computer system, the investigator may be able to directly observe only the final state of the system. The set of final, or accepting, states is defined as F, where F ⊆ Q. The start state (q₀, where q₀∈ Q) is likely to be unobservable, and may be unknown. Because of this, any state in the model may potentially be a start state. To account for this, a generic start state g, where  g ∉ Q, can be defined. g is a generic start state with a tradition to each state in Q on each input leading to that particular state. The result of this process is a model of the system that allows for any possible transitions in the system that result in the observed final state from any starting state.

This FSA of the system can then be used to test statements about interactions with the system. As a very basic example, consider an FSA with only two states. The first state is the system before a program is ran, and no prefetch entry has been created (!PrefetchX). The second state is after a program has been ran, and a prefetch entry has been created (PrefetchX). The transition symbol is defined as “Run_Program_X”. The FSA can be visiualized as:

(!PrefetchX) -> Run_Program_X -> (PrefetchX)

For the sake of this example, it is known that a prefetch entry will not be created unless a program is ran, so the start state is defined as (!PrefetchX). An investigator observes that in the final state of the system PrefetchX did exist, so the final accepting state is (PrefetchX).

A suspect who normally uses the system is asked whether they executed Program X, and she claims she did not. Her statement may then also be modeled in terms of the previous FSA, where any transition is allowed except “Run_Program_X”. Her statement can be visualized as:

(*) -> !Run_Program_X -> (*)

In this statement, she is claiming that any state and transition is possible except for “Run_Program_X”.

When both the system and the suspect’s statement are modeled, the FSA can be intersected to determine if the final observed state of the system is reachable with the restrictions the suspect statement places on the model. In the given example, the only possible transition to get to the observed final state is Run_Program_X. If the system model were intersected with the suspect’s statement, the final state (PrefetchX) would not be reachable because the transition that leads to the final state would not be possible. In this case, the suspect statement is inconsistent with the observed final state, and should therefore be investigated further.

This very simple example can be applied to more complex situations and models; however, a challenge with using a computational approach to model real-world systems is a very large state-space to model even for relatively simple systems.

For a more in-depth explanation, please see Analysis of Evidence Using Formal Event Reconstruction.

[1] James, J., P. Gladyshev, M.T. Abdullah, Y. Zhu. (2010) “Analysis of Evidence Using Formal Event Reconstruction.” Digital Forensics and Cyber Crime 31: 85-98. [PDF][arXiv:1302.2308]