Mokhov, Serguei A., Paquet, Joey and Debbabi, Mourad (2011) Reasoning About a Simulated Printer Case Investigation with Forensic Lucid. In: International ICST Conference on Digital Forensics & Cyber Crime (ICDF2C), October 2011, Dublin, Ireland. (In Press)
Preview |
Text (Expanded version after camera-ready submission) (application/pdf)
344kBflucid-printer-case-arXiv.pdf - Updated Version |
Preview |
Text (Updated) (application/pdf)
589kBflucid-printer-case-presentation.pdf - Presentation |
Abstract
In this work we model the ACME (a fictitious company name) "printer case incident" and make its specification in Forensic Lucid, a Lucid- and intensional-logic-based programming language for cyberforensic analysis and event reconstruction specification. The printer case involves a dispute between two parties that was previously solved using the finite-state automata (FSA) approach, and is now re-done in a more usable way in Forensic Lucid. Our simulation is based on the said case modeling by encoding concepts like evidence and the related witness accounts as an evidential statement context in a Forensic Lucid program, which is an input to the transition function that models the possible deductions in the case. We then invoke the transition function (actually its reverse) with the evidential statement context to see if the evidence we encoded agrees with one's claims and then attempt to reconstruct the sequence of events that may explain the claim or disprove it.
| 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 (Paper) |
| Refereed: | Yes |
| Authors: | Mokhov, Serguei A. and Paquet, Joey and Debbabi, Mourad |
| Date: | October 2011 |
| Projects: |
|
| Funders: |
|
| Keywords: | cybercrime investigation modeling, intensional logic and programming, cyberforensics, Forensic Lucid, finite-state automata |
| ID Code: | 973949 |
| Deposited By: | Serguei Mokhov |
| Deposited On: | 30 Apr 2012 15:12 |
| Last Modified: | 18 Jan 2018 17:37 |
| Related URLs: |
References:
[1] E. A. Ashcroft, A. A. Faustini, R. Jagannathan, and W. W. Wadge. Multidimensional Programming. Oxford University Press, London, Feb. 1995. ISBN: 978-0195075977.[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.
[5] 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.
[6] P. Gladyshev. Finite state machine analysis of a blackmail investigation. International Journal of Digital Evidence, 4(1), 2005.
[7] P. Gladyshev and A. Patel. Finite state machine approach to digital event reconstruction. Digital Investigation Journal, 2(1), 2004.
[8] 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.
[9] 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.
[10] R. Lalement. Computation as Logic. Prentice Hall, 1993. C.A.R. Hoare Series Editor. English translation from French by John Plaice.
[11] 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.
[12] 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.
[13] S. A. Mokhov. Encoding forensic multimedia evidence from MARF applications as Forensic Lucid expressions. In T. Sobh, K. Elleithy, and A. Mahmood, editors, Novel Algorithms and Techniques in Telecommunications and Networking, proceedings of CISSE’08, pages 413–416, University of Bridgeport, CT, USA, Dec. 2008. Springer. Printed in January 2010.
[14] 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.
[15] S. A. Mokhov. Enhancing the formal cyberforensic approach with observation modeling with credibility factors and mathematical theory of evidence [online], also in ;login: vol. 34, no. 6, p. 101, Dec. 2009. Presented at WIPS at USENIX Security’09, http://www.usenix.org/events/sec09/wips.html.
[16] S. A. Mokhov. The role of self-forensics modeling for vehicle crash investigations and event reconstruction simulation. In J. S. Gauthier, editor, Proceedings of the Huntsville Simulation Conference (HSC’09), pages 342–349. SCS, Oct. 2009. Online at http://arxiv.org/abs/0905.2449.
[17] 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.
[18] S. A. Mokhov, J. Paquet, and M. Debbabi. Formally specifying operational semantics and language constructs of Forensic Lucid. In O. Goebel, S. Frings, D. Gunther, J. Nedon, and D. Schadt, editors, Proceedings of the IT Incident Management and IT Forensics (IMF’08), LNI140, pages 197–216. GI, Sept. 2008.
[19] 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. Online at http://arxiv.org/abs/0906.0049.
[20] 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. Short paper; full version online at http://arxiv.org/abs/1009.5423.
[21] J. Paquet. Scientific Intensional Programming. PhD thesis, Department of Computer Science, Laval University, Sainte-Foy, Canada, 1999.
[22] 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.
[23] 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.
[24] J. Paquet, S. A. Mokhov, E. I. Vassev, X. Tong, Y. Ji, A. H. Pourteymour, K. Wan, A. Wu, S. Rabah, B. Han, B. Lu, L. Tao, Y. Ding, C. L. Ren, and 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.
[25] J. Paquet and A. H. Wu. 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, June 2005.
[26] J. Plaice, B. Mancilla, G. Ditu, and W. W. Wadge. Sequential demand-driven evaluation of eager TransLucid. In Proceedings of the 32nd Annual IEEE International Computer Software and Applications Conference (COMPSAC), pages 1266–1271, Turku, Finland, July 2008. IEEE Computer Society.
[27] T. Rahilly and J. Plaice. A multithreaded implementation for TransLucid. In Proceedings of the 32nd Annual IEEE International Computer Software and Applications Conference (COMPSAC), pages 1272–1277, Turku, Finland, July 2008. IEEE Computer Society.
[28] G. Riley. CLIPS: A tool for building expert systems [online], 2007–2009. http://clipsrules.sourceforge.net/, last viewed: October 2009.
[29] 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.
[30] W. W. Wadge and E. A. Ashcroft. Lucid, the Dataflow Programming Language. Academic Press, London, 1985.
[31] K. Wan. Lucx: Lucid Enriched with Context. PhD thesis, Department of Computer Science and Software Engineering, Concordia University, Montreal, Canada, 2006.
[32] 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.
[33] 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. Online at: http://arxiv.org/abs/0909.0764.
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
Download Statistics
Download Statistics