Authors: Jan Gruber, Merlin Humml, Lutz Schröder and Felix C. Freiling
DFRWS EU 2023
Abstract
We study the problem of digital forensic event reconstruction, i.e., the question of whether a certain event has happened in the past of an execution by a given digital system. Instead of devising new
search algorithms to solve the problem directly, we define two novel concepts in standard lineartime temporal logic and use these concepts to solve event reconstruction using established tools for
model checking. The first concept is that of sufficient evidence, i.e., a characterization of states whose observation is sufficient to prove that a certain event happened in the past. The second concept is that of necessary evidence, i.e., a characterization of states whose negation can be used to refute the claim that a certain event happened in the past. Using the model checker NuSMV, we built a prototype that can calculate these two sets for a given digital system in order to solve the forensic event reconstruction problem. We relate these concepts to previous work in formal event reconstruction and apply it to Gladyshev’s “ACME Manufacturing” benchmark example to illustrate the usefulness of our approach and the improved notion of digital evidence.