Toward Formal Reasoning in Cyberforensic Case Investigation with Forensic Lucid

Title: Toward Formal Reasoning in Cyberforensic Case Investigation with Forensic Lucid

Speaker: Serguei A. Mokhov, Concordia University, Montreal, Canada

Time:  Tuesday, May 8, 2012; 10:00-11:30

Location:  East Main Building 10-101

Abstract:  This work focuses on the application of the intensional logic to cyberforensic analysis and its benefits and difficulties are compared with the finite-state automata approach. This work extends the use of the scientific intensional programming paradigm onto modeling and implementation of a cyberforensics investigation process with the backtrace of event reconstruction, modeling the evidence as multidimensional hierarchical contexts, and proving or disproving the claims with it in the intensional manner of evaluation. This is a practical, context-aware improvement over the finite state automata (FSA) approach we have seen in the related works. As a base implementation language model we use in this approach is a new dialect of the Lucid programming language, that we call Forensic Lucid and we define hierarchical contexts based on the intensional logic for the evaluation of cyberforensic expressions. We also augment the work with the credibility factors surrounding digital evidence and witness accounts, which have not been previously modeled. The Forensic Lucid programming language proposed for this intensional cyberforensic analysis, includes the syntax and operational semantics. In large part, the language is based on its predecessor and codecessor Lucid dialects, such as GIPL, Indexical Lucid, Lucx, Objective Lucid, and JOOIP bound by the intensional (temporal) logic that is behind them. The distributed Java-based eduction (demand-driven) evaluation engine of the General Intensional Programming System (GIPSY) is the run-time system to cope with the scalability issues of the large evidential knowledge base. We then propose a near future work with the dataflow graph visualization and a toolset for compilation and execution of the Forensic Lucid programs. We show some examples by re-writing them in Forensic Lucid. We then postulate other investigations applications beyond the digital forensics domain.

This work is based in part on the following papers:

"Reasoning About a Simulated Printer Case Investigation with Forensic Lucid", http://arxiv.org/abs/0906.5181

"Towards Automated Deduction in Blackmail Case Analysis with Forensic Lucid", http://arxiv.org/abs/0906.0049

"Formally Specifying Operational Semantics and Language Constructs of Forensic Lucid", http://subs.emis.de/LNI/Proceedings/Proceedings140/gi-proc-140-014.pdf

"On the Need for Data Flow Graph Visualization of Forensic Lucid Programs and Forensic Evidence, and their Evaluation by GIPSY", http://arxiv.org/abs/1009.5423

"Using the General Intensional Programming System (GIPSY) for Evaluation of Higher-Order Intensional Logic (HOIL) Expressions", http://arxiv.org/abs/0906.3911

Bio:  Serguei Mokhov is a PhD Candidate in Computer Science, Concordia University, Montreal, Canada where he completed his bachelor's and master's degrees in Computer Science and Information Systems Security. Mr. Mokhov is presently a Senior Scholar visiting Tsinghua University, Beijing, China, the Department of Computer Science and Technology, the Visualization and Graphics Lab. He additionally is a part-time faculty member at the Department of Computer Science and Software Engineering and a Systems Administrator in the Faculty of Engineering and Computer Science's Network Administration Group. He is also an Assistant Editor of Scholarpedia, a peer-reviewed open-access encyclopedia, TPC member in several conferences and a referee for a few journals. Mr. Mokhov's multidisciplinary research includes diverse aspects in distributed and parallel computing, pattern recognition and data mining, computer forensics and security, computer graphics and visualization, intensional programming, autonomic computing, and software engineering, where he has had a number of publications. Serguei Mokhov is a strong proponent and developer of open-source software, having contributed most of his research software to the community.