Confidence in digital forensics software is of vital importance when digital evidence is examined. This project examines how to establish that digital forensics software is trustworthy via mechanized theorem provers and formal methods.

We have developed an architecture for independent verification of the results from digital forensics software. This is based on the use of forensic certificates. See verifiable forensic certificates for further details. The feasibility of verifying forensic certificates with the Coq theorem prover has been examined as part of this investigation, see verifying Honeynet challenge reports.

• Certificates for Verifiable Forensics, by Radha Jagadeesan, CM Lubinski, Corin Pitcher, James Riely, and Charles Winebrinner. In Computer Security Foundations Symposium (CSF), 2014.
• Feasible Formal Forensics: Computational Proofs of a Honeynet Challenge, by CM Lubinski. MS thesis.
• Generation of Verifiable Evidence for Declarative Data Forensics: A File System Case Study, by Iana Boneva, Radha Jagadeesan, Corin Pitcher, and James Riely. Unpublished manuscript (Source code).

The following scripts for the Coq theorem prover are available:

• Code and CoqDoc documentation for formal verification of a forensic report for a Honeynet Challenge. For further details, see verifying Honeynet challenge reports.

For further information, contact Corin Pitcher [cpitcher@cs.depaul.edu].