There is Something Fishy About Your Evidence... Or How to Develop Inconsistency Checks for Digital Evidence Using the B Method

Get BibTex-formatted data

Author

Pavel Gladyshev & Andrea Enbacka

Entry type

techreport

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.

Date

2006 – 6 – 1

Key alpha

Gladyshev

Publication Date

2006-06-01

Location

A hard-copy of this is in the CERIAS Library

BibTex-formatted data

To refer to this entry, you may select and copy the text below and paste it into your BibTex document. Note that the text may not contain all macros that BibTex supports.

@Techreport{ Gladyshev,
	title = "There is Something Fishy About Your Evidence... Or How to Develop Inconsistency Checks for Digital Evidence Using the B Method",
	author = "Pavel Gladyshev & Andrea Enbacka",
	year = "2006",
	month = "6",
	day = "1",
	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.",
}