A Formal Framework for specifying and Analyzing Liabilities Using Log as Digital Evidence
type: Dataset
contact point: Organization
  fn: CCSD
keyword: logs
keyword: infoinfo-secomputer-science-cssoftware-engineering-csse
keyword: infoeu-reposemanticsdoctoralthesis
keyword: responsabilite-pour-les-defaillances-logicielles
keyword: software-liability
keyword: formal-specification
keyword: methodes-formelles
keyword: theses
landing page: https://theses.hal.science/tel-00800516
description: 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 and one must admit that even critical systems are not immune from that type of errors. One of the reasons for this situation is that software requirements are generally hard to elicit precisely and it is often impossible to predict all the contexts in which software products will actually be used. Considering the interests at stake, it is therefore of prime importance to be able to establish liabilities when damages are caused by software errors. Essential requirements to define these liabilities are (1) the availability of reliable evidence, (2) a clear definition of the expected behaviors of the components of the system and (3) the agreement between the parties with respect to liabilities. In this thesis, we address these problems and 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.
issued: 2026-05-12T18:55:03.187782
language: en
modified: 2026-05-12T18:55:03.187787

test_moissonnage_selune
type: Agent

A Formal Framework for specifying and Analyzing Liabilities Using Log as Digital Evidence
type: Distribution
access URL: https://theses.hal.science/tel-00800516
format: HTML
issued: 2026-05-12T18:55:03.196320
modified: 2026-05-12T18:55:03.163519