CTL
26 June 2012 - 10h30
A Formal Framework for Specifying and Analyzing Liabilities Using Log as Digital Evidence (Phd Defense)
by Eduardo Mazza from Verimag
Abstract: Despite the effort made to define methods for the design of high quality software, experience shows that failures of IT systems due to software errors remain very common. Considering the interests at stake, it is therefore of prime importance to be able to establish liabilities when damages are caused by software errors. In this thesis, we propose a formal framework to precisely specify and establish liabilities in a software contract. This framework can be used to assist the parties both in the drafting phase of the contract and in the definition of the architecture to collect evidence. Our first contribution is a method for the integration of a formal definition of digital evidence and liabilities in a legal contract. Digital evidence is based on distributed execution logs produced by \\\acceptable log architectures\\\. The notion of acceptability relies on a formal threat model based on the set of potential claims. Another main contribution is the definition of an incremental procedure, which is implemented in the LAPRO tool, for the analysis of distributed logs.
Jury:
Regine Laleau Université Paris-Est Créteil Lyon Rapporteur
Gerardo Schneider University of Gothenburg Rapporteur
Guillaume Dufay Trusted Labs Examinateur
Jean-Marc Jézéquel IRISA Examinateur
Roland Groz Grenoble INP Examinateur
Marie-Laure Potet Grenoble INP Directeur de thèse
Daniel Le Métayer INRIA Directeur de thèse
