Abstract
Inconsistencies fin various data structures, such as missing log records and modified operating system files, have 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) formulating inconsistency checks in terms of that model, and (3) rigorously verifying correctness of these checks using the B Method. The methodology is illustrated by developing ConAlyzer utility- an inconsistency checker for the FTP log files.
