Modelling and refinement of forensic data acquisition specifications |
| |
| Institution: | 1. Faculty of Information Technology, Brno University of Technology, Brno, Czech Republic;2. Hilti Chair for Data and Application Security, Institute of Information Systems, University of Liechtenstein, Liechtenstein;3. Waterford Institute of Technology, Waterford, Ireland;4. Albstadt-Sigmaringen University, Sigmaringen, Germany;1. School of Information Science and Engineering, Hunan University, Changsha, Hunan Province 410082, China;2. Key Laboratory for Embedded and Network Computing of Hunan Province, Hunan University, Changsha, Hunan Province 410082, China |
| |
| Abstract: | This paper defines a model of a special type of digital forensics tools, known as data acquisition 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 more robust and reliable specifications of the functionality of digital forensics applications. As a minimum, the evidence produced by such tools must 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 forensics tools by means of testing, 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 implementations of data acquisition procedures can be analysed. |
| |
| Keywords: | Computer forensics Disk data acquisition Formal specifications Event-B method Formal refinement |
| 本文献已被 ScienceDirect 等数据库收录！ |
|
