Abstract

Forensic examination of logs plays a big role in modern computer security. Due to the sheer amount of data involved and the evolving complexity of computer systems, the forensic examination of logs is a time consuming and daunting task. Information stored in logs of a computer system is of crucial importance to gather forensic evidence of investigated actions or attacks against the system. Analysis of this information should be rigorous and credible, hence it lends itself to formal methods. In this thesis, we propose a model checking approach to the formalization of the forensic log analysis. In order to provide a structure to the log events, we express each event as a term of a term algebra. The signature of the algebra is carefully chosen to include all relevant information necessary to conduct the analysis. Properties of the model are expressed as formulas of a logic having dynamic, linear, temporal, and modal characteristics. A tableau-based proof system is provided for this logic upon which a model checking algorithm can be developed. In order to illustrate the proposed approach, the Windows XP auditing system is utilized. The properties that we capture in our logic include invariant properties of a system, forensic hypotheses, and generic or specific attack signatures. Moreover, we discuss the admissibility of forensics hypotheses and the underlying verification issues. Throughout our research we realized the significance the Windows registry can provide when correlated with the logs. The registry, being a source of system and application information, provides a reference point when detecting anomalies in the logs. Correlating the registry with the logs leverages the forensic analysis adding evidence to the investigation. We present the method of the correlation as well as a proof-of-concept implementation of the correlation of logs with the registry.