A Formal Framework for Specifying and Analyzing Logs as Electronic Evidence - Formal Methods: Foundations and Applications - page 194

A Formal Framework for Specifying and
Analyzing Logs as Electronic Evidence

Eduardo Mazza 1 , Marie-Laure Potet 1 , and Daniel Le Métayer 2

1 Verimag, Centre Équation, 2 avenue de Vignate, F-38610 Gières
{Eduardo.Mazza,Marie-Laure.Potet}@imag.fr
2 LICIT, INRIA Grenoble Rhône-Alpes
[e-mail]

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.

1 Introduction

Due to the growing impact of the Information and Communication Technologies
on everyday life, and the increasing complexity of computer systems, the logging
of these systems raises greater challenges. Logging is a necessity for debugging
a system at development time, or after a fault, for identifying security attacks,
guaranteeing safety, and establishing liability for software providers. With re-
spect to the last one, Fred B. Schneider pointed [23] that liability determination
needs a mature discipline of forensics for computing systems and components.
It requires to change software development practices, because, in addition to
delivering systems, producers will also need to deliver instruments to show that
they behave well.
The use of log as electronic evidence for establishing contractual liability is
a challenging problem [18, 6, 12]. Actual solutions that propose formal models
to specify liability [17, 10] are more focused on the system models rather than
using logs as electronic evidences in cases of litigation. Meanwhile, other works
[4, 11, 21, 3] present a well-defined model for analysing properties in logs, but
a small effort has been made to specify the liability associated with the log
content. Existing research stops short of discussing how one might determining
whether the information found in a given log is precise enough to be used for
legal disputes.
The LISE project 1 aims to address liability issues from the legal and technical
points of view. The goal is to cover the whole chain of “liability engineering”, from

1 Liability Issues in Software Engineering: http://licit.inrialpes.fr/lise/