More Web Proxy on the site http://driver.im/

Article

A formal framework for specifying and analyzing logs as electronic evidence

Authors:

Marie-Laure Potet,

Daniel Le MétayerAuthors Info & Claims

SBMF'10: Proceedings of the 13th Brazilian conference on Formal methods: foundations and applications

Pages 194 - 209

Published: 08 November 2010 Publication History

Abstract

The issues of logging for determining liability requires to define, prior to a dispute, the logging system and the log analysis in a manner that would determine the parties liable for a predetermined misbehavior of the system. We propose a formal framework for specifying and reasoning about decentralized logs to be used in legal disputes. In addition, we study how previous results can be used in the incremental analysis of larger inputs to obtain precise or approximated results. We illustrate our approach with an example of a travel arrangement service.

References

[1]

Abrial, J.: The B-Book. Cambridge University Press, Cambridge (1996)

[2]

Badeau, F., Amelot, A.: Using B as a High Level Programming Language in an Industrial Project: Roissy VAL. In: Treharne, H., King, S., Henson, M.C., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 334-354. Springer, Heidelberg (2005)

Digital Library

[3]

Barringer, H., Groce, A., Havelund, K., Smith, M.H.: An Entry Point for Formal Methods: Specification and Analysis of Event Logs. CoRR abs/1003.1682 (2010)

[4]

Barringer, H., Groce, A., Havelund, K., Smith, M.H.: Formal Analysis of Log Files. Aerospace Computing, Information, and Communication (to appear, 2010)

[5]

Behm, P., Benoit, P., Faivre, A., Meynadier, J.-M.: Meteor: A Successful Application of B in a Large Project. In: Woodcock, J.C.P., Davies, J. (eds.) FM 1999. LNCS, vol. 1708, pp. 369-387. Springer, Heidelberg (1999)

Digital Library

[6]

Buskirk, E.V., Liu, V.T.: Digital Evidence: Challenging the Presumption of Reliability. Journal of Digital Forensic Practice 1(1), 19-26 (2006)

[7]

Cederquist, J.G., Corin, R., Dekker, M.A.C., Etalle, S., den Hartog, J.I., Lenzini, G.: Audit-based Compliance Control. International Journal of Information Security 6(2-3), 133-151 (2007)

Digital Library

[8]

Farrell, A.D.H., Sergot, M.J., Salle, M., Bartolini, C.: Using the Event Calculus for Tracking the Normative State of Contracts. International Journal of Cooperative Information Systems (IJCIS) 14(2-3), 99-129 (2005)

[9]

Fenech, S., Pace, G.J., Schneider, G.: CLAN: A tool for contract analysis and conflict discovery. In: Liu, Z., Ravn, A.P. (eds.) ATVA 2009. LNCS, vol. 5799, pp. 90-96. Springer, Heidelberg (2009)

Digital Library

[10]

Grossi, D., Royakkers, L.M.M., Dignum, F.: Organizational Structure and Responsibility. Artificial Intelligence and Law 15(3), 223-249 (2007)

Digital Library

[11]

Hallal, H., Boroday, S., Petrenko, A., Ulrich, A.: A Formal Approach to Property Testing in Causally Consistent Distributed Traces. Formal Aspects of Computing 18(1), 63-83 (2006)

[12]

Insa, F.: The Admissibility of Electronic Evidence in Court (AEEC): Fighting against High-Tech Crime - Results of a European Study. Journal of Digital Forensic Practice 1(4), 285-289 (2006)

[13]

Kyas, M., Prisacariu, C., Schneider, G.: Run-Time Monitoring of Electronic Contracts. In: Cha, S(S.), Choi, J.-Y., Kim, M., Lee, I., Viswanathan, M. (eds.) ATVA 2008. LNCS, vol. 5311, pp. 397-407. Springer, Heidelberg (2008)

Digital Library

[14]

Lamport, L.: Time, Clocks, and the Ordering of Events in a Distributed System. Communications of the ACM 21(7), 558-565 (1978)

Digital Library

[15]

Le Metayer, D., Maarek, M., Mazza, E., Potet, M.L., Viet Triem Tong, V., Craipeau, N., Frenot, S., Hardouin, R.: Liability in Software Engineering: Overview of the LISE Approach and Illustration on a Case Study. In: International Conference on Software Engineering (ICSE), pp. 135-144 (2010)

Digital Library

[16]

Le Metayer, D., Mazza, E., Potet, M.L.: Designing Log Architecture For Legal Evidence. In: Software Engineering And Formal Methods (SEFM). IEEE, Los Alamitos (2010)

Digital Library

[17]

Lima, T.D., Royakkers, L.M.M., Dignum, F.: A Logic For Reasoning About Responsibility. Logic Journal of the IGPL 18(1), 99-117 (2010)

[18]

Maurer, U.M.: New Approaches to Digital Evidence. Proceedings of the IEEE 92(6), 933-947 (2004)

[19]

Peisert, S., Bishop, M., Karin, S., Marzullo, K.: Toward Models for Forensic Analysis. In: Systematic Approaches to Digital Forensic Engineering, pp. 3-15. IEEE, Los Alamitos (2007)

Digital Library

[20]

Rekhis, S., Krichene, J., Boudriga, N.: Cognitive-Maps Based Investigation of Digital Security Incidents. In: Systematic Approaches to Digital Forensic Engineering, pp. 25-40 (2008)

Digital Library

[21]

Saleh, M., Arasteh, A.R., Sakha, A., Debbabi, M.: Forensic Analysis of Logs: Modeling and verification. Knowledge-Based Systems 20(7), 671-682 (2007)

Digital Library

[22]

Sandler, D., Derr, K., Crosby, S.A., Wallach, D.S.: Finding the Evidence in Tamper-Evident Logs. In: Systematic Approaches to Digital Forensic Engineering, pp. 69-75 (2008)

Digital Library

[23]

Schneider, F.B.: Accountability for Perfection. IEEE Security & Privacy 7(2), 3-4 (2009)

Digital Library

[24]

Schneier, B., Kelsey, J.: Secure audit logs to support computer forensics. ACM Transactions on Information and System Security 2(2), 159-176 (1999)

Digital Library

[25]

Skene, J., Raimondi, F., Emmerich, W.: Service-Level Agreements for Electronic Services. IEEE Transactions on Software Engineering 36(2), 288-304 (2010)

Digital Library

[26]

Stirewalt, R.E.K., Dillon, L.K., Kraemer, E.: The Inference Validity Problem in Legal Discovery. In: International Conference on Software Engineering (ICSE), pp. 303-306. IEEE, Los Alamitos (2009)

[27]

Waters, B.R., Balfanz, D., Durfee, G., Smetters, D.K.: Building an Encrypted and Searchable Audit Log. In: Proceedings of the Network and Distributed System Security. The Internet Society (2004)

Cited By

Le Métayer D(2011)Formal methods as a link between software code and legal rulesProceedings of the 9th international conference on Software engineering and formal methods10.5555/2075679.2075682(3-18)Online publication date: 14-Nov-2011
https://dl.acm.org/doi/10.5555/2075679.2075682
Le Métayer DMaarek MMazza EPotet MFrénot STong VCraipeau NHardouin R(2011)Liability issues in software engineeringCommunications of the ACM10.1145/1924421.192444454:4(99-106)Online publication date: 1-Apr-2011
https://dl.acm.org/doi/10.1145/1924421.1924444

Recommendations

A Formal Framework for ASTRAL Intralevel Proof Obligations

ASTRAL is a formal specification language for real-time systems. It is intended to support formal software development, and therefore has been formally defined. This paper focuses on how to formally prove the mathematical correctness of ASTRAL ...
Specifying and analyzing security automata using CSP-OZ
ASIACCS '07: Proceedings of the 2nd ACM symposium on Information, computer and communications security

Security automata are a variant of Büchi automata used to specify security policies that can be enforced by monitoring system execution. In this paper, we propose using CSP-OZ, a specification language combining Communicating Sequential Processes (CSP) ...
Specifying and analyzing early requirements in Tropos

We present a framework that supports the formal verification of early requirements specifications. The framework is based on Formal Tropos, a specification language that adopts primitive concepts for modeling early requirements (such as actor, goal, and ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

SBMF'10: Proceedings of the 13th Brazilian conference on Formal methods: foundations and applications

November 2010

290 pages

ISBN:9783642198281

Editors:
Jim Davies
Oxford University, Department of Computer Science, Oxford, UK
,
Leila Silva
Universidade Federal de Sergipe, Departamento de Ciência da Computação e Estatística, Aracaju, SE, Brazil
,
Adenilso Simao
Avenida Trabalhador São-Carlense, São Carlos, SP, Brazil

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 08 November 2010

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 31 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Le Métayer D(2011)Formal methods as a link between software code and legal rulesProceedings of the 9th international conference on Software engineering and formal methods10.5555/2075679.2075682(3-18)Online publication date: 14-Nov-2011
https://dl.acm.org/doi/10.5555/2075679.2075682
Le Métayer DMaarek MMazza EPotet MFrénot STong VCraipeau NHardouin R(2011)Liability issues in software engineeringCommunications of the ACM10.1145/1924421.192444454:4(99-106)Online publication date: 1-Apr-2011
https://dl.acm.org/doi/10.1145/1924421.1924444

View Options

View options

Media

Figures

Other

Tables

View Table of Contents