State Machine Theory of Digital Forensic Analysis

Software

Event Analysis and Reconstruction in Lisp (EARL) is my historical proof-of-concept software for finite state machine analysis of digital evidence illustrated with a couple of examples.

Articles and Reports

1. J. James, P. Gladyshev, M.T.Abdullah, Y. Zhu "Analysis of Evidence Using Formal Event Reconstruction", in Proceedings of the First International Conference on Digital Fonrensics and Cyberc Crime (ICDF2C), Albany, NY, USA, September 2009.
   • This paper shows that both the system under investigation and the evidence can be described as finite automata. The event reconstruction is then performed by computing the intersection of these automata.
     
2. P. Gladyshev, A. Enbacka "Rigorous Development of Automated Inconsistency Checks for Digital Evidence Using the B Method", International Journal of Digital Evidence, vol. 6, no. 2., Utica College, November 2007.
   • Inconsistencies in evidence may indicate evidence tampering. This paper discusses how a formal model of the system can be used to design and prove validity of evidence inconsistency checks.
     
3. P. Gladyshev, A. Patel "Formalising Event Time Bounding in Digital Investigations", International Journal of Digital Evidence, vol. 4, no. 2., Utica College, December 2005.
   • Event time bounding is a well known technique that allows the investigator to determine temporal boundaries of a particular event using known times of other events, which are causally connected to the event of interest. This paper presents mathematical analysis of this technique, and an algorithm for its automation.
     
4. P. Gladyshev, "Adding Real Time into State Machine Analysis of Digital Evidence", University College Dublin, June 2005.
   • This paper presents mathematical foundations of the temporal reasoning algorithm for EARL library.
   
   
5. P. Gladyshev, "Finite State Machine Analysis of a Blackmail Investigation", International Journal of Digital Evidence, vol. 4, no. 1., Utica College, May 2005.
   • This paper is an informal introduction into state machine analysis of digital evidence llustrated on a real-world example (the example is included into distribution of EARL).
   
   
6. P. Gladyshev, "Formalising Event Reconstruction in Digital Investigations", Ph.D. dissertation, Department of Computer Science, University College Dublin, August 2004.
   • A book-length, in-depth discussion of event reconstruction in digital investgiation.
   
   
7. P. Gladyshev, A. Patel, "Finite State Machine Approach to Digital Event Reconstruction", Digital Investigation journal, vol.1, no. 2, Elsevier, May 2004. A draft of the paper is available here.
   • A concise summary of the Ph.D. dissertation. Gives a formal mathematical definition of the event reconstruction problem in digital investigations and presents an event reconstruction algorithm for solving it.

Pavel Gladyshev, Ph.D., M.Sc., Dip.Eng.

School of Computer Science,
University College Dublin,
Belfield, Dublin 4, Ireland
email: pavel dot gladyshev at ucd dot ie