ACM通信
软件工程中的责任问题:使用形式方法减少法律不确定性
来源:iStockPhoto.com
本文报告了一项涉及律师和计算机科学家的多学科项目的结果，旨在提出一套方法和工具(1)以精确和明确的方式定义软件责任和(2)在发生事故时确定此类责任。通过一个电子签名案例研究，介绍了该项目所采用的整体方法。该案例研究说明了这样一种情况:为了减少法律上的不确定性，订约双方希望在合同中列入具体条款，以便尽可能精确地界定他们之间对系统的主要故障类型承担的责任份额。
1.简介
软件合同通常包括强烈的责任限制，甚至对供应商的产品造成的损害给予豁免。这种情况不利于高质量软件的开发，因为软件行业没有足够的经济激励来应用严格的开发和验证方法。的确，经验表明，如果能够影响产品开发的行为者同时也是对产品缺陷承担责任的行为者，那么产品往往质量更高，也更安全。1通常证明这种责任缺失的理由是这样一个事实:软件产品是过于复杂和通用的对象，其预期的特性(和潜在的缺陷)无法被精确地描述，因此不能被视为传统的(有形的)产品。诚然，这一论点不是没有任何根据的:众所周知，以一种明确的、全面的和可以理解的方式定义集成各种组件的系统的预期行为是一个相当大的挑战，更不用说使用这样的定义作为责任协议的基础。接受这一挑战正是我们的目标:我们的目标是从法律和技术的角度研究责任问题，并提出一个正式的框架，以(1)以精确和明确的方式定义责任，(2)在事件发生时确立这种责任。请注意，我们这里关注的是软件缺陷的责任，而不考虑侵权或任何其他知识产权责任，这涉及到非常不同的问题。
显然，在一个正式的框架中指定所有的负债既不可能也不可取。通常，订约双方希望尽可能准确地表达对他们极为重要的某些方面，而宁愿不那么精确地陈述其他方面(要么是因为在订立合同时不可能预见可能发生的所有事件，要么是因为他们不希望受到过于精确的承诺的约束)。考虑到这一要求，我们提供了一套工具和方法，以便在合同起草过程中根据需要使用(而不是单一的“全有或全无”方法)。我们的模型基于执行轨迹，它是系统日志文件的抽象。简而言之，责任被指定为以声明和执行跟踪为参数并返回一组“负责任的”参与者的函数。这组参与者(理想情况下是单例)依赖于声明和跟踪中发生的错误。错误和声明都表示为跟踪属性。通过选择与特定情况相关的索赔和错误，可以使责任函数尽可能精确或详细。
本文的介绍基于一个案例研究:一个安装在手机上的电子签名应用程序。第2节描述了起点(受协议约束的IT系统、涉及的各方、各方之间的非正式协议和法律上下文);第3节介绍负债定义的正式框架。第4节提供了相关工作的草图，第5节确定了进一步研究的途径。
2.起点
让我们考虑一个电子签署系统，让电子贸易公司(环保会)发送一份文件，让个人用流动电话签署。文件的签字需要个人的批准(和认证)，所有的通信和签字操作都是通过他的手机进行的。在实际情况中，签名系统的激活会在个人请求或与ECC进行协商之前进行，但我们在这里不考虑这个协商阶段。
流动电话本身设有智能卡(用以核实使用者的个人识别号码)及签名应用程序。我们假设移动电话提供商(MPP)、签名应用程序提供商(SAP)和智能卡提供商(SCP)想要执行一项协议，将这样的移动电话签名解决方案推向市场。为了减少法律上的不确定性，当事各方希望在协定中列入具体规定，以尽可能精确地界定他们之间对系统的主要故障类型承担的责任份额。它们的意图是利用这些规定，通过适用明确规定的规则，以友好的方式解决责任问题。在这个阶段，可能所有组件(软件和硬件)都已经可用，剩下的唯一任务就是它们的集成。也可能是一些或所有组件仍然需要开发。一般来说，不能假设软件组件可以以特定的方式设计或修改，从而使负债的实现更容易。在这个阶段所做的唯一假设是:
- 在技术方面:系统功能体系结构的可用性(组件的接口和预期行为的非正式定义)
- 在业务方面:双方就债务份额达成的非正式协议
本文所述基础设施的目标是允许双方将这一非正式协议转化为一份在法律意义上有效且尽可能精确的合同，特别是在技术问题方面，以最大限度地减少法律上的不确定性。在本节的其余部分中，我们描述了最初的技术和法律情况:IT系统本身(章节2.1)，涉及的参与者(章节2.2)，签署协议的双方之间的非正式协议(章节2.3)，以及围绕协议的法律上下文(章节2.4)。
2.1.IT系统
在契约阶段的开始，IT系统通常以一种非正式的方式由它的体系结构定义:它的组件、它们的接口、预期的行为和交互。在我们的案例研究中，我们假设电子签名系统由以下组件组成:
- 一个服务器(服务公司）
- 签名申请(SigApp）
- 智能卡(卡）
- 流动输入/输出(IO)组件，收集手机的键盘和显示器(包括其驱动程序)
- 操作系统(OpSys）
所有的组件，除了服务公司都嵌在手机里。在本文中，我们关注与手机系统相关的负债，而不考虑与服务公司或者通讯网络。这些责任可以通过增加ECC和电信运营商作为附加方，以同样的方式处理。唯一的功能OpSys我们在这里考虑的是它在移动电话组件之间(即，在移动电话组件之间)的所有通信中所扮演的媒介角色SigApp,卡,IO）.
系统的架构及其信息流如图所示图1．协议从ECC开始ECC要求签署文件D(消息1)文档由服务公司而且SigApp，并向该手机的主人出示(自己的)IO(消息2、3和4)自己的拒绝签署,ECC通知是通过IO, SigApp,服务公司(消息5-n、6-n、7-n和8-n)。如果自己的的文件及输入的个人识别码自己的被转发卡通过SigApp(消息5-y、6-y和7-y)。其次，取决于是否卡是否验证PIN码，文件和签名产生的卡被发送到ECC通过SigApp而且服务公司(消息8-y-r、9-y-r和10-y-r)，或者ECC通知通过SigApp而且服务公司认证失败的消息(消息8-y-w、9-y-w和10-y-w)。请注意，这个场景是一个真实协议的简化版本，这足以说明我们的目的:例如，在一个真实的系统中，由于安全原因，PIN码不会被清楚地发送，它将通过哈希编码提供。
2.2.演员
我们假设该合同由制造和销售签名解决方案的三方签订:
- 流动电话供应商(MPP）
- 签署应用程序提供者(SAP）
- 智能卡供应商(SCP）
手机的主人(自己的)和ECC应该与谁执行不同的合同MPP其中也扮演着手机运营商的角色。我们只关心B2B之间的合同MPP, SAP,SCP在这里。我们回到2.4节的法律后果，包括手机的所有者(自己的)。在续集中，我们将使用“party”这个词MPP, SAP,SCP，以及“用户”一词代表系统的最终用户(ECC而且自己的）.
系统中的每个组件都由其中一方提供。在我们的例子中，我们假设:
- 的SigApp组件由SAP。
- 的卡组件由SCP。
- 的IO而且OpSys组件由边际产量。
2.3.非正式协议
双方希望尽可能精确地确定在向移动电话所有者提出索赔时他们之间的责任份额。在实践中，索赔的对象通常是MPP因为MPP是唯一与手机拥有人有直接接触(以及合约关系)的一方(既是MPP也是运营商)。MPP将必须赔偿手机的所有者，如果他的索赔是有效的，并可能反过来由一个(或几个)的其他方赔偿，这取决于索赔的类型，可用的日志文件，以及协议中定义的责任份额。
在下面的文章中，我们假设每个要签署的文件最初都是由ECC并且这个戳记(i)是唯一的，(ii)总是包含在给定会话的消息中，并且(iii)从不修改。这个戳记可以看作是一个事务号，它使区分属于不同签名会话的消息变得更加容易。取消或放松这种假设是可能的，但代价是建立一个更复杂的模型。
作为一个例子，我们考虑两种来自手机所有者的索赔，称为DiffDoc而且NotSigned，涉及签署一份所谓的文件D盖章:
- DiffDoc:原告自己的声称他收到了一份文件D与所谓的文件盖上不同的邮戳D(盖章)。例如，在采购订单中，D而且D’可能会因订购物品的数量或价格而有所不同。
- NotSigned:原告自己的声称他从未收到过任何盖章的文件。
我们假设双方就这两类索赔的以下非正式责任份额达成一致:
- 如果自己的声称他收到了一份文件D与所谓的文件盖上不同的邮戳D(盖章)，那么，如果此声明有效
- 一个。SAP如有责任SigApp已经转发给自己的与收到的文件不同(盖章)的文件ECC。
- b。否则MPP应当承担责任。
- a.如果智能卡错误地验证了文件的密码D盖章,然后SCP应当承担责任。
- b。否则MPP应当承担责任。
我们在这里不讨论这个非正式协议的价值或理由，只是把它作为一个可能分担责任的例子。应该清楚的是，这部分责任是双方基于技术、商业和法律论据进行谈判的结果，它不必(通常也不能)得到正式的证明。例如，上述关于违约责任的规则可能被认为是可以接受的MPP因为他以承担与客户有关的风险为代价，拿走了企业收入的很大一部分。问题的关键是，正式框架不应对债务的份额施加任何不适当的限制，而应提供各方尽可能准确地表达其愿望的手段。
2.4.法律环境
尽管当事人的意图是根据明确规定的规则以友好的方式解决责任问题，但显然有必要考虑到计算机系统的法律背景。对法律约束的任何误解或忽视都可能导致合同条款在法庭上无效，从而增加而不是减少法律风险。这里要考虑的两类主要法律约束关系到这一过程的两个主要阶段:(1)正式定义当事方之间的责任份额和(2)分析日志文件以确定事实之后的这些责任。在下面的文章中，我们将依次考察这两类法律约束。
责任限制:评估合同责任限制有效性的第一个标准是当事人的资格。例如，大多数司法管辖区都对消费者提供具体保护，因为消费者被认为是与专业人士签订合同的弱势一方。让我们首先考虑只涉及专业人士的合同。法律规定了责任限制条款无效的几种情况。第一个被认为责任限制无效的明显情况是，要求条款利益的一方犯有故意过错、故意失实陈述或重大过失行为。另一种情况是，这种限制将破坏一方的基本义务，从而在合同中造成不可接受的不平衡。但是，这种情况比较难以评估，要由法官来评估，他可能接受这种限制，认为它是无效的，甚至强加一个不同的责任上限。一个
就消费者而言，法律提供了许多保护措施，严格限制了责任限制条款的适用。这些规则的理念是，消费者在合同关系中处于弱势地位，应该提供法律担保来维持合同中的某种形式的平衡。例如，专业人员必须向其消费者提供法国法律中的“不符合”和“隐藏缺陷”保证，以及美国统一商法典中的“默示保证”(包括“适销性”和“适用性”)。任何会造成严重不平衡、损害消费者利益的条款都将被认为是不合理的。
让我们注意到，我们在这里关注的是合同责任(责任在合同本身中定义):当然，严格责任(当产品缺陷导致个人或财产损失时)总是适用于第三方(不是合同当事人的行动者)。不过，专业人员仍有可能确定合同规则，具体规定其中一方对受害者(第三方)的各自赔偿份额。b
为了结束本小节，让我们提到其他需要考虑的标准，以完善法律分析，特别是:合同本身的资格(产品或服务协议)，如果是产品协议，它是合格的购买协议还是许可协议，软件的性质(专用或现成的软件)，行为者的行为，等等。
日志文件作为证据:关于合同使用日志文件的第一个观察结果是，数字证据现在与传统的书面证据处于同等地位。此外，就法律事实而言(相对于法律行为，如合同)，一般规则是对可用于提供证据的手段不加限制。就法律行为而言，规则取决于交易的金额:例如，在法国，对价值低于1500欧元的合同建立证据的手段没有限制。在我们的项目环境中使用的日志涉及软件组件的行为，这可以被定性为法律事实。即使它们也将被用来确立电子合同的存在和内容(如我们的案例研究)，我们可以考虑在这个阶段，它们的价值将低于法律规定的要求“书面证据”的门槛，或者根据前述的等价原则，日志文件提供的证据将被接受为“书面证据”。
在法庭上使用日志文件的一个潜在障碍可能是“任何人都不能为自己提供证据”的原则。然而，似乎越来越多的人承认，这一普遍原则允许计算机产生的证据有例外。举个例子，法国人接受了一份航空公司打印的旅客在登机柜台迟到的名单作为证据Cour de废弃。c日志文件作为证据有效的另一个条件是其公平性和合法性。例如，信件、信息或电话对话在发送者或接收者不知情的情况下被记录下来，不能用于对他们不利。就我们的项目而言，需要注意的是在日志文件中记录个人数据的风险:在某些情况下，这样的记录可能会被认为是不公平的，导致无法在法庭上使用日志作为证据。
一般来说，为了确保协议中基于日志的证据规定的力度，建议精确定义日志文件的生产、存储的所有技术步骤，以及用于确保其真实性和完整性的手段。最后但并非最不重要的是，与前一小节一样，涉及消费者的案件在证据方面值得特别注意:任何限制消费者通过提供有用的证据来为其案件辩护的可能性的合同条款在法庭上都可能被认为是不合理的。
国际法律:在结束本节时，让我们提一下适用法律的问题。不用说，信息技术业务本质上是国际化的，尽管我们在第一阶段关注的是欧洲的法规，但未来我们将更加关注拓宽法律研究的范围，并理解在设计我们的框架时应考虑到法律和司法管辖区的尊重差异。例如，某些类型的责任限制更有可能被更强调合同自由的美国法院认为是有效的。14
3.责任的正式说明
当事人之间的债务份额在2.3节中以一种传统的、非正式的方式表示。自然语言的文本，甚至是法律语言的文本，往往隐藏着歧义和误导的表述。当这些语句涉及到像软件一样复杂的机制时，情况就更糟了。这种模糊性是合同双方在法律上不确定的根源。在计算机科学领域中，正式(数学)方法的使用已经被长期研究并付诸实践，以定义软件系统的规范(它们的预期行为)，并证明它们的正确性或在它们的实现中检测错误。然而，由于各种原因(包括技术上和经济上的)，大规模地应用形式化方法来证明一个完整系统的正确性仍然是困难的。
与之前关于正式方法的工作相比，我们这里的目标不是将它们应用于系统本身的验证(在我们的案例研究中是手机解决方案)，而是定义故障时的责任，并构建一个分析工具，从系统的日志文件中建立这些责任。
然而，正如第1节所述，应该清楚的是，我们的目标不是提供一个统一的框架，其中所有的负债都必须表示出来。这里提出的方法可以由当事各方自行决定，并尽可能多地表达与被认为代表他们的最高风险来源的特征或潜在失败有关的责任。
在本节中，在3.3节介绍责任函数之前，我们依次给出了用于建立责任的参数(3.1节和3.2节)。
3.1.跟踪模型
根据第2节中的非正式描述，组件、参与者和用户的集合定义如下:
这套邮票是和吗C通信实体(组件和用户)的集合。O而且米分别表示通信操作的集合和消息内容。发送和接收事件之间的区别允许我们捕获通信错误。d
我们假设跟踪中的签名会话是完整的，并且组成消息的每个元素的类型(文档、响应、PIN码和签名)隐式地与元素本身相关联，以避免任何歧义。
我们表示痕迹所有痕迹的集合，一个痕迹T定义为将戳记与项列表关联的函数。每一项都由通信操作(发送或接收)、发送方、接收方和消息的内容定义:
关于上述定义的第一个注释是，我们使用了一个函数类型(从戳记到项目列表)来表示跟踪。这种选择使得在续集中更容易操作跟踪，因为我们总是对与给定会话对应的项感兴趣。也可以选择其他表示，例如包括邮票信息的项目列表。
让我们注意到，为了使数学定义和推理更简单，本节中使用的概念表示对真实系统的抽象。因此，我们在这里使用术语“trace”，并保留术语“log”来表示系统记录的实际信息。Le Métayer等人描述了跟踪和日志之间的联系。12
3.2.跟踪属性
本文先后介绍了两类跟踪属性:误差属性和索赔属性。
错误属性:确定负债分配的最重要参数是可以在系统的日志文件中检测到的错误的性质。理想的情况是，该框架应足够一般化，以反映各方的愿望，并能够有系统地探讨各种错误的组合。实现这一探索的一种可能的方法是，从系统所满足的关键特性的说明开始，并推导出可以导致否定这些特性的情况。
我们的目标是分析日志文件，我们根据跟踪直接描述系统的预期属性。例如，事实是SigApp应该发送IO文档D收到服务公司(仅限本文档)可以表述如下:
在这里考虑的场景中，系统地研究违反该属性的案例会导致以下错误:
空间方面的考虑使我们无法在这里提出这种系统的推导。它依赖于对属性的否定的分解成析取范式，以及对“不存在”属性的附加分解转换的选择性应用。上述分离项对应三种典型的错误类型:
- 第一个术语定义了一种情况，即发送的消息具有与预期不同的内容。
- 第二个术语是预期消息没有发送的情况。
- 第三个术语是发送意外消息的情况。
类似地，否定了这个性质卡只有在收到签名时才返回签名自己的的PIN码POWN导致上述三种类型的几个错误，从中我们认为只有两种是相关的当事人。第一个,Card-WrongVal，描述了批准和签名被发送的案例卡即使它没有收到正确的PIN码:
第二个,Card-WrongInval，定义了一种情况卡拒绝在收到正确的个人密码的文件上签字P自己的：
无需多说，错误也可以根据当事人对系统故障的潜在来源的理解和他们处理特定案例的愿望直接定义。当当事人希望采取更系统的方法以最大限度地减少遗漏相关错误的风险时，可以使用这里建议的推导方法。
最后但并非最不重要的是，用于表示此案例研究的属性的语言相对简单，因为它不考虑跟踪中项目的顺序。通常，可能需要更丰富的逻辑，例如，表示时间属性。属性语言的选择对整个过程没有任何影响，但它可能会使一些技术步骤(如日志体系结构的分析)或多或少变得困难。13
声明属性:索赔属性代表用户索赔的“依据”:它们对应于用户所经历的系统故障。在实践中，这种失败应该对用户造成损害，从而引起责任，但损害被排除在正式的模型之外。因此，可以像错误一样将声明表示为跟踪中的属性。这里我们考虑两个索赔属性，Claim-DiffDoc而且Claim-NotSigned，定义了第2.3节中所述索赔的理由:
第一个定义定义了与以下情形相对应的权利要求自己的已经提交文件了吗D，并盖上邮票(由(收到，SigApp, IO, (D'])与文档不同D由签名应用程序发送给服务器(消息(Send，SigApp,服务公司,是的,D;年代)))。第二个定义定义了一个声明，该声明对应于签名应用程序向服务器发送消息(Send，SigApp,服务公司,是的,D;年代)表明自己的签署的文件什么时候盖章自己的从未提交过任何文件盖章。
3.3.责任的功能
责任的正式规范可以定义为将索赔、跟踪和印章映射到一组当事人的函数e：
在哪里索赔= {DiffDoc, NotSigned}。
作为一个例子，下面的函数捕捉了第2.3节中介绍的负债份额:
这两个案例责任对应于第2.3节中考虑的两类索赔。对于每种类型的索赔要求，第一个测试的目标是检查提出的索赔要求的有效性自己的．如果自己的提出一个没有被跟踪证实的请求，然后的结果责任是空集合，因为没有一方必须对不正当的索赔负责。否则,如果自己的声称收到了一份文件D与所谓的文件不同D,然后SAP是责任如果SigApp已经转发给自己的与收到的文件不同(盖章)的文件ECC (SigApp-Diff (T)))；否则,MPP是责任。类似地,如果自己的他声称自己从未收到过任何盖章的文件SCP如智能卡错误地验证个人密码(Card-WrongVal (T)))；否则MPP是责任。
4.相关工作
责任、保证和责任的重要性及其对软件质量的潜在影响已经被计算机科学家和法律工作者所强调。1，4，21，22然而，我们不知道以前关于应用正式方法来定义软件责任的工作。早期关于合同规范的研究主要涉及一般意义上的义务6，9，19或与特定类型的合同，如商业合同或隐私规则11，18但不要说明与软件错误相关的责任。
服务水平协议也定义了合同条款，但通常侧重于服务质量而不是功能需求，并且不强调正式规范。一个明显的例外是俚语24，25它被赋予了形式化的语义，可以用来指定各种服务，如应用服务提供、互联网服务提供或存储服务提供。此外，还从正式和实际的角度考虑了俚语服务的可监控性和监测性。26
其他几个相互关联的领域也有我们的部分目标，比如软件可靠性，3.基于模型的诊断,5，16入侵检测,10取证,2，20.和数字证据。7，27，28不用说，这些领域中的每一个都是我们项目的有用的灵感来源，但我们相信，由于它们的不同目标，它们没有一个提供了本文中解决的关键问题的答案，即责任的正式规范和工具。
5.结论
如第1节所述，本文的目标是通过一个案例研究来概述我们的方法。由于本次演讲针对案例研究，而不是泛泛地陈述，因此这里没有描述一些技术问题和选择。在本节中，我们提出了一些概括和进一步研究的途径。
痕迹和性质的概念在本文中以一种稍微简单的方式提出。一般而言，各方不妨以更灵活的方式确定责任，并在某些部分的错误执行与系统的故障(以及由此造成的损害)之间建立联系。为了解决这一需求，我们在Goesseler等人中定义了“逻辑因果关系”的概念。8因果关系在责任的法律定性中起着关键的作用。它在计算机科学中也被研究了很长一段时间，但有着截然不同的视角和目标。在分布式系统社区中，因果关系本质上被视为一种时间属性。在Goesseler等人中，8我们已经定义了几个逻辑因果关系的变体，使我们能够表达一个事件的事实e2(例如，失败)将不会发生，如果另一个事件e1没有发生(“必要的因果关系”)还是事实e2不能这么快就避免吗e1已经发生(“充分的因果关系”)。我们已经证明了这些因果性质是可确定的，并提出了痕量分析程序来建立它们。这些因果关系的概念可以整合在这里提出的框架中，以增加用于定义责任函数的语言的表达能力。
另一个需要进一步考虑的方面是证据本身的性质和存储在日志中的值。首先，可能是某些值，例如，出于隐私或安全原因，不应该记录在日志中。还有一种情况是，系统的日志文件中没有包含所有相关信息。例如，在我们的案例研究中，手机所有者已经宣布其设备被盗或已经签署了由ECC发送的产品确认收据，这一事实可以作为分析情况的有用信息(取决于双方决定的责任规则)。因此，跟踪可以不仅仅是日志文件的抽象版本，还包括来自所有参与者的其他类型的操作。
用于说明本文的简单案例研究不允许我们讨论与分布式系统相关的问题。在此上下文中，一个关键的设计选择是日志文件本身的分发。事实上，在可能涉及该日志将被用作证据的索赔行为者控制的设备上记录日志条目，对其他方来说可能是不可接受的。在Le Métayer等中，13我们为日志架构的规范引入了一个框架，并提出了描述“可接受的日志架构”的标准。这些标准取决于系统本身的功能体系结构和各方之间的潜在索赔。它们可以用来检查日志体系结构是否适合于一组给定的潜在索赔，并建议改进以从不可接受的日志体系结构派生出可接受的日志体系结构。在形式方面，我们已经表明，对于给定的威胁模型，可接受的日志体系结构产生的日志可以作为确定责任的证据:从技术上讲，任何对这些日志的索赔的结论性评估都将返回与对真实事件序列的索赔评估相同的答案。
就日志分析本身而言，我们在Mazza等人中使用B方法提出了一个分析器的正式规范。15我们已经证明了增量分析过程的正确性。这个结果使我们有可能在第一次分析的输出的基础上，通过考虑额外的日志或进一步的属性来改进它。
最后，我们应该强调，我们的框架提供的方法和工具可以以渐进的方式应用，这取决于双方的意愿、经济利益和起草合同的时间限制。
- 第一个层次的应用是系统的(但非正式的)负债定义，采用章节2.3的风格。
- 第二级是负债的正式定义，如3.3节所示。这个正式定义本身可能或多或少有些详细，只包括非正式定义的责任规则的一部分。此外，它不需要软件的完整规范，而只需要与目标责任规则相关的属性。
- 第三级是实施日志基础设施或加强现有的日志设施，以确保在提出索赔时能够获得确定责任所需的所有信息。Le Métayer等描述了我们的框架的一个实现示例，12它定义了OSGi的日志架构。
- 第四个层次是实现日志分析器，以协助人工专家进行乏味且容易出错的日志检查。
- 第5级是关于责任的正式定义的日志分析器的正确性的验证(考虑日志文件和跟踪之间的对应关系)。这一水平将对系统产生的结果的有效性带来额外的保证。
这些水平中的每一个都有助于进一步减少负债方面的不确定性，各方可以决定选择与系统可能失败所涉及的风险相称的水平。
最后但并非最不重要的是，我们目前正在处理与日志文件相关的另外两个关键问题，这里没有讨论:使用基于索引的分解方法和技术在存储方面进行优化(压缩、保留延迟等)，以确保其真实性和完整性17，23包括日志项的可信序列化。
致谢
我们要感谢LISE项目的所有成员，他们通过许多讨论和交流，为本文所描述的工作做出了贡献，特别是Christophe Alleaume, Valérie-Laure Benabou, Denis Beras, Christophe Bidan, Gregor Goessler, Julien Le Clainche, Ludovic Mé和Sylvain Steer。
参考文献
1.安德森，R.，摩尔，T.信息安全经济学等。信息安全峰会(IS2)(2009)。
2.Arasteh, a.r.， Debbabi, M.， Sakha, A.， Saleh, M.分析多个日志作为法医证据。挖。投资。4(2007), 8291。
3.阿维齐尼斯，A.，拉普利，j . c .。，Randell, B. Fundamental concepts of computer system dependability. In机器人可靠性研讨会:人类环境中可靠机器人的技术挑战(2001)。
4.Berry, D.M.电器和软件:买方保证的重要性和开发商在推广使用系统质量保证和正式方法方面的责任。在在快速移动场景中建模软件系统结构研讨会论文集(Santa Margherita Ligure，意大利，2000);http://www.montereyworkshop.org/PROCEEDINGS/BERRY/
5.L.， Lazovik, A.， Dague, P.可诊断性的最优可观察性。在国际诊断原则研讨会(2008)。
6.Farrell, a.d.h.， Sergot, m.j.， Sallé， M.， Bartolini, C.使用事件演算跟踪契约的规范状态。Int。j .鸡笼。通知。Sys。(IJCIS) 14， 23(2005)， 99129。
7.Gladyshev, P. Enbacka, A.使用B方法对数字证据进行严格的自动不一致性检查。Int。j .挖。证据(IJDE) 6， 2(2007)， 121。
8.Goessler, G.， Raclet, J.-B。，Le Métayer, D. Causality analysis in contract violation. In运行时验证国际会议(RV 2010)，辽宁航空学报6418(2010)，270284。
9.Governatori, G.， Milosevic, Z.， Sadiq, S.W.业务流程和业务契约之间的合规性检查。在EDOC．IEEE计算机学会(2006)，221232。
10.琼斯，a.k.，希尔肯，R.S.计算机系统入侵检测综述， TR，弗吉尼亚大学计算机科学系，1999年。
11.Le Métayer, D.一个正式的隐私管理框架。在安全与信任的正式层面(FAST)，陆海空三军，陆海空三军，162176。
12.Le Métayer, D.， Maarek, M.， Mazza, E.， poet, M. l。，Frénot, S., Viet Triem Tong, V., Craipeau, N., Hardouin, R. Liability in software engineeringOverview of the LISE approach and illustration on a case study. In国际软件工程会议,卷1。ACM和IEEE(2010), 135144。
13.Le Métayer, D, Mazza, E, Potet, m - l。为法律证据设计日志架构。在软件工程与形式化方法国际会议(sefm2010)。IEEE(2010), 156165。
14.利波维茨基，S. Les关于responsabilité和garantie dans contratites的条款限制。接近比较法国/ États-Unis。哪些局限性。专业知识des systèmes d'信息,没有。237(2000年5月)，143148。
15.Mazza, E, Potet, m - l。，Le Métayer, D. A formal framework for specifying and analyzing logs as electronic evidence. In巴西正式方法研讨会(SBMF 2010)(2010)。
16.基于模型的基于状态图和故障树的故障监测与诊断系统。的完整性。Eng。系统。81年安全(2003), 325341。
17.OSGi平台的安全基准测试:朝向加固的OSGi。Softw.Prac。Exp。(SPE) 39， 5(2009)， 471499。
18.佩顿·琼斯，s.l.，希伯，j.m.。如何写一份金融合同。在编程的乐趣，计算机基础，第6章，2003年。
19.电子合同的正式语言。在FMOODS，施普林格，LNCS 4468(2007)， 174189。
20.网络系统安全中基于时间逻辑的法医调查模型。第一版。Netw。3685年安全(2005), 325338。
21.赖安，dj关于安全与软件责任的两种观点。让法律体系来决定。IEEE安全隐私(JanuaryFebruary 2003)。
22.施耐德，F.B.，追求完美。IEEE安全隐私(MarchApril 2009)。
23.Schneier, B.， Kelsey, J.安全审计日志以支持计算机取证。ACM反式。通知。系统。安全(TISSEC) 2， 2(1999)， 159176。
24.Skene, J.， Lamanna, D.D.， Emmerich, W.精确服务水平协议。在软件工程国际会议(ICSE)， ieee(2004)， 179188。
25.Skene, J.， Raimondi, F.， Emmerich, W.电子服务的服务水平协议。IEEE Tran。软件中。(TSE) 36， 2(2010)， 288304。
26.Skene, A.， Crampton, J.， Emmerich, W.应用服务提供的服务水平协议的可监控性。在软件与性能国际研讨会(WOSP)， acm(2007)， 314。
脚注
a.“佛吉亚案”说明了法国对“基本合同义务”概念的不同解释。2010年6月，最终上诉法院的商会(“Cour de cassation”)驳回了将案件提交给上诉法院的申请，上诉法院宣称责任限制与软件供应商(Oracle)的基本义务并不矛盾，因为客户(佛吉亚)可以获得合理的赔偿。决定原则是考虑合同的整体平衡和当事人的行为来决定责任限制的有效性。
b.在欧洲法律中，产品缺陷的受害者可以起诉任何参与产品制造或经销的行为者。
c。卡斯。文明。1再保险, 7月13日th．2004:牛。文明。2004年,我,没有。207.
本文介绍了ANR(国家研究机构)在ANR-07- sesu -007授权下资助的LISE(软件工程中的责任问题)项目的结果。这篇论文的前一个版本发表在第32届ACM/IEEE软件工程国际会议论文集ICSE 2010。
©2011 acm 0001-0782/11/0400 $10.00
如果您不是为了盈利或商业利益而制作或分发本作品的部分或全部，并在第一页注明本通知和完整引用，则允许您免费制作本作品的部分或全部数字或纸质副本，供个人或课堂使用。本作品的组成部分必须由ACM以外的其他人享有版权。信用文摘是允许的。以其他方式复制、重新发布、在服务器上发布或重新分发到列表，需要事先获得特定的许可和/或费用。请求发布的权限permissions@acm.org或传真(212)869-0481。
数字图书馆是由计算机协会出版的。版权所有©2011 ACM股份有限公司