User:Serguei A. Mokhov/Proposed/Forensic Lucid

• Dr. Serguei A. Mokhov, Concordia University, Montreal, QC, Canada

This article will present Forensic Lucid, a programming/specification language, descendant of the Lucid programming language, founded in intensional logic and Dempster-Shafer mathematical theory of evidence to specify and encode evidence for digital forensics investigation and reason about it automatically with a trace of event reconstruction.

We apply intensional logic to automated cyberforensic analysis and reasoning and event reconstruction and its benefits and difficulties and compares it with the previously defined finite-state automata approach. The intensional logic makes regular mathematical and logic expressions context-aware, i.e., where the context of evaluation is a first-class value and can be manipulated by the logic expressions via context operators. The context consists of dimension-value pairs. To help the study, the foundation of the Forensic Lucid language is laid out along with the forensic context operators to navigate evidential statement and the crime scene specification.

Introduction

This work presents an exploration towards the use of the scientific intensional programming paradigm (Paquet, 1999) to formally model and implement cyberforensics investigation process with the backtrace of event reconstruction, modeling the evidence, and proving or disproving the claims with it in the intensional manner of expression and evaluation. Our proposed solution is intended as a practical improvement on the finite state automata (FSA) approach we have seen in (Gladyshev, 2005; Gladyshev and Patel, 2004).

The base programming language model used in this approach is a new dialect of the Lucid language (Wadge and Ashcroft, 1985; Ashcroft et al., 1995; Ashcroft and Wadge, 1977b; Ashcroft and Wadge, 1976; Ashcroft and Wadge, 1977a), as being implemented within the General Intensional Programming System (GIPSY) (Paquet and Wu, 2005; Mokhov, 2005; Paquet, 2009; Han et al., 2010). As an added benefit arising from the use of Lucid and its GIPSY implementation, the cyberforensics investigation cases may be conducted using a distributed/parallel intensional approach for some form of the event reconstruction. This work is a natural evolution of and refinement of the related works by Mokhov et al. (Mokhov et al., 2008; Mokhov and Paquet, 2008; Mokhov et al., 2009a; Mokhov, 2008a; Mokhov and Vassev, 2009; Mokhov, 2009).

Background

This section summarizes the related research results used in this work. The reader is assumed to have some familiarity with or exposure to the languages, tools, techniques, and concepts introduced here. If it is not the case, please consult the Appendix and the references on the subjects in question. The FSA approach is introduced in the form of a mock up investigation case, followed by a brief introduction to Lucid and GIPSY.

The FSA approach was the first formal approach to cyberforensic analysis and event reconstruction (the other formalisms were studied in (Arasteh and Debbabi, 2007; Arasteh et al., 2007)). While the FSA approach was very valuable to the community, it is not as elegant as it could have been nor it is very usable by the majority of the less-tech-savvy investigators. The goal of this work is to lay a foundation to lead to a solution that remedies these two major drawbacks of the FSA approach. It also takes aim at benefiting from parallel demand-driven context-aware evaluation in terms of implementing system, which the original LISP-based implementation (Gladyshev and Patel, 2004) approach misses out entirely.

We believe the intensional approach to the problem will be an asset in the fields of cyberforensics and intensional logic and programming as it is promising to be more practical and usable than the FSA in the end. Since Lucid was originally designed and used to prove correctness of programs (Ashcroft and Wadge, 1976; Ashcroft and Wadge, 1977a), and is based on the temporal logic and data-flow languages, we can relatively easily adopt its machinery to backtracking in proving or disproving the evidential statements and claims in the investigation process as an expression evaluation that translates to sets of true or false given all the facts in the context providing a set of backtraces. For that we define a novel Lucid dialect with a new set of primitives predefined for forensic tasks. Unlike the LISP-based system implementing the finite state automata, we still retain the flexibility of parallel evaluation of several claims or several components of one claim at the same time by relying on the GIPSY's demand-driven general execution engine (GEE) whose backend is powered by various distributed systems technologies such as the DMS (Lu et al., 2003; Vassev and Paquet, 2005b; Vassev and Paquet, 2005a; Vassev, 2005; Pourteymour et al., 2007; Pourteymour et al., 2008; Pouteymour, 2008).

References

• Arasteh and Debbabi, 2007Arasteh, A. R. and Debbabi, M. (2007). Forensic memory analysis: From stack and code to execution history. Digital Investigation Journal, 4(1):114--125.
• Arasteh et al., 2007 Arasteh, A. R., Debbabi, M., Sakha, A., and Saleh, M. (2007). Analyzing multiple logs for forensic evidence. Digital Investigation Journal, 4(1):82--91.
• Ashcroft et al., 1995 Ashcroft, E. A., Faustini, A. A., Jagannathan, R., and Wadge, W. W. (1995). Multidimensional Programming. Oxford University Press, London. ISBN: 978-0195075977.
• Ashcroft and Wadge, 1976 Ashcroft, E. A. and Wadge, W. W. (1976). Lucid -- a formal system for writing and proving programs. SIAM J. Comput., 5(3).
• Ashcroft and Wadge, 1977a Ashcroft, E. A. and Wadge, W. W. (1977a). Erratum: Lucid -- a formal system for writing and proving programs.SIAM J. Comput., 6(1):200.
• Ashcroft and Wadge, 1977b Ashcroft, E. A. and Wadge, W. W. (1977b). Lucid, a nonprocedural language with iteration. Communications of the ACM, 20(7):519--526.
• AspectJ Contributors, 2007 AspectJ Contributors (2007). AspectJ: Crosscutting Objects for Better Modularity. eclipse.org.(online).
• Debbabi, 2006Debbabi, M. (2006). INSE 6150: Lecture 6: Formal analysis (II). Concordia Institute for Information Systems Engineering, Concordia University, Montreal, Canada. (online).
• Ding, 2004 Ding, Y. (2004). Automated translation between graphical and textual representations of intensional programs in the GIPSY. Master's thesis, Department of Computer Science and Software Engineering, Concordia University, Montreal, Canada. (online).
• Gladyshev, 2005Gladyshev, P. (2005). Finite state machine analysis of a blackmail investigation. International Journal of Digital Evidence, 4(1).
• Gladyshev and Patel, 2004Gladyshev, P. and Patel, A. (2004). Finite state machine approach to digital event reconstruction. Digital Investigation Journal, 2(1).
• Grogono et al., 2005Grogono, P., Mokhov, S., and Paquet, J. (2005). Towards JLucid, Lucid with embedded Java functions in the GIPSY. In Proceedings of the 2005 International Conference on Programming Languages and Compilers (PLC 2005), pages 15--21. CSREA Press.
• Han et al., 2010Han, B., Mokhov, S. A., and Paquet, J. (2010). Advances in the design and implementation of a multi-tier architecture in the GIPSY environment with Java. In Proceedings of SERA 2010, pages 259--266. IEEE Computer Society. abs/0906.4837.
• Lalement, 1993Lalement, R. (1993). Computation as Logic. Prentice Hall. C.A.R. Hoare Series Editor. English translation from French by John Plaice.
• Lu, 2004Lu, B. (2004). Developing the Distributed Component of a Framework for Processing Intensional Programming Languages.

PhD thesis, Department of Computer Science and Software Engineering, Concordia University, Montreal, Canada.

• Lu et al., 2003Lu, B., Grogono, P., and Paquet, J. (2003). Distributed execution of multidimensional programming languages.

In Proceedings of the 15th IASTED International Conference on Parallel and Distributed Computing and Systems (PDCS 2003), volume 1, pages 284--289. International Association of Science and Technology for Development.

• Mokhov and Paquet, 2005Mokhov, S. and Paquet, J. (2005). Objective Lucid -- first step in object-oriented intensional programming in the GIPSY. In Proceedings of the 2005 International Conference on Programming Languages and Compilers (PLC 2005), pages 22--28. CSREA Press.
• Mokhov, 2005Mokhov, S. A. (2005). Towards hybrid intensional programming with JLucid, Objective Lucid, and General Imperative Compiler Framework in the GIPSY. Master's thesis, Department of Computer Science and Software Engineering, Concordia University, Montreal, Canada. ISBN 0494102934; abs/0907.2640.
• Mokhov, 2008aMokhov, S. A. (2008a). Encoding forensic multimedia evidence from MARF applications as Forensic Lucid expressions. In Sobh, T., Elleithy, K., and Mahmood, A., editors, Novel Algorithms and Techniques in Telecommunications and Networking, proceedings of CISSE'08">, pages 413--416, University of Bridgeport, CT, USA. Springer. Printed in January 2010.
• Mokhov, 2008bMokhov, S. A. (2008b). Towards syntax and semantics of hierarchical contexts in multimedia processing applications using MARFL. In Proceedings of the 32nd Annual IEEE International Computer Software and Applications Conference (COMPSAC), pages 1288--1294, Turku, Finland. IEEE Computer Society.
• Mokhov, 2009Mokhov, S. A. (2009). The role of self-forensics modeling for vehicle crash investigations and event reconstruction simulation. In Gauthier, J. S., editor, Proceedings of the Huntsville Simulation Conference (HSC'09), pages 342--349. SCS. abs/0905.2449.
• Mokhov and Paquet, 2008Mokhov, S. A. and Paquet, J. (2008). Formally specifying and proving operational aspects of Forensic Lucid in Isabelle. Technical Report 2008-1-Ait Mohamed, Department of Electrical and Computer Engineering, Concordia University, Montreal, Canada. In Theorem Proving in Higher Order Logics (TPHOLs2008): Emerging Trends Proceedings.
• Mokhov and Paquet, 2010a Mokhov, S. A. and Paquet, J. (2010a). A type system for higher-order intensional logic support for variable bindings in hybrid intensional-imperative programs in GIPSY. In Matsuo, T., Ishii, N., and Lee, R., editors, 9th IEEE/ACIS International Conference on Computer and Information Science, IEEE/ACIS ICIS 2010, pages 921--928. IEEE Computer Society. Presented at SERA 2010; abs/0906.3919.
• Mokhov and Paquet, 2010bMokhov, S. A. and Paquet, J. (2010b). Using the General Intensional Programming System (GIPSY) for evaluation of higher-order intensional logic (HOIL) expressions. In Proceedings of SERA 2010, pages 101--109. IEEE Computer Society. abs/0906.3911.
• Mokhov et al., 2008Mokhov, S. A., Paquet, J., and Debbabi, M. (2008). Formally specifying operational semantics and language constructs of Forensic Lucid. In Goebel, O., Frings, S., Gunther, D., Nedon, J., and Schadt, D., editors, Proceedings of the IT Incident Management and IT Forensics (IMF'08), LNI140, pages 197--216. GI. (online).
• Mokhov et al., 2009aMokhov, S. A., Paquet, J., and Debbabi, M. (2009a). Towards automated deduction in blackmail case analysis with Forensic Lucid. In Gauthier, J. S., editor, Proceedings of the Huntsville Simulation Conference (HSC'09), pages 326--333. SCS.

abs/0906.0049.

• Mokhov et al., 2010Mokhov, S. A., Paquet, J., and Debbabi, M. (2010). The need to support of data flow graph visualization of Forensic Lucid programs, forensic evidence, and their evaluation by GIPSY. Poster at VizSec'10; online at abs/1009.5423.
• Mokhov et al., 2009b Mokhov, S. A., Paquet, J., and Tong, X. (2009b). A type system for hybrid intensional-imperative programming support in GIPSY. In Proceedings of C3S2E'09, pages 101--107, New York, NY, USA. ACM.
• Mokhov and Vassev, 2009Mokhov, S. A. and Vassev, E. (2009). Self-forensics through case studies of small to medium software systems. In Proceedings of IMF'09, pages 128--141. IEEE Computer Society.
• Paquet, 1999Paquet, J. (1999). Scientific Intensional Programming. PhD thesis, Department of Computer Science, Laval University, Sainte-Foy, Canada.
• Paquet, 2009Paquet, J. (2009). Distributed eductive execution of hybrid intensional programs. In Proceedings of the 33rd Annual IEEE International Computer Software and Applications Conference (COMPSAC'09), pages 218--224, Seattle, Washington, USA. IEEE Computer Society.
• Paquet and Kropf, 2000Paquet, J. and Kropf, P. (2000). The GIPSY architecture. In Proceedings of Distributed Computing on the Web, Quebec City, Canada.
• Paquet et al., 2008Paquet, J., Mokhov, S. A., and Tong, X. (2008). Design and implementation of context calculus in the GIPSY environment. In Proceedings of the 32nd Annual IEEE International Computer Software and Applications Conference ({COMPSAC), pages 1278--1283, Turku, Finland. IEEE Computer Society.
• Paquet et al., 2004Paquet, J., Wu, A., and Grogono, P. (2004). Towards a framework for the General Intensional Programming Compiler in the GIPSY. In Proceedings of the 19th Annual ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications ({OOPSLA 2004), pages 164--165, New York, NY, USA. ACM.
• Paquet and Wu, 2005Paquet, J. and Wu, A. H. (2005). GIPSY -- a platform for the investigation on intensional programming languages. In Proceedings of the 2005 International Conference on Programming Languages and Compilers ({PLC 2005), pages 8--14. CSREA Press.
• Paulson et al., 2013Paulson, L. C., Nipkow, T., and Wenzel, M. (2007--2013). Isabelle: A generic proof assistant. University of Cambridge and Technical University of Munich. (online), last viewed March 2013.
• Plaice et al., 2008Plaice, J., Mancilla, B., Ditu, G., and Wadge, W. W. (2008). Sequential demand-driven evaluation of eager TransLucid. In Proceedings of the 32nd Annual IEEE International Computer Software and Applications Conference ({COMPSA), pages 1266--1271, Turku, Finland. IEEE Computer Society.
• Pourteymour et al., 2007Pourteymour, A. H., Vassev, E., and Paquet, J. (2007). Towards a new demand-driven message-oriented middleware in GIPSY. In Proceedings of PDPTA 2007">, pages 91--97. PDPTA, CSREA Press.
• Pourteymour et al., 2008Pourteymour, A. H., Vassev, E., and Paquet, J. (2008). Design and implementation of demand migration systems in GIPSY. In Proceedings of PDPTA 2009">. CSREA Press.
• Pourteymour, 2008Pourteymour, A. H. (2008). Comparative study of Demand Migration Framework implementation using JMS and Jini. Master's thesis, Department of Computer Science and Software Engineering, Concordia University, Montreal, Canada.
• Rahilly and Plaice, 2008Rahilly, T. and Plaice, J. (2008). A multithreaded implementation for TransLucid.

In Proceedings of the 32nd Annual IEEE International Computer Software and Applications Conference ({COMPSAC">), pages 1272--1277, Turku, Finland. IEEE Computer Society.

• Riley, 2011Riley, G. (2007--2011).CLIPS: A tool for building expert systems. (online), last viewed May 2012.
• The GIPSY Research and Development Group, 2013{The GIPSY Research and Development Group (2002--2013). The General Intensional Programming System (GIPSY) project. Department of Computer Science and Software Engineering, Concordia University, Montreal, Canada. (online), last viewed March 2013.
• Tong, 2008 Tong, X. (2008). Design and implementation of context calculus in the GIPSY. Master's thesis, Department of Computer Science and Software Engineering, Concordia University, Montreal, Canada.
• Vassev and Paquet, 2005aVassev, E. and Paquet, J. (2005a). A general architecture for demand migration in a demand-driven execution engine in a heterogeneous and distributed environment. In Proceedings of the 3rd Annual Communication Networks and Services Research Conference ({CNSR 2005), pages 176--182. IEEE Computer Society.
• Vassev and Paquet, 2005bVassev, E. and Paquet, J. (2005b). A generic framework for migrating demands in the GIPSY's demand-driven execution engine. In Proceedings of the 2005 International Conference on Programming Languages and Compilers ({PLC 2005), pages 29--35. CSREA Press.
• Vassev, 2005 Vassev, E. I. (2005). General architecture for demand migration in the GIPSY demand-driven execution engine. Master's thesis, Department of Computer Science and Software Engineering, Concordia University, Montreal, Canada. ISBN 0494102969.
• Viswanadha and Contributors, 2008Viswanadha, S. and Contributors (2001--2008). Java compiler compiler (JavaCC) - the Java parser generator. (online).
• Wadge and Ashcroft, 1985Wadge, W. W. and Ashcroft, E. A. (1985). Lucid, the Dataflow Programming Language. Academic Press, London.
• Wan, 2006Wan, K. (2006). Lucx: Lucid Enriched with Context. PhD thesis, Department of Computer Science and Software Engineering, Concordia University, Montreal, Canada.
• Wan et al., 2005Wan, K., Alagar, V., and Paquet, J. (2005). Lucx: Lucid enriched with context. In Proceedings of the 2005 International Conference on Programming Languages and Compilers ({PLC 2005), pages 48--14. CSREA Press.
• Wu et al., 2010Wu, A., Paquet, J., and Mokhov, S. A. (2010). Object-oriented intensional programming: Intensional Java/Lucid classes. In Proceedings of SERA 2010, pages 158--167. IEEE Computer Society. abs/0909.0764.
• Wu and Paquet, 2005Wu, A. H. and Paquet, J. (2005). Object-oriented intensional programming in the GIPSY: Preliminary investigations. In Proceedings of the 2005 International Conference on Programming Languages and Compilers ({PLC 2005), pages 43--47. CSREA Press.

See also

• Category:Intensional programming