Rigorous Development of Automated Inconsistency Checks for Digital Evidence Using the B Method

Inconsistencies in various data structures, such as missing log records and modified operating system files, have long been used by intrusion investigators and forensic analysts as indicators of suspicious activity. This paper describes a rigorous methodology for developing such inconsistency checks and verifying their correctness. It is based on the use of the B Method – a formal method of software development. The idea of the methodology is to (1) formulate a state-machine model of the (sub)system in which inconsistencies are being detected, (2) formulate consistency criteria for the state of that model, (3) rigorously verify correctness of these criteria using the B Method, and (4) automatically search evidential data for violations of the formulated consistency criteria using ConAlyzer utility developed for this purpose. The methodology is illustrated on an FTP server example.

• Type: Journal
• Year: 2007
• Where: IJDE
• Authors: Pavel Gladyshev, Andreas Enbacka
• Keywords: Consistency Criteria, Formulate Consistency Criteria, IJDE 2007, Various Data Structures