Formal Verification of Necessary and Sufficient Evidence in Forensic Event Reconstruction - Gruber, Jan; Humml, Merlin; Schröder, Lutz; Freiling, Felix (Proceedings of the Digital Forensics Research Conference Europe (DFRWS EU), 2023)
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 defne two novel concepts in standard linear- time temporal logic and use these concepts to solve event reconstruction using established tools for model checking. The fiirst 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.
Keywords: digital evidence; digital investigations; forensic event reconstruction; formal methods; forensic computing