A formalisation of digital forensic string search specifications

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.