Sciweavers

IJDE
2007

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

13 years 3 months ago
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.
Pavel Gladyshev, Andreas Enbacka
Added 15 Dec 2010
Updated 15 Dec 2010
Type Journal
Year 2007
Where IJDE
Authors Pavel Gladyshev, Andreas Enbacka
Comments (0)