Login | Register

Toward Formal Reasoning in Cyberforensic Case Investigation with Forensic Lucid

Title:

Toward Formal Reasoning in Cyberforensic Case Investigation with Forensic Lucid

Mokhov, Serguei A. (2012) Toward Formal Reasoning in Cyberforensic Case Investigation with Forensic Lucid. In: Lecture: Toward Formal Reasoning in Cyberforensic Case Investigation with Forensic Lucid, May 8, 2012, East Main Building 10-101, Department of Computer Science and Technology, Tsinghua University, Beijing, China.

[thumbnail of Lecture]
Preview
Text (Lecture) (application/pdf)
tsinghua-forensic-lucid-presentation.pdf - Presentation
2MB

Official URL: http://www.tsinghua.edu.cn/publish/csen/4927/2012/...

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.

Divisions:Concordia University > Gina Cody School of Engineering and Computer Science > Computer Science and Software Engineering
Concordia University > Gina Cody School of Engineering and Computer Science > Concordia Institute for Information Systems Engineering
Concordia University > Research Units > Computer Security Laboratory
Item Type:Conference or Workshop Item (Lecture)
Refereed:No
Authors:Mokhov, Serguei A.
Date:8 May 2012
Projects:
  • Forensic Lucid
  • Intensional Cyberforensics
  • General Intensional Programming System (GIPSY)
Funders:
  • China-Canada Scholars Exchange Program (CCSEP)
  • Faculty of Engineering and Computer Science (ENCS), Concordia University, Canada
  • NSERC
Keywords:Forensic Lucid, intensional logic, formal methods, digital investigation
ID Code:974044
Deposited By: Serguei Mokhov
Deposited On:14 May 2012 20:49
Last Modified:18 Jan 2018 17:37

References:

[1] G. Allwein and J. Barwise, editors. Logical reasoning with diagrams. Oxford University Press, Inc., New York,
NY, USA, 1996. ISBN 0-19-510427-7.
[2] E. A. Ashcroft and W. W. Wadge. Lucid – a formal system for writing and proving programs. SIAM J. Comput.,
5(3), 1976.
[3] E. A. Ashcroft and W. W. Wadge. Erratum: Lucid – a formal system for writing and proving programs. SIAM J.
Comput., 6(1):200, 1977.
[4] E. A. Ashcroft and W. W. Wadge. Lucid, a nonprocedural language with iteration. Communications of the
ACM, 20(7):519–526, July 1977. ISSN 0001-0782. doi: 10.1145/359636.359715.
[5] E. A. Ashcroft, A. A. Faustini, R. Jagannathan, and W. W. Wadge. Multidimensional Programming. Oxford
University Press, London, Feb. 1995. ISBN: 978-0195075977.
[6] AspectJ Contributors. AspectJ: Crosscutting Objects for Better Modularity. eclipse.org, 2007.
http://www.eclipse.org/aspectj/.
[7] R. Bardohl, M. Minas, G. Taentzer, and A. Sch¨ urr. Application of graph transformation to visual languages. In
Handbook of Graph Grammars and Computing by Graph Transformation: Applications, Languages, and Tools,
volume 2, pages 105–180. World Scientific Publishing Co., Inc., River Edge, NJ, USA, 1999. ISBN
981-02-4020-1.
[8] Y. Ding. 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, June 2004.
http://newton.cs.concordia.ca/~paquet/filetransfer/publications/theses/DingYiminMSc2004.pdf
[9] Y. Ding. 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, 2004.
[10] W. Du. On the relationship between AOP and intensional programming through context, July 2005. Keynote
talk at the Intensional Programming Session of PLC’05.
[11] Eclipse contributors et al. Eclipse Platform. eclipse.org, 2000–2012. http://www.eclipse.org, last viewed
April 2012.
[12] P. Gladyshev. Finite state machine analysis of a blackmail investigation. International Journal of Digital
Evidence, 4(1), 2005.
[13] P. Gladyshev and A. Patel. Finite state machine approach to digital event reconstruction. Digital Investigation
Journal, 2(1), 2004.
[14] P. Grogono, S. Mokhov, and J. Paquet. 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, June 2005.
[15] R. Haenni, J. Kohlas, and N. Lehmann. Probabilistic argumentation systems. Technical report, Institute of
Informatics, University of Fribourg, Fribourg, Switzerland, Oct. 1999.
[16] B. Han, S. A. Mokhov, and J. Paquet. 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,
2010. ISBN 978-0-7695-4075-7. doi: 10.1109/SERA.2010.40. Online at http://arxiv.org/abs/0906.4837.
[17] IBM, BEA Systems, Microsoft, SAP AG, and Siebel Systems. Business Process Execution Language for Web
Services version 1.1. [online], IBM, Feb. 2007.
http://www.ibm.com/developerworks/library/specification/ws-bpel/.
[18] Y. Ji. Scalability evaluation of the GIPSY runtime system. Master’s thesis, Department of Computer Science
and Software Engineering, Concordia University, Montreal, Canada, Mar. 2011.
[19] D. Koenig. Web services business process execution language (WS-BPEL 2.0): The standards landscape.
Presentation, IBM Software Group, 2007.
[20] N. G. Miller. A Diagrammatic Formal System for Euclidean Geometry. PhD thesis, Cornell University, U.S.A,
2001.
[21] S. Mokhov and J. Paquet. 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, June 2005.
[22] S. A. Mokhov. 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, Oct. 2005. ISBN 0494102934; online at
http://arxiv.org/abs/0907.2640.
[23] S. A. Mokhov. 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, July 2008. IEEE Computer Society. doi:
10.1109/COMPSAC.2008.206.
[24] S. A. Mokhov and J. Paquet. 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, Aug. 2008. In Theorem Proving in Higher Order Logics
(TPHOLs2008): Emerging Trends Proceedings.
[25] S. A. Mokhov and J. Paquet. 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, May 2010. ISBN 978-0-7695-4075-7. doi: 10.1109/SERA.2010.23. Online at
http://arxiv.org/abs/0906.3911.
[26] S. A. Mokhov and E. Vassev. Self-forensics through case studies of small to medium software systems. In
Proceedings of IMF’09, pages 128–141. IEEE Computer Society, Sept. 2009. ISBN 978-0-7695-3807-5. doi:
10.1109/IMF.2009.19.
[27] S. A. Mokhov, J. Paquet, and M. Debbabi. Designing a language for intensional cyberforensic analysis.
Unpublished, 2007.
[28] S. A. Mokhov, J. Paquet, and M. Debbabi. Formally specifying operational semantics and language constructs
of Forensic Lucid. In O. G¨ obel, S. Frings, D. G¨unther, J. Nedon, and D. Schadt, editors, Proceedings of the IT
Incident Management and IT Forensics (IMF’08), LNI140, pages 197–216. GI, Sept. 2008. ISBN
978-3-88579-234-5. Online at
http://subs.emis.de/LNI/Proceedings/Proceedings140/gi-proc-140-014.pdf.
[29] S. A. Mokhov, J. Paquet, and M. Debbabi. Towards automated deduction in blackmail case analysis with
Forensic Lucid. In J. S. Gauthier, editor, Proceedings of the Huntsville Simulation Conference (HSC’09), pages
326–333. SCS, Oct. 2009. ISBN 978-1-61738-587-2. Online at http://arxiv.org/abs/0906.0049.
[30] S. A. Mokhov, J. Paquet, and X. Tong. A type system for hybrid intensional-imperative programming support in
GIPSY. In Proceedings of C3S2E’09, pages 101–107, New York, NY, USA, May 2009. ACM. ISBN
978-1-60558-401-0. doi: 10.1145/1557626.1557642.
[31] S. A. Mokhov, J. Paquet, and M. Debbabi. On the need for data flow graph visualization of Forensic Lucid
programs and forensic evidence, and their evaluation by GIPSY. In Proceedings of the Ninth Annual
International Conference on Privacy, Security and Trust (PST), 2011, pages 120–123. IEEE Computer Society,
July 2011. ISBN 978-1-4577-0582-3. doi: 10.1109/PST.2011.5971973. Short paper; full version online at
http://arxiv.org/abs/1009.5423.
[32] S. A. Mokhov, J. Paquet, and M. Debbabi. Reasoning about a simulated printer case investigation with
Forensic Lucid. In P. Gladyshev, editor, Proceedings of ICDF2C’11. Springer, Oct. 2011. To appear, online at
http://arxiv.org/abs/0906.5181.
[33] B. Moolenaar and Contributors. Vim the editor – Vi Improved. [online], 2009. http://www.vim.org/.
[34] NetBeans Community. NetBeans Integrated Development Environment. [online], 2004–2012.
http://www.netbeans.org.
[35] OpenESB Contributors. BPEL service engine. [online], 2009.
https://open-esb.dev.java.net/BPELSE.html.
[36] J. Paquet. Scientific Intensional Programming. PhD thesis, Department of Computer Science, Laval
University, Sainte-Foy, Canada, 1999.
[37] J. Paquet. 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, July 2009. IEEE Computer Society. ISBN 978-0-7695-3726-9.
[38] J. Paquet, S. A. Mokhov, and X. Tong. 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, July 2008. IEEE Computer Society. doi:
10.1109/COMPSAC.2008.200.
[39] M. Puckette and PD Community. Pure Data. [online], 2007–2012. http://puredata.org.
[40] G. Riley. CLIPS: A tool for building expert systems. [online], 2007–2011.
http://clipsrules.sourceforge.net/, last viewed May 2012.
[41] G. Shafer. The Mathematical Theory of Evidence. Princeton University Press, 1976.
[42] Sun Microsystems, Inc. NetBeans 6.7.1. [online], 2009–2010.
http://netbeans.org/downloads/6.7.1/index.html.
[43] P. Swoboda. A Formalisation and Implementation of Distributed Intensional Programming. PhD thesis, The
University of New South Wales, Sydney, Australia, 2004.
[44] P. Swoboda and J. Plaice. An active functional intensional database. In F. Galindo, editor, Advances in
Pervasive Computing, pages 56–65. Springer, 2004. LNCS 3180.
[45] P. Swoboda and J. Plaice. A new approach to distributed context-aware computing. In A. Ferscha,
H. Hoertner, and G. Kotsis, editors, Advances in Pervasive Computing. Austrian Computer Society, 2004.
ISBN 3-85403-176-9.
[46] P. Swoboda and W. W. Wadge. Vmake, ISE, and IRCS: General tools for the intensionalization of software
systems. In M. Gergatsoulis and P. Rondogiannis, editors, Intensional Programming II. World-Scientific, 2000.
[47] The GIPSY Research and Development Group. The General Intensional Programming System (GIPSY)
project. Department of Computer Science and Software Engineering, Concordia University, Montreal,
Canada, 2002–2012. http://newton.cs.concordia.ca/~gipsy/, last viewed April 2012.
[48] The PRISM Team. PRISM: a probabilistic model checker. [online], 2004–2012.
http://www.prismmodelchecker.org/, last viewed June 2010.
[49] X. Tong. Design and implementation of context calculus in the GIPSY. Master’s thesis, Department of
Computer Science and Software Engineering, Concordia University, Montreal, Canada, Apr. 2008.
[50] X. Tong, J. Paquet, and S. A. Mokhov. Complete context calculus design and implementation in GIPSY.
[online], 2007–2008. http://arxiv.org/abs/1002.4392.
[51] E. Vassev. ASSL: Autonomic System Specification Language – A Framework for Specification and Code
Generation of Autonomic Systems. LAP Lambert Academic Publishing, Nov. 2009. ISBN: 3-838-31383-6.
[52] E. Vassev and S. A. Mokhov. An ASSL-generated architecture for autonomic systems. In Proceedings of
C3S2E’09, pages 121–126, New York, NY, USA, May 2009. ACM. ISBN 978-1-60558-401-0. doi:
10.1145/1557626.1557645.
[53] E. Vassev and J. Paquet. Towards autonomic GIPSY. In Proceedings of the Fifth IEEE Workshop on
Engineering of Autonomic and Autonomous Systems (EASE 2008), pages 25–34. IEEE Computer Society,
2008. ISBN 978-0-7695-3140-3. doi: 10.1109/EASe.2008.9.
[54] E. I. Vassev. Towards a Framework for Specification and Code Generation of Autonomic Systems. PhD thesis,
Department of Computer Science and Software Engineering, Concordia University, Montreal, Canada, 2008.
[55] P. C. Vinh and J. P. Bowen. On the visual representation of configuration in reconfigurable computing.
Electron. Notes Theor. Comput. Sci., 109:3–15, 2004. ISSN 1571-0661. doi: 10.1016/j.entcs.2004.02.052.
[56] W. W. Wadge and E. A. Ashcroft. Lucid, the Dataflow Programming Language. Academic Press, London,
1985.
[57] K. Wan. Lucx: Lucid Enriched with Context. PhD thesis, Department of Computer Science and Software
Engineering, Concordia University, Montreal, Canada, 2006.
[58] K. Wan, V. Alagar, and J. Paquet. Lucx: Lucid enriched with context. In Proceedings of the 2005 International
Conference on Programming Languages and Compilers (PLC 2005), pages 48–14. CSREA Press, June 2005.
[59] A. Wu, J. Paquet, and S. A. Mokhov. Object-oriented intensional programming: Intensional Java/Lucid
classes. In Proceedings of SERA 2010, pages 158–167. IEEE Computer Society, 2010. ISBN
978-0-7695-4075-7. doi: 10.1109/SERA.2010.29. Online at: http://arxiv.org/abs/0909.0764.
[60] A. H. Wu. OO-IP Hybrid Language Design and a Framework Approach to the GIPC. PhD thesis, Department
of Computer Science and Software Engineering, Concordia University, Montreal, Canada, 2009.
[61] C. Zheng and J. R. Heath. Simulation and visualization of resource allocation, control, and load balancing
procedures for a multiprocessor architecture. In MS’06: Proceedings of the 17th IASTED international
conference on Modelling and simulation, pages 382–387, Anaheim, CA, USA, 2006. ACTA Press. ISBN
0-88986-592-2.
All items in Spectrum are protected by copyright, with all rights reserved. The use of items is governed by Spectrum's terms of access.

Repository Staff Only: item control page

Downloads per month over past year

Research related to the current document (at the CORE website)
- Research related to the current document (at the CORE website)
Back to top Back to top