The results of the evidence analysis phase in Digital Forensics (DF) provide objective data which however require further elaboration by the investigators, that have to contextualize analysis results within an investigative environment so as to provide possible hypotheses that can be proposed as proofs in court, to be evaluated by lawyers and judges. Aim of our research has been that of exploring the applicability of Answer Set Programming (ASP) to the automatization of evidence analysis. This offers many advantages, among which that of making different possible investigative hypotheses explicit, while otherwise different human experts often devise and select different solutions in an implicit way. Moreover, ASP provides a potential for verifiability which is crucial in such an application field. Very complex investigations for which human experts can hardly find solutions turn out in fact to be reducible to optimization problems in classes P or NP or not far beyond, that can be thus expressed in ASP. As a proof of concept, in this paper we present the formulation of some real investigative cases via simple ASP programs, and discuss how this leads to the formulation of concrete investigative hypotheses.
Digital Forensics (DF) is a branch of criminalistics which deals with the identification, acquisition, preservation, analysis and presentation of the information content of computer systems, or in general of digital devices [1, 2]. The aim is to identify digital sources of proofs, and to organize such proofs in order to make them robust in view of their discussion in court, either in civil or penal trials. Digital forensics is concerned with the analysis of potential elements of proof after a crime has been committed (“postmortem”). Clearly, the development of digital forensics is highly related to the development of Information and communication technologies in the last decades, and to the widespread diffusion of electronic devices and infrastructures. It involves various disciplines such as computer science, electronic engineering, various branches of law, investigation techniques and criminological sciences. Rough evidence must be however used to elicit hypotheses concerning events, actions and facts (or sequences of them) with the goal to present them in court. Evidence analysis involves examining fragmented incomplete knowledge, and defining complex scenarios by aggregation, likely involving time, uncertainty, causality, and alternative possibilities. No single methodology exists today for digital evidence analysis. The scientific investigation experts usually work by means of their experience and intuition (expertise).
In fact, evidence acquisition is supported by a number of hardware and software tools, both closed and open source. These tools are continuously evolving to follow the evolution of the involved technologies and devices. Instead, evidence analysis, is much less supported. In evidence analysis, the technicians and experts perform the following tasks. (i) collect, categorize and revise the evidence items retrieved from electronic devices. (ii) examine them so as to hypothesize the possible existence of a crime and potential crime perpetrators. (iii) elicit from the evidence possible proofs that support the hypotheses. (iv) organize and present the proofs in a form which is acceptable by the involved parties, namely lawyers and judges, which may include to exhibit explicit supporting arguments. Figure 13 shows some real sequences of the technical activities involved. Few software tools exist that only cover some partial aspects, and all of them are “black box” tools, i.e., they provide results without motivation or explanation, and without any possibility of verification. Thus, such results can hardly be presented as reliable proofs to the involved parties. Moreover, the absence of decision support sys
tems leads to undesirable uncertainty about the outcome of evidence analysis. Often, different technicians analyzing the same case reach different conclusions, and this may determine different judge’s decisions in court.
Formal and verifiable artificial intelligence and automated reasoning methods and techniques for evidence analysis would be very useful for the elicitation of sources of proof. Several aspects should to be taken into account such as timing of events and actions, possible (causal) correlations, context in which suspicious actions occurred, skills of the involved suspects, validity of alibis, etc. Moreover, given available evidence, different possible underlying scenarios may exist, that should be identified, examined and evaluated. All the above should be performed via “white box” techniques, meaning that such techniques should be verifiable with respect to the results they provide, how such results are generated, and how the results can be explained. The new wished-for software tools should be reliable and provide a high level of assurance, in the sense of confidence in the system’s correct behavior. computational logic is a suitable candidate to definition and implementation of such tools, and non-monotonic reasoning is clearly extensively required.
The long-term objective of this research is to provide law enforcement, investigators, intelligence agencies, criminologists, public prosecutors, lawyers and judges with decision-support-systems that can effectively aid them in their activities. The adoption of such systems can contribute to making how to proceed clearer and faster, and also under some respects more reliable. In fact, the choice of computational logic as a basis guarantees transparency and verifiability of tools and results. The aim of the present paper is to provide a proof-of-concept of the applicability of computational logic and non-monotonic reasoning to such tasks. In order to convince the several parties involved, whatever limited their computer science expertise might be, we have considered a series of fragments of cases and have transposed them into simple self-explanatory answer set programs which provide results which are easy to understand. However, we have considered fragments of real cases which are presently being investigated by the Italian Department of Scientific Investigations of Carabinieri 4.
We have adopted Answer Set Programming (ASP, cf., among others, [3–9]) because ASP programs are declarative and readable and because, as shown in the following sections, as a matter of fact several analysis problems can be nicely reduced to optimization problems for which ASP is particularly well-suited. In fact, the above picture shows how the analysis phase consists in an ordered sequence of detailed technical activity, performed on the seized memories (or on their forensic copy) following hard rules and formal procedures, through tools and/or forensic equipment, to research specific elements, perform the verification of a state or condition, etc. The outcome of the analysis is a detailed and well-motivated technical report. However these reports , although providing a comprehensive response in technical terms, may be insufficient or even not directly usable from the investigation point of view. Further elaboration is in general needed in order to contextualize technical data in the investigation context. Due to the experience in DF gained by one of the authors of this paper as a member officer of a DF laboratory of an italian police force, with national jurisdiction, it has been possible to identify and experimentally treat (fragments of) complex investigations by reduction to 4 the Police branch of the Italian Army http://www.carabinieri.it answer set programming. This paper presents the results of these experiments. Results are indeed very promising, as the reduction of investigation cases to answer set programming has allowed the experts to identify new investigative hypotheses, that have been practically exploited.
The paper is organized as follows: in Section 2 we provide a short introduction to ASP; in Sections 3- 5 we present three simple though representative examples; finally, in Section 6 we conclude. 2
Answer Set Programming (ASP) in a Nutshell “Answer Set Programming” (ASP) is a well-established logic programming paradigm adopting logic programs with default negation under the answer set semantics, which [3, 4] is a view of logic programs as sets of inference rules (more precisely, default inference rules). In fact, one can see an answer set program as a set of constraints on the solution of a problem, where each answer set represents a solution compatible with the constraints expressed by the program. The reader may refer to [3–9], among others, for a presentation of ASP as a tool for declarative problem-solving.
Syntactically, a program is a collection of rules of the form:
H
L1; : : : ; Lm; not Lm+1; : : : ; not Lm+n where H is an atom, m 0 and n 0, and each Li is an atom. Symbol is usually indicated with :- in practical systems. An atom Li and its negative counterpart not Li are called literals. The left-hand side and the right-hand side of the rule are called head and body, respectively. A rule with empty body is called a fact. A rule with empty head is a constraint, where a constraint of the form L1; :::; Ln: states that literals L1; : : : ; Ln cannot be simultaneously true in any answer set.
A program may have several answer sets, each of which represent a solution to given problem which is consistent w.r.t. the problem description and constraints. If a program has no answer set, this means that no such solution can be found and the program is said to be inconsistent (as opposed to consistent).
In practical terms a problem encoding, in the form of ASP program, is processed by an ASP solver which computes the answer set(s) of the program, from which the solutions can be easily extracted (by abstracting away from irrelevant details). Several well-developed answer set solvers [10] that compute the answer sets of a given program can be freely downloaded by potential users. All solvers provide a number of additional features useful for practical programming, that we will introduce only whenever needed. Solvers are periodically checked and compared over well-established benchmarks, and over challenging sample applications proposed at the yearly ASP competition (cf. [11] for a recent report).
The expressive power of ASP, as well as, its computational complexity have been deeply investigated [12]. Precisely, in the propositional case the problem of deciding whether a given program admits answer sets is NP-complete, and so is the problem of deciding whether there is an answer set containing a specific atom (while deciding whether a specific atom is in all the answer sets is Co-NP-complete). ASP is clearly able to express NP-complete problems.
The judicial authority requested the digital forensics laboratory to analyze the contents of an hard disk, in order to check for the presence of illegal contents files. If so, they requested to check for potential activities of sharing on Internet of illegal materials. The hard disk under analysis was physically damaged (as often done by criminals if they suspect capture). Therefore, after a head replacement, the evidence acquistion phase recovered a large amount of files (of various types: images, videos, documents, etc.), however without their original name. This because the damage present on the disk plates disallowed the recovery the information of the MFT5. For this reason, an arbitrary name has been assigned to all the files recovered. Information about the original name of files and their original location in the file system is thus missing. 3.2
By analyzing the recovered files, technicians detected the occurrence of: – files with illegal contents; – various “INDX files”, corresponding in the NTFS file system to directory files, which contains the follow METADATA: filename; physical and logical size of the file; created, accessed, modified and changed timestamps; – index related to the eMule (which is a widely-used file-exchange application), including a file containing sharing statistics, whose original name is “known.met”.
Starting from the elements described above, we have been able to reply to the judicial authority’s question with: a reasonably reliable hypothesis of association of the recovered file to the respective original name; a reasonable certainty that illegal files were actually exchanged on the Internet. This has been obtained by modeling the given problem by means of a very simple well-known ASP example, reported below. 3.3
The Marriage Problem (or SMP - Stable Marriage Problem) is a well-known NP-hard optimization problem which finds a stable matching between two sets of elements S1 and S2 (say men and women) given a set of preferences for each element. A matching is a mapping from the elements of one set to the elements of the other set which thus creates a set of couples (A; B) where A 2 S1 and B 2 S2. A matching is stable whenever it is not the case that some element A^ of the first matched set prefers some given element B^ of the second matched set over the element to which A^ is already matched, and the same holds for B^. 5 Master File Table: structured block table containing the attributes of all files in the volume of an NTFS file system. 3.4 been created as follow:
arbitrary names.
The given problem is in fact reducible to SMP as follows. In the real case, the lists have – men list: defined as the list of names extracted from directory files “INDX files”; – women: defined as the list of recovered files with have been provisionally assigned
The preferences list (or relation order) between the men and women lists is derived from the comparison of the properties of the individual recovered files (file type, size, etc.) with those identified in file ‘INDX files”. 3.5
Once compiled the lists men, women and preferences, you can search for answer sets by means of the following ASP program (in the syntax of the smodels solver). Facts in the program correspond to a real (though very small) example. preference(f001, flower_jpg). preference(f001, woman_jpg). preference(f002, flower_jpg). preference(f002, child_jpg). preference(f003, child_jpg). preference(f003, woman_jpg). bigamy(X,Y) :- preference(X,Y), preference(X,Y1), couple(X,Y), couple(X,Y1), Y!=Y1. bigamy(X,Y) :- preference(X,Y), preference(X1,Y), couple(X1,Y), X!=X1. couple(X,Y) :- preference(X,Y), not bigamy(X,Y). #hide. #show couple(X,Y). 3.6
The results obtained with the smodels solver on the real example are the follow:
From the answer sets, it is possible (as the reader can see) to formulate hypotheses about the original names of the recovered files. Furthermore, by comparing the file names indexed in the file Known.met6, it has been possible to make reasonable assumptions about the effective sharing of files with illegal content. 4 4.1
After a heinous crime, an allegedly suspect has been arrested. The police sequestered all his mobile devices (smartphone, route navigator, tablet, etc...). The judicial authority requested the DF laboratory to analyze the digital contents of the mobile devices in order to determine their position with respect to the crime site during an interval of time which includes the estimated time when the crime was perpetrated. From the analysis of the mobile devices, a set of geographical GPS coordinates have been extracted, some of them related to the the time interval under investigation. There are however some gaps, one of them certainly due to a proven switch off of few minutes around the crime time. To start with, a list called GPS-LIST is generated, collecting all the positions extracted from the various devices, grouped and ordered by time unit of interest (seconds, multiple of seconds, minutes, etc..). The objective is that of establishing whether the known GPS coordinates are compatible with some path which locates the given mobile devices at the crime site during the given time interval. If no such path exists, then the suspect must be discharged. If some compatible path is found, then the investigation about the potential perpetrator can proceed. The objective has been reached via reduction to the following simple game. Hidato is a logical puzzle (also known as “Hidoku”) invented by the Israeli mathematician Dr. Gyora Benedek. The aim of Hidato is to fill a matrix of numbers, partially filled a priori, using consecutive numbers connected over a horizontal, vertical or diagonal ideal line. Below we show, as a simple example, a 6x6 initial matrix. 18 0 0 0 26 0 19 0 0 27 0 0 0 14 0 0 23 31 1 0 0 8 33 0 0 0 5 0 0 0 0 0 10 0 36 35 6 As mentioned, known.met is a file of the widely-used eMule file-exchange application that stores the statistics of all files that the software shared, all files present in the download list and downloaded in the past. 4.4 It has been possible to perform the reduction of the given investigation problem to the “Hidato Puzzle” problem, by creating a matrix representing the geographical area of interest, where each element of the matrix represents a physical zone crossable in a unit of time. The physical size of the individual cell of the matrix (grid) on the map will be proportionate to the time unit that will be considered, both the hypothetical transfer speed. The matrix has been populated with the elements of the previously-created LISTGPS, i.e., with known positions of the suspect.
Considering the above matrix, assume that the crime has been committed at location 34, at a time included in the interval with lower bound corresponding to when the suspect was at location 1 and upper bound corresponding to when the suspect was at location 36. All devices have been provably switched off between locations 5 and 10. 4.5
Once built the matrix, we can determine whether a suspect route exists by finding the
answer sets of the following ASP program [13] (here we have used the clingo solver).
Notice that the omitted cells are assumed to have value 0.
#const n = 6.
matrix(
matrix(
matrix(
matrix(
These results are particularly interesting for the investigation, as they both correspond to paths which are compatible with the hypothesis of the suspect committing the crime.
18 20 28 29 26 25 19 17 21 27 30 24 13 14 16 22 23 31 1 12 15 8 33 32 2 11 5 9 7 34 3 4 10 6 36 35
It should be noted that a variant of the Hidato algorithm exists, that considers maps whose structure is more complex than a rectangular matrix.
During an investigation concerning a bloody murder, it is necessary check the alibi provided by a suspect. In the questioning, the suspect has been rather vague about the timing of his movements. However, he declared what follows.
– to have left home (place X) at a certain time; – to have reached the office at place Y where he worked on the computer for a certain time; – to have subsequently reached place Z where, soon after opening the entrance door, he discovered the body and raised the alarm.
In order to verify the suspect’s alibi, the judicial authority requested the DF laboratory to analyze: – the contents of the smartphone owned by the suspect; – the computer confiscated in place Y, where the suspect says to have worked; – a video-surveillance equipment installed at a post office situated near place Z, as its video-camera surveys the street that provides access to Z. 5.2
The coroner’s analysis on the body has established the temporal interval including the time of death. From the forensic analysis of the smarphone it has been possible to compile a list of GPS positions related to a time interval including the time of death, denoted by GPS-LIST. The analysis of the computer allowed the experts to extract the list of accesses on the day of the crime, denoted by LOGON-LIST. The analysis of the video-surveillance equipment allowed the experts to isolate some sequences, denoted by VIDEO-LIST, that show a male subject whose somatic features are compatible with the suspect. All the above lists have been ordered according to the temporal sequence of their elements. The investigation case at hand can be modeled as a planning problem where time is a fundamental element in order to establish whether a sequence of actions exist that may allow to reach a certain objective within a certain time. Several approaches to causal and temporal reasoning in ASP exist, that could be usefully exploited for this kind of problem7. Here, for lack of space and for the sake of simplicity we model the problem by means of the very famous “Monkey & Banana” problem, which is the archetype of such kind of problems in artificial intelligence. The specification of “Monkey & Banana” is the following: A monkey is in a room. Suspended from the ceiling is a banana, beyond the monkey’s reach. In the room there is also a chair (in some versions there is a stick, that we do not consider). The ceiling is just the right height so that a monkey standing on a chair could knock the banana down (in the more general version by using the stick, in our version just by hand). The monkey knows how to move around, carry other things around, reach for the banana. What is the best sequence of actions for the monkey? The initial conditions are that: the chair is not just below the bananas, rather it is in a different location in the room; the monkey is in a different location with respect to the chair and the bananas. The reduction of the case at hand to the ‘Monkey & Banana” problem is the following. Notice the reduction of the “idle” state of the monkey to unknown actions that the suspect may have performed at that time.
Monkey ! Banana ! Eats Banana ! Initial Position Monkey ! Initial Position Chair Below Banana Walks Move Chair Ascend Idle
! Y ! Z ! Walks ! Motion to Z ! Open the Door ! Unknown Action Problem’s constraint are that, at any time, the monkey: – may perform only one action at each time instant among walk, move chair, stand on chair, or stay idle; – if the monkey stands on the chair, it cannot walk, and it cannot climb further; – if the chair is not moved then it stays where it is, and vice versa if it is moved it changes its position; – the monkey is somewhere in the room, where it remains unless it walks, which implies changing position; 7 For lack of space we cannot provide the pertinent bibliography: please refer to [14] and to the references therein. – the monkey may climb or move the chair only if it is in the chair’s location; – the monkey can reach the banana only if it has climbed the chair, and the chair is under the banana.
The following ASP program, obtained by modifying a version that can be found at http://www.dbai.tuwien.ac.at/proj/dlv/tutorial/, is formulated for the DLV solver, and provides in the answer sets the timed sequences of actions (if any exists) by which the monkey can reach and eat the banana. walk(Time) v move_chair(Time) v ascend(Time) v idle(Time) v eats_banana(Time) :#int(Time). monkey_motion(T) :- walk(T). monkey_motion(T) :- move_chair(T). stands_on_chair(T2) :- ascend(T), T2 = T + 1. :- stands_on_chair(T), ascend(T). :- stands_on_chair(T), monkey_motion(T). stands_on_chair(T2) :- stands_on_chair(T), T2 = T + 1. reach_banana(T) :- can_reach_banana(T). can_reach_banana(T) :- stands_on_chair(T),
chair_at_place(below_banana, T). :-eats_banana(T), not can_reach_banana(T). :- eats_banana(T1),eats_banana(T2), T1!=T2. happy :- eats_banana(T). :- not happy. step(N, walk, Destination) :- walk(N),
monkey_at_place(Destination, N2),N2 = N + 1. step(N, move_chair, Destination) :move_chair(N),monkey_at_place(Destination, N2),
N2 = N + 1. step(N, ascend, " ") :- ascend(N). step(N, idle, " ") :- idle(N). step(N, eats_banana, " ") :- eats_banana(N). The proposed reduction in the first place allows investigators to verify the alibi provided by the suspect. In fact, the possible timed lists of actions performed by the suspect are determined as answer sets of the above program. Such lists are constructed so as to be compatible with the detected GPS positions of the suspect, the detected computer activity and the actions that the suspect has declared to have performed. By running the solver on the real case with a maximum number of steps N = 3, corresponding to the case where the suspect is provably at the office at time 0, we get exactly the action sequences needed to reach the goal. {step(0,walk,chair_starting_point), step(1,move_chair,below_banana), step(2,ascend," "), step(3,eats_banana," ")} Therefore, if the suspect raised the alarm at time 3 he actually had no time for committing the crime and therefore he should presumably be discharged.
In case instead the alibi is not fully verified, then further investigation is needed. By increasing the time, for example to N = 5, we in fact get many sets of possible alternative actions, where idle is an unknown action for which it might interesting to investigate further so as to prove or reject the investigation thesis. {step(0,idle," "),step(1,walk,chair_starting_point), step(2,move_chair,below_banana), step(3,ascend," "), step(4,idle," "),step(5,eats_banana," ")} {step(0,walk,below_banana), step(1,walk,chair_starting_point), step(2,move_chair,below_banana), step(3,ascend," ") step(4,idle," "), step(5,eats_banana," ") } Among the answer sets there are many which suggest suspicious behavior. The first one above outlines a scenario where the initial suspect’s actions are unknown. Then he moves to the crime site where however he has the time and opportunity to commit the crime at step 4. Even worse is the second answer set, where the suspect moves to the crime site, than moves back to the office, moves a second time to the crime site where again he has the time and opportunity to commit the crime at step 4. As the suspect’s presence at the crime site is confirmed by the video-surveillance equipment records, this behavior is suggestive of, e.g., going to meet the victim and having a discussion, going back to the office (maybe to get a weapon) and then actually committing the crime. 6
In this paper we have demonstrated the applicability of non-monotonic reasoning techniques to evidence analysis in digital forensics by mapping some fragments of real cases to existing simple answer set programs. The application of artificial intelligence and in particular of non-monotonic reasoning techniques to evidence analysis is a novelty: in fact, even very influential publications in digital forensics such as [1, 2] are basically a guide for human experts about how to better understand and exploit digital data. Therefore the present work, though preliminary, opens significant new perspectives. Future developments include building a toolkit exploiting not only ASP but also other nonmonotonic-reasoning techniques such as abduction, temporal reasoning, causal reasoning and others, as elements of decision-support-systems that can effectively aid investigation activities and support of the production of evidence to be examined in trial. The multidisciplinary future challenge is that of making such tools formally accepted in court proceedings: this involves in general terms complex societal and psychological issues. From the technical point of view, for making such tools acceptable and perceived as reliable, it is crucial to develop verification, certification, assurance and explanation techniques.