软件认证联盟：挑战与目标 论述软件认证的障碍与解决方法

理论计算机科学电子笔记238（2009）11-17www.elsevier.com/locate/entcs软件认证联盟及其9大障碍约翰·哈哈托纳，1岁， Mats Heimdahlb，2， 马克·劳福德c，3岁，汤姆·迈鲍姆c，3，艾伦·沃森c，3，4，弗雷德·沃登d，5a美国堪萨斯州曼哈顿堪萨斯州立大学计算与信息科学系b明尼苏达大学软件工程中心，计算机科学与工程，明尼苏达大学，明尼阿波利斯，美国c加拿大安大略省汉密尔顿市麦克马斯特大学软件质量研究实验室d微软公司，关闭WA，USA摘要2007年8月和12月，北美学术研究人员、行业代表和监管机构分别受邀参加在华盛顿和明尼阿波利斯举行的会议，目的是成立一个软件认证联盟（SCC）。在第一次会议上，为联合体制定了目标，并颁发了大挑战证书。在第二次会议上，所有与会者都被要求完成声明：“软件认证很难，因为。 . .". 然后，小组通过讨论和投票的方式将结果综合成“前9名”名单。 在本文中，我们描述了我们相信这应该是SCC的目标，通过这些阻止我们使软件认证成为主流的9大障碍的细节。关键词：软件认证联盟（SCC），目标，项目，形式化方法1引言人们在日常生活中越来越依赖软件。除了我们在办公室和家庭中熟悉的所有传统软件驱动系统之外，嵌入式系统中的软件还在我们的汽车中的防抱死制动器、飞机中的线控系统、核电站和救生生物医学系统中实现控制算法。 所有这些系统都是“硬实时”系统 它必须以精确的定时特性做出反应才能正常工作。在一个电子竞技中，1电子邮件：hatcliff@cis.ksu.edu2电子邮件：heimdahl@cs.umn.edu3这项工作得到了NSERC的部分支持4电子邮件：lawford，maibaum，wassyng@mcmaster.ca5电子邮件：fredwurd@microsoft.com1571-0661 © 2009 Elsevier B.V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.09.00212J. Hatcliff等人/理论计算机科学电子笔记238（2009）11为提高这些实时软件系统的质量，从而减少系统故障对公众造成的风险，已对形式化的数学规范、验证和确认技术进行了广泛的研究。虽然这些方法开始显示出在提高软件质量的承诺，它并不总是清楚的软件从业者如何以及这些理论技术模型真正的嵌入式系统，以及它们如何可以应用到实际的工业系统。至于某些形式化的技术是否真的只对学术例子有用，目前还没有定论。 另一方面，工业界和监管机构也越来越清楚，基于与开发过程一致性和测试技术的传统技术，无论多么广泛，都不能保证系统性能达到足够令人满意的水平。这方面的最佳指标之一是最近出版的美国国家科学院关于依赖系统软件的报告[1]。我们预测，这份报告将对指导监管机构和行业非常有意义，它记录了软件开发的当前状态以及需要在未来要做的事情报告强调了两项调查结果。首先，软件开发必须改进，以便在软件发挥越来越大作用的世界中提供更可靠的基于软件的系统。第二，我们需要记录和分析软件故障，以了解影响因素，特别是如果影响因素与开发过程有关。此外，报告还提出了一些重要建议。这些建议是针对两个不同的群体：i）软件的建造者和用户，以及ii）软件教育和研究的支持者。 建议第一组包括：使用正式的方法、软件开发技术和已知有效的原则;构建包含安全问题的可靠性案例;不完全依赖过程和测试来提供可靠性;要求透明度和问责制;将认证建立在对可靠性声明和证据的检查和分析基础上。对第二组的建议包括：在软件专业人员/研究人员的教育中更加强调可靠性;资助基础研究，以提高包含软件的系统的可靠性，重点是可靠性的证据我们基本上同意本报告的结论和建议。 我们认为，报告中隐含的，但应该更强调的是，我们需要使用我们已经知道的关于构建高度可靠的软件的知识，我们需要对如何构建和认证基于软件的系统进行更多的研究，其中重点应该从过程转移到产品。1.1认证的目标认证的目标是根据科学、工程和测量理论的原则，系统地确定一个工件是否符合公认的、定义明确的和可测量的标准。J. Hatcliff等人/理论计算机科学电子笔记238（2009）11131.2联合体目标该联盟代表了一项研究努力，完全没有任何监管机构/公司的任何明确认可。它的目的是了解认证是关于包含（重要）软件组件的系统，对影响此类系统认证的流程和标准提出建议。 我们希望行业、监管机构和大学参与到这个联盟中来，这样我们的建议在现实世界中就能切实有效。我们对医疗设备、核电站、汽车和航空航天领域的系统认证感兴趣。这些领域通常涵盖从相对不受监管的（汽车）到严格监管的（核能）。我们认为，我们需要关注特定领域的问题，但也需要在不同领域和监管水平之间分享想法。 如果我们做好这件事，我们的想法可以在未来由监管机构驱动的开放流程和/或标准组织采用。为此，SCC提出了以下目标：(i) 促进对包含软件的系统（ScS）认证及其所基于的标准(ii) 促进以产品为中心的ScS认证标准的成本效益部署;(iii) 促进公众、政府和业界对ScS认证概念的理解，并接受为软件相关产品制定认证标准的必要性;(iv) 研究并将形式化方法整合到ScS认证和开发中;(v) 协调软件认证计划和活动，以进一步实现上述目标i-iv1.3实现SCC目标主要目标• 开发并记录通用认证模型，作为定义特定领域监管和认证要求的框架。• 概念验证：制定和记录软件监管要求，帮助软件开发人员和软件监管机构在特定领域开发安全可靠的软件应用程序。详细的目标• 使用现有的软件工程和正式方法知识，为特定领域的关键软件（包括硬实时、安全关键系统）制定适当的循证标准和审计点。• 创建符合上述标准的软件开发方法和关键软件开发的审计点• 研究和开发改进的方法和工具，用于开发crit-14J. Hatcliff等人/理论计算机科学电子笔记238（2009）11ical软件。2第一千一百一十一章大挑战令人惊讶的是，目前对关键软件的可靠性如何监管并没有一致的看法。 社会开始要求关键系统中使用的软件必须满足最低的安全性、可靠性和可靠性标准。这些系统的制造商处于不利的地位，没有明确的指导方针，什么可以被视为可接受的做法。即使在系统不是关键任务的情况下，软件生产商和他们的客户也对保证质量的方法感兴趣，这种方法可能会导致提供有保证的软件最好是考虑应该满足什么标准，以及如何确保在我们被迫匆忙采取行动之前遵守这些标准，因为另一个严重事故或一系列软件相关故障的后果 在这种情况下，SCC通过麦克马斯特大学的软件质量研究实验室，向软件工程和正式方法社区发起了一项“软件大挑战”，涉及管理真实医疗器械（即心脏起搏器）的关键软件6。该设备的规格由波士顿科学公司热情地提供，非常紧密地基于他们不久前建造的设备。它具有原始设备的所有功能和微控制器基础硬件参考平台是这一挑战的关键组成部分SCC还设计了一个以证据为基础，以产品为中心的认证过程，以提供评估挑战解决方案的方法。鼓励参与者提交支持性证据以及他们的解决方案。该支持性证据将用于开展认证活动。这将使挑战赛“社区”能够探索许可证（即认证）的概念以及标准在此类软件生产中的作用。此外，它将为比较挑战的假定解决方案提供更客观的基础。认证活动的结果将提供给参与者，并最终纳入挑战产生的出版物中在北美销售的此类器械的主要认证机构是美国食品药品监督管理局（FDA）。FDA已经表示，他们将积极参与这一挑战。我们目前正在努力让加拿大卫生部也参与进来上述挑战已被接受为由英国管理的Grand Challenge Consortium推广的国际“Grand Challenge”之一我们认为这是许多类似挑战中的第一个，其他挑战还涉及汽车和航空航天领域安全关键系统可以被看作是软件认证的“薄弱环节”，因为系统故障的成本和后果目前证明了行业认为形式方法的额外费用是合理的。挑战在于创建实践工程师可以使用的理论和工具，使理论应用于工业中的“现实世界”问题。随着严格的技术变得更加完善，有了更好的工具支持，6有关“领跑者大挑战”的详情，请访问：http://sqrl.mcmaster.ca/pacemaker.htmJ. Hatcliff等人/理论计算机科学电子笔记238（2009）1115软件开发行业将看到形式化方法的应用和软件认证的接受程度的增加。因此，SCC最初专注于航空航天、汽车、医疗和核领域的认证工作软件认证在12月的SCC会议上，与会者确定了以下9个障碍。其中前4个被选为前4个障碍，顺序如下。剩下的5个障碍没有被优先考虑。(i) 期望的清晰度和与监管机构沟通的方法-应用程序开发人员不知道要生产什么，通常不得不支付顾问费用来解决问题。在许多情况下，顾问并不正确。监管机构也很难传达预期的变化(ii) 缺乏对证据的明确定义以及如何对其进行评估-我们没有足够的理论来帮助我们确定表明软件产品可靠性的属性和标准的有效性。 我们也有一个问题，在理解如何结合不同的证据文物时，确定采矿的整体评价的(iii) 需求和环境假设的文档记录不佳-这是老生常谈，但确实如此，没有准确和完整的需求，我们就没有可靠的证据证明应用程序将提供所需的行为。 它众所周知，不完整/差的需求和不正确/未说明的环境假设会导致差的应用程序。(iv) 不完全理解检查、测试和分析的适当使用--我们不清楚什么时候应该使用检查、测试和数学分析来达到特定的可靠性水平(v) 没有覆盖范围的总体理论，使覆盖范围能够在多种核查技术之间积累-显然，没有单一的质量保证技术对于有效的验证是足够的，并且作为有效的证明证据。以往的经验表明，各种自动化形式验证技术（如静态分析、模型检查和定理证明）以及常规测试技术都是有效的，但这些技术在验证的属性强度、所涵盖的行为类型以及最自然应用的生命周期阶段方面存在差异。 这些技术中的每一种不仅需要报告行为/属性的覆盖范围并产生验证证据，而且覆盖范围/证据需要在各种技术之间共享和累积。通过一个统一的覆盖/证据框架在各种技术之间共享覆盖/证据将（a）使一种技术的成功减少伴随技术的义务，（b）澄清必须通过以下技术填补的核查差距。 最有说服力的正确性论证将依赖于能够以定量的方式准确地陈述多种验证技术如何各自为整体正确性提供证据。16J. Hatcliff等人/理论计算机科学电子笔记238（2009）11(vi) 定时、容差和并发程序等属性的覆盖理论-测试的结构覆盖概念在安全关键软件的开发和认证中起着关键作用。尽管可追溯到DO-178 B中规定的修改条件/决策覆盖（MCDC）等要求的测试的结构覆盖要求是提供正确性证据的一种远非完美的机制，但它们是现有认证标准中为数不多的几个概念之一，这些概念提供了对程序行为在质量保证过程中被检查的程度的量化评估。 不幸的是，现有的覆盖措施未能考虑到（a）属性，如定时和公差范围的数据值和（b）的程度，在并发计算中的交织行使。因此，即使是成功实现高水平强制覆盖措施的开发团队，也常常无法充分探索和验证计划错误的常见来源(vii) 很难先验地估计验证和确认成本-目前，很难为引入正式技术提出强有力的商业理由 或者，事实上，对于任何新技术，因为很难估计（a） 进行各种形式的正式分析所需的时间，以及（b）核证过程本身的成本或与开发生命周期后期发现的缺陷减少有关的长期成本的减少，在类似系统的后续开发中更多地重复使用，减少对已部署系统的召回，以及减少责任成本。(viii) 缺乏可互操作的工具来管理、推理和提供可跟踪性- 结果是，小的更改通常需要大的扩展。我们需要可扩展的工具。(ix) 法律、法规、律师和政治--认证具有法律意义，因此，直接的技术决策存在所有正常的障碍。尽管技术问题可能很难解决，但政治上的考虑使这一过程变得不可估量地复杂。4结论我们认为，严格的软件工程原则和正式方法应用于：i）开发可靠的软件应用程序，并附有适当级别的认证证据;以及ii）开发软件认证过程，该过程更侧重于产品（包括附带证据）而不是软件开发过程。上述障碍虽然是独立得出的，但与NAS报告[1]基本一致5SCC参与者12月SCC会议的与会者有：Jo Atlee，Rick Chapman，Rance Cleaveland，DarrenMooper，Arie Gur Finkel，John Hatterdan，Mats Heimdahl，Brian Larson，Mark Lawford，Tom Maibaum，Dennis Peters，Oleg Sokolsky，DavidJ. Hatcliff等人/理论计算机科学电子笔记238（2009）1117屈里曼，艾伦·沃森，弗雷德·沃登.引用[1] Jackson，D.，J. Bloch，M.德瓦尔特河Gardner，P.李，S。B. 利普纳角Perrow，J.Pincus，J.拉什比L.沙，M。托马斯，S。Wallsten和D. Woods，“软件依赖系统：充足的证据？”国家科学院出版社，2007年。URLhttp://www.nap.edu/catalog.php?备案号：粤ICP备1101923号-1