A Formalisation of Digital Forensic String Search Specifications

Abstract

Computer forensic tools are tools concerned with the identification, recovery, preservation and analysis
of evidence in digital media involved in criminal investigations and illegal cases. String search
tools are a special class of such forensic tools, which are used to search for specific queries in the
investigated medium. However, one main issue we find in literature mainly is that computer forensic
tools, including string search tools, are generally specified in an informal and oftentimes ambiguous
and inconstant manner. We adopt in this short paper formal specification approaches, in particular
Event-B, in order to define clearly the behaviour and properties of string search tools, a class of computer
forensic tools, and investigate whether there are any requirements that cannot be achieved. Our
results show that some basic and optional requirements as stated in literature related to string search
tools could be not be consistent and some are unnecessarily restrictive.