摘要：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 ¨C 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.
