A formal model for forensic storage media preparation tools

This paper defines a model of a special type of digital forensics tools, known as digital media preparation forensic tools, using the formal refinement language Event-B. The complexity and criticality of many types of computer and Cyber crime nowadays combined with improper or incorrect use of digital forensic tools calls for the evidence produced by such tools to be able to meet the minimum admissibility standards the legal system requires, in general implying that it must be generated from reliable and robust tools. Despite the fact that some research and effort has been spent on the validation of digital media preparation forensic tools by means of testing (e.g. within NIST), the verification of such tools and the formal specification of their expected behaviour remains largely under-researched. The goal of this work is to provide a formal specification against which the implementations of such tools can be analysed and tested in the future.