Formal Verification of Necessary and Sufficient Evidence in Forensic Event Reconstruction

Gruber J, Humml M, Schröder L, Freiling F (2023)

Publication Language: English

Publication Type: Conference contribution, Conference Contribution

Publication year: 2023

Pages Range: 1-11

Conference Proceedings Title: Proceedings of the Digital Forensics Research Conference Europe (DFRWS EU)

Event location: Bonn

URI: https://dfrws.org/wp-content/uploads/2023/03/2023-03-20_formal-verification-of-ne-se_gruber_dfrws-proc.pdf

Open Access Link: https://dfrws.org/wp-content/uploads/2023/03/2023-03-20_formal-verification-of-ne-se_gruber_dfrws-proc.pdf

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 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.

Authors with CRIS profile

Related research project(s)

How to cite

APA:

Gruber, J., Humml, M., Schröder, L., & Freiling, F. (2023). Formal Verification of Necessary and Sufficient Evidence in Forensic Event Reconstruction. In Edita Bajramovic and Ricardo J. Rodríguez (Eds.), Proceedings of the Digital Forensics Research Conference Europe (DFRWS EU) (pp. 1-11). Bonn, DE.

MLA:

Gruber, Jan, et al. "Formal Verification of Necessary and Sufficient Evidence in Forensic Event Reconstruction." Proceedings of the Digital Forensics Research Conference Europe (DFRWS EU 2023), Bonn Ed. Edita Bajramovic and Ricardo J. Rodríguez, 2023. 1-11.

BibTeX: Download