Doi: 10.1145/1924421.1924444

Liability Issues in
Software Engineering

The use of formal methods to reduce legal uncertainties By Daniel Le Métayer, Manuel Maarek, Eduardo Mazza, Marie-Laure Potet, Stéphane Frénot, Valérie Viet Triem Tong, Nicolas Craipeau, and Ronan Hardouin

abstract

This paper reports on the results of a multidisciplinary project involving lawyers and computer scientists with the aim to put forward a set of methods and tools to ( 1) define software liability in a precise and unambiguous way and ( 2) establish such liability in case of incident. The overall approach taken in the project is presented through an electronic signature case study. The case study illustrates a situation where, in order to reduce legal uncertainties, the parties wish to include in the contract specific clauses to define as precisely as possible the share of liabilities between them for the main types of failures of the system.

1. intRoDuCtion

Software contracts usually include strong liability limitations or even exemptions of the providers for damages caused by their products. This situation does not favor the development of high-quality software because the software industry does not have sufficient economical incentives to apply stringent development and verification methods. Indeed, experience shows that products tend to be of higher quality and more secure when the actors in position to influence their development are also the actors bearing the liability for their defects. 1 The usual argument to justify this lack of liability is the fact that software products are too complex and versatile objects whose expected features (and potential defects) cannot be characterized precisely, and which therefore cannot be treated as traditional (tangible) goods. Admittedly, this argument is not without any ground: It is well known that defining in an unambiguous, comprehensive, and understandable way the expected behavior of systems integrating a variety of components is quite a challenge, not to mention the use of such definition as a basis for a liability agreement. Taking up this challenge is precisely our objective: Our aim is to study liability issues both from the legal and technical points of view and to put forward a formal framework to ( 1) define liability in a precise and unambiguous way and ( 2) establish such liability in case of incident. Note that we focus on liabilities for software flaws here and do not consider infringement or any other intellectual property right liabilities which involve very different issues.

Obviously, specifying all liabilities in a formal frame-
work is neither possible nor desirable. Usually, the parties
wish to express as precisely as possible certain aspects
which are of prime importance for them and prefer to
state other aspects less precisely (either because it is
impossible to foresee at contracting time all the events
that may occur or because they do not want to be bound
by too precise commitments). Taking this requirement
into account, we provide a set of tools and methods to be
used on a need basis in the contract drafting process (as
opposed to a monolithic, “all or nothing” approach). Our
model is based on execution traces which are abstrac-
tions of the log files of the system. In a nutshell, liability is
specified as a function taking as parameters a claim and
an execution trace and returning a set of “responsible”
actors. This set of actors (ideally a singleton) depends
on the claim and the errors occurring in the trace. Both
errors and claims are expressed as trace properties. The
liability function can be made as precise or detailed as
necessary by choosing the claims and errors relevant for
a given situation.

2. staRtinG Point

Let us consider an electronic signature system allowing an e-commerce company (ECC) to send a document to be signed by an individual on his mobile phone. The signature of the document is subject to the individual’s approval (and authentication) and all communications and signature operations are performed through his mobile phone. In a real situation, the activation of the signature system would be preceded by a request from the individual or by a negotiation with the ECC, but we do not consider this negotiation phase here.

The mobile phone itself incorporates a smart card (for
the verification of the Personal Identification Number
This paper presents the results of the LISE (Liability Issues
in Software Engineering) project funded by ANR (Agence
Nationale de la Recherche) under grant ANR-07-SESU-
007. A previous version of this paper was published in the
Proceedings of the 32nd ACM/IEEE International Conference
on Software Engineering, ICSE 2010.