To conclude, we should stress that the methods and
tools provided by our framework can be applied in an
incremental way, depending on the wishes of the parties,
the economic stakes, and the timing constraints for drafting the contract.
1. The first level of application is a systematic (but
informal) definition of liabilities in the style of
Section 2. 3.
2. The second level is the formal definition of liabilities
as presented in Section 3. 3. This formal definition
itself can be more or less detailed and encompass only
a part of the liability rules defined informally. In
addition, it does not require a complete specification
of the software but only the properties relevant for the
targeted liability rules.
3. The third level is the implementation of a log infrastructure or the enhancement of existing logging facilities to ensure that all the information required to
establish liabilities will be available if a claim is raised.
An example of implementation of our framework is
described in Le Métayer et al.,
12 which defines a log
architecture for OSGi.
4. The fourth level is the implementation of a log analyzer to assist human experts in the otherwise tedious
and error-prone log inspection.
5. A fifth level would be the verification of the correctness
of the log analyzer with respect to the formal definition
of liabilities (considering the correspondence between
log files and traces). This level would bring an
additional guarantee about the validity of the results
produced by the system.
Each of these levels contributes to reducing further the uncertainties with respect to liabilities and the
parties can decide to choose the level commensurate with
the risks involved with the potential failures of the system.
Last but not least, we are currently working on two
other key issues related to log files which have not been
discussed here: their optimization in terms of storage
(compaction, retention delay, etc.) using an index-based
factorization method and techniques to ensure their
authenticity and integrity17, 23 including trusted serialization of log items.
We would like to thank all the members of the LISE project,
who have, through many discussions and exchanges, contributed to the work described here, in particular Christophe
Alleaume, Valérie-Laure Benabou, Denis Beras, Christophe
Bidan, Gregor Goessler, Julien Le Clainche, Ludovic Mé, and
3. avizienis, a., laprie, J.-c., randell,
b. Fundamental concepts of
computer system dependability.
In IARP/IEEE-RAS Workshop on
robot dependability: technological
challenges of dependable robots in
human environments (2001).
4. berry, d.M. appliances and software:
the importance of the buyer's
warranty and the developer's
liability in promoting the use of
systematic quality assurance and
formal methods. In Proceedings
of the Workshop on Modeling
Software System Structures in
a Fastly Moving Scenario (santa
Margherita ligure, Italy, 2000);
5. brandan-briones, l., lazovik, a.,
dague, P. optimal observability for
diagnosability. In International
Workshop on Principles of Diagnosis
6. Farrell, a.d.h., sergot, M.J., sallé, M.,
bartolini, c. using the event
calculus for tracking the normative
state of contracts. Int. J. Coop.
Inform. Sys. (IJCIS) 14, 2–3
7. Gladyshev, P. enbacka, a. rigorous
development of automated
inconsistency checks for digital
evidence using the b method. Int.
J. Dig. Evidence (IJDE) 6, 2 (2007),
8. Goessler, G., raclet, J.-b., le
Métayer, d. causality analysis in
contract violation. In International
Conference on Runtime Verification
(RV 2010), lncs 6418 (2010),
9. Governatori, G., Milosevic, Z., sadiq,
s.w. compliance checking
between business processes and
business contracts. In EDOC.
Ieee computer society (2006),
10. Jones, a.k., sielken, r.s. Computer
System Intrusion Detection:
A Survey, tr, university of Virginia
computer science department,
11. le Métayer, d. a formal privacy
management framework. In Formal
Aspects of Security and Trust (FAST),
springer Verlag, lncs 5491 (2009),
12. le Métayer, d., Maarek, M., Mazza,
e., Potet, M.-l., Frénot, s., Viet triem
tong, V., craipeau, n., hardouin, r.
liability in software engineering—
overview of the lIse approach
and illustration on a case study. In
International Conference on
Volume 1. acM/Ieee (2010),
13. le Métayer, d, Mazza, e, Potet, M.-l.
designing log architectures for legal
evidence. In International Conference
on Software Engineering and Formal
Methods (SEFM 2010). Ieee (2010),
14. lipovetsky, s. les clauses limitatives
de responsabilité et de garantie dans
les contrats informatiques.
approche comparative France/
États-unis. Quelles limitations.
Expertises des systèmes
d’information, n° 237 (May 2000),
15. Mazza, e, Potet, M.-l., le Métayer, d.
a formal framework for specifying
and analyzing logs as electronic
evidence. In Brazilian Symposium on
Formal Methods (SBMF 2010)
16. Papadopoulos, y. Model-based system
monitoring and diagnosis of failures
using statecharts and fault trees.
Reliab. Eng. Syst. Safety 81 (2003),
17. Parrend, P. Frénot, s. security
benchmarks of osGi platforms:
toward hardened osGi.
Softw.– Prac. Exp. (SPE) 39, 5 (2009),
18. Peyton Jones, s.l., eber, J.-M.
how to write a financial contract.
In The Fun of Programming,
cornerstones of computing, chapter
19. Prisacariu, c., schneider, G. a formal
language for electronic contracts.
In FMOODS, springer, lncs 4468
20. rekhis, s., boudriga, n. a temporal
logic-based model for forensic
investigation in networked system
security. Comput. Netw. Security 3685
21. ryan, d.J. two views on security
vand software liability. let the
legal system decide. IEEE
Security Privacy (January–February
22. schneider, F.b. accountability for
perfection. IEEE Security Privacy
23. schneier, b., kelsey, J. secure
audit logs to support computer
forensics. ACM Trans. Inform.
Syst. Security (TISSEC) 2, 2 (1999),
24. skene, J., lamanna, d.d., emmerich,
w. Precise service level agreements.
In ACM/IEEE International
Conference on Software Engineering
(ICSE), Ieee (2004), 179–188.
25. skene, J., raimondi, F., emmerich, w.
service-level agreements for
electronic services. IEEE Tran.
Software Eng. ( TSE) 36, 2 (2010),
26. skene, J., skene, a., crampton, J.,
emmerich, w. the monitorability
of service-level agreements for
application-service provision. In
International Workshop on Software
and Performance ( WOSP), acM
27. solon, M., harper, P. Preparing
evidence for court. Digit. Invest. 1
28. stephenson, P. Modeling of post-incident root cause analysis. Digit.
Evidence 2, 2 (2003).
Daniel Le Métayer and Manuel Maarek,
InrIa, Grenoble rhône-alpes, France.
Eduardo Mazza and Marie-Laure Potet,
VerIMaG, university of Grenoble, France.
Stéphane Frénot, InrIa, Grenoble
rhône-alpes, and Insa, lyon, France.
Valérie Viet Triem Tong, ssIr, supélec
nicolas Craipeau, PrInt, university of
Ronan hardouin, dante, university of
Versailles, saint-Quentin, France.
1. anderson, r., Moore, t. Information
security economics—and beyond.
Information security summit (Is2)
2. arasteh, a.r., debbabi, M., sakha,
a., saleh, M. analyzing multiple logs
for forensic evidence. Dig. Invest. 4
© 2011 acM 0001-0782/11/04 $10.00