保证案例:合理的安全案例



来源



评估安全性而不丢失任何内容的最佳方法是什么?是否可以在一个文档(或图表)中收集所有各种各样的安全工件,并以一种可以理解的详细程度可视化任何方面的方式组织它们?



技术人员很乐于发明这样的“哲学之石”,即使它不提供安全性,也至少会以所需的完整性级别对其进行评估。这样的发展已经存在了20多年,但是,对于说俄语的读者来说,几乎是未知的。这将与“保证案例”(或“安全案例”)方法有关,这意味着结构化的论证和书面证据,证明系统或服务符合特定要求是合理的。



介绍



在阅读本文之前,我想提请您注意几个要点。所声明的材料首先适用于关键信息基础架构(CII)的对象。对于此类对象,特别是对于信息和控制系统,必须执行安全性分析。安全分析的结果以适当的报告的形式显示。所有这些工作已经进行了数十年,但是,报告通常具有任意的文本形式,其逻辑并不总是易于理解。



所提出方法的主要思想是可以使用半正式符号以图形形式显示安全性分析的结果,并具有所有随后的优点。因此,“保证案例”是一种综合查看所有确保和评估安全性措施的方式,而无需替换或取消诸如测试,静态代码分析,可靠性计算,FMEA,风险分析等私有方法。本文是先前发布的安全性系列的继续



论据图及其哲学渊源



我们如何理解或断言某些物体是安全的?显然,为此必须引入许多标准。但是,对于这些标准,我们需要确定我们对物体的了解有多可靠?我们为什么可以相信这些知识?是什么使我们的推理和推理真正可信?深入研究了这些问题之后,没有本体论,认识论,认识论,逻辑等哲学学科,也没有没有担心这些问题的伟大思想家,人们就做不到。在古代世界,例如亚里斯多德和柏拉图,在“近代”时代,弗朗西斯·培根被认为是现代科学方法的奠基人。



如何以合理和合乎逻辑的方式证明或评估安全性?这种方法基于论证理论。1958年出版的英国哲学家斯蒂芬·图尔明Stephen Toulmin)的著作《论辩的用法为论证的现代发展提供了新的动力。 Tulmin用其他参数扩展了逻辑隐含推理,并提出以图形形式表示此操作。 Tulmin的表示法与以下实体一起使用:数据(D)-用于分析的初始数据,声明()-逻辑暗示推断的目的(如果为D So C),保证书(W)-附加参数,限定词(Q)-对逻辑结果的置信度可推论的推论(R)是另外一个反论点(图1)。





图1. Stephen Tulmin的符号



用于可视化和推理Toulmin 的自变量或自变量图(Argument the Map),但他最成功地总结了用于分析和验证自变量的结构模型。请注意,现代参数映射通常不使用Tulmin的表示法,所有内容都得到了简化,例如,如下图所示。这是付费在线服务Rational使用的表示法(有一个免费版本,但功能极为有限)(图2)。付费版本能够将结果图转换为逻辑结构的文本。该网站还提供有关批判性思维和论据映射的免费指南和教程





图2.与服务一起开发的参数图理性



如您所见,一切都是透明的,只有四个实体以及它们之间的三种关系。逻辑输入的结果称为争用,确认参数-原因(由于连接),反参数-反对(但连接),但是反参数的反参数具有特殊名称-反驳(但是连接)。



当前,尚无公认的构造自变量映射的符号。用于自变量结构的表示法不统一。例如,推理结果可以称为要求,争用,结论,目标。参数可以称为前提,理由等。在参数建模领域有许多国际倡议和社区(例如,参数交换格式,AIF),但他们没有解决统一的问题。有一项研究在论点图和思维图之间进行了比较(思维图,每个人都可能听说过)。确实,思维导图编辑器的功能使您可以构建自变量图的类似物。



保证案例的历史和概念



所有这些与安全性有什么关系?为了回答这个问题,让我们回到二十世纪下半叶,那里是确保安全的现代理论和实践的起源。然后,由于核能,航天技术,油气和化学工业,运输等复杂技术产业的发展,人类面临着前所未有的人为灾难。



然后出现了第一份安全分析报告,其中汇总了所有相关要求以及确认其符合性的信息。后来出现了“安全案例”一词(实际上是关于安全性的分析报告),它是“保证案例”的前身。请注意,术语“安全案例”或“保证案例”不能直接翻译成俄语;在这种情况下,最合逻辑的翻译是“安全案例”。尽管,例如,在ISO / IEC 15026系列标准的俄语翻译中(系统和软件工程-系统和软件保证),“保证案例”被翻译为“保证案例”。



应当指出,在某些行业中,仍然使用术语“安全案例”和“保证案例”。保证案例(Assurance Case)是一个更现代的术语,与安全案例相反,因为今天的系统不仅必须满足安全要求,而且还必须满足安全要求。因此,建议使用“保证案例”的概念,并使用“安全案例”将其视为特例。



“保证案例”在这个术语的现代意义上是指有关执行的安全性分析的报告,包括以图形或表格形式的可视表示形式,这些报告使用半正式的符号表示(这些符号将在下面进行讨论)。同时,由于可以将保证案例一方面解释为文档(安全分析报告或安全案例报告),另一方面又可以将其解释为使用半正式表示法的论证系统,因此获得了相同术语的某些差异。 ...理想情况下,保证案例可以包含两个部分,也就是说,评估安全性的文档是基于参数模型构建的。



但是,让我们回到二十世纪。要求开发和分析潜在危险工业设施安全案例的第一份监管文件是CIMAH(工业重大事故危害控制)法规,该法规最初于1984年在英国发布,然后在其他几个国家进行了修改。在北海Piper Alpha石油平台发生史无前例的事故后,安全案例的广泛实施开始付诸实践,该事故于1988年造成167人死亡。



在1990年代,研究人员继续寻求评估安全性的新方法。这个想法似乎浮出水面:让我们开发一个特殊的符号来证明人造物体和系统符合安全要求是合理的。英国的两个大学团队接管了成立分公司Adelard的伦敦大学和约克大学。我必须说,今天,阿德拉德(Adelard)和约克大学(University of York)在推广“保证案”方面占据领导地位。



对于符号的开发,重点放在逻辑上的推理上,即系统的属性或组件符合规定的要求。我们已经考虑过的斯蒂芬·托尔明的作品被选为理论依据。作为人道主义者,图尔明几乎没有考虑过人造系统,但他作为“保证案”论点的奠基人就载入了历史。



英国人以图尔明的表示法为基础,很快开发了“保证案例”方法(在当时称为“安全案例”),并将结果带入了实际的工业实施中。在约克大学,博士生Tim Kelly在John McDermid教授的指导下开发并推广了目标结构表示法(GSN)。结果,有一种罕见的情况是当论文争论安全性:管理安全案例的系统方法。博士论文。约克大学(University of York,1998)被认为已经是20多年来的经典著作,并且继续被人们积极引用。但是,我认为解决安全问题的方法更具学术性,因此,由于某种原因,与支持保障案例的软件工具的开发并没有采取看似可以理解和合乎逻辑的步骤。



相比之下,由Robin Bloomfield和Peter Bishop领导的Adelard主要关注将结果商业化。在约克的同时,在伦敦开发了“声明,论据和证据”(CAE)符号以及Adelard ASCE软件工具(保证和安全案例环境),它同时支持CAE和GSN。在英国,法律和标准要求在许多与安全相关的领域中开发保证案例(安全案例),因此ASCE在这里具有相当强大的市场。 ASCE一直是并且仍然是最常用的Assurance Case开发工具。该工具的主要部分是图形编辑器,在其中可以将其他文本或超链接信息附加到图形块(图3)。您不能自己从Adelard网站下载ASCE软件。您必须完成30天试用期或学术许可的申请,之后公司将审核该请求。





图3. Adelard ASCE程序的界面



现在,让我们看看用于开发保证案例的两个基本符号(CAE和GSN)。



CAE(索赔,论据和证据)表示法



CAE(声明,论据和证据)表示法在三个指定的实体上运行:目标表示系统所需属性的实现,确认为论证提供了书面基础,证明了目标的实现或未实现,论点是使用推理规则构建并建立连接的有目的的确认。通常使用诸如确定性(或逻辑性),概率性和定性性之类的参数。为了指定目标,论据和证据,引入了具有各种形状的图形基元(图4)。



图4.索赔,论据和证据(CAE)表示法:主要组成部分



建立目标和子目标的层次结构是制定“保证案例”的第一步。如图所示,目标,自变量和断言的结构不必是三层的,例如,可以使用其他子目标来支持自变量。CAE表示法也很容易转换为表格形式。该表的列将具有相同的目标,参数和确认,现在将在表记录内建立链接。例如,exida使用了类似的方法来开发保证案例



GSN(目标结构表示法)



GSN的运作要素包括目标(目标,用矩形表示,是CAE中的索赔的类似物),论证策略(用平行四边形表示,并且是论点的策略)和解决方案(用圆圈表示并类似于证据)(图5)。上下文用于目标的信息支持。假设和理由可以用来支持这一论点。目标的结构是分层的。





图5.目标结构表示法(GSN):主要组成部分



在比较CAE和GSN时,应注意CAE更加关注单个论证的依据。为此,进行了论证步骤的详细设计。 GSN更侧重于通用参数结构(模式)。由于实体的数量较多,GSN的要求较不严格,同时,通过更简洁的描述,可以将其简化为CAE。每个符号的使用可能是非常主观的,因为构造参数的方法取决于执行此任务的人员。一些“保证案例”从业者注意到,与语义元素定义的完整性相关的符号存在许多空白。



碰巧的是,今天的GSN更常见。标准中固定的GSN格式目标管理表示法(GSN)社区标准,以及对象管理组(OMG)结构化保证案例元模型(SACM)数据模型



知识库:行业,标准,研究,工具,替代符号



保证案例主要用于其使用受到监管文件约束的行业。这里的领导人是英国和英联邦的其他一些国家。英国卫生基金会报告《在工业和医疗保健中使用安全案例》(2012年)描述了在医疗保健,航空,核电,汽车,国防,石化和铁路行业中《保证案例》(安全案例)的监管经验。



考虑到在英国境外适用保证案件的要求,应注意:

  • 汽车标准ISO 26262:2011,道路车辆-功能安全,是详细列出IEC 61508要求的功能安全标准系列的一部分;
  • European Organisation for the Safety of Air Navigation (EUROCONTROL): “Safety Case Development Manual, 2006”, “EAD (European Aeronautical Information System Database) Safety Case, 2009”, “EAD (European Aeronautical Information System Database) Safety Case Guidance, 2010”;
  • “Licensing of safety critical software for nuclear reactors – Common position of international nuclear regulators and authorised technical support organisations, 2018”, (, , , , , , , , );
  • ISO / IEC 15026系列标准,系统和软件工程-系统和软件保证,包括四个部分:第1部分:概念和词汇(2019); 第2部分:保证案例(2011年);第3部分:系统完整性级别(2015年);第4部分:生命周期中的保证(2012)。



同样值得一提的是活跃于保证案件领域的许多组织(除了已经提到的Adelard和约克大学的高完整性系统工程小组)。这些包括:



Adelard ASCE(案例案例和安全案例环境) 仍然是最著名的Assurance Case支持软件。不同年份提到的大多数项目都没有达到任何严重的水平。 NASA宣布创建AdvoCATE软件,但他们将其用于自己的目的,并且不打算将其发布给市场。考虑到符号的简单性,您可以使用例如MS Visio来绘制“保证案例”图,并用超链接对其进行补充。



开发保证案例的替代方法包括NOR-STA软件工具...它将由波兰的Argevide公司(格但斯克工业大学的衍生公司)开发。 NOR-STA支持其自己的TRUST-IT表示法。不同之处在于,NOR-STA代替了图形表示,而是使用结构化的分层列表(图6)。







图6. Trust-IT表示法:



保证案例的目标层次结构列表中的核心组件和案例研究实体用不同的图标表示。议论策略用于确认对陈述的遵守,事实或观察,理由,假设和其他陈述被用作证据的类似物。与台式机Adelard ASCE不同,NOR-STA在线使用并支持分布式团队合作。



另外,保证案例用于解决以下应用程序:

  • 评估复杂属性的属性,例如质量,可靠性,安全性;
  • 通过将标准要求转换为论证结构来支持认证和标准化;
  • 基于保证的开发(ABD)或基于保修的产品开发是基于模型的开发(MBD)的一种形式。
  • 知识管理,例如,对文档的结构进行建模或确定活动的任何领域(业务流程,工作流,变更管理等)中的结构链接。


信息安全保证案



安全(可信任)案例被称为保证案例的一种。如有必要,可以在安全案例中添加安全案例组件。实际上,“保证案例”背后的想法是将安全性与安全性相结合。在认证领域,ISO / IEC 15408(通用标准)标准有所发展,其要求已转换为与“保证案例”结构兼容的结构。可以针对其他相关标准(例如ISO 27000或IEC 62443或任何其他框架)进行此转换。



一个示例是“安全保证案例”片段张贴在US-CERT网站上。本摘要回顾了软件开发生命周期(SDLC)的实现证明。重点在于消除编码缺陷(尤其是缓冲区溢出),为此使用了诸如培训程序员,代码审查,静态分析和测试之类的方法。当然,您可以对此片段的完整性进行争论,但它仅是为了举例说明(图7)。





图7.安全性保证案例片段



因此,尽管信息安全是最需要保证性案例的应用程序,但应注意的是,尽管它具有潜力和大量的试验研究,但是保证性案例尚未成为该领域的普遍做法。



案例研究保证案例



最后,让我们看一个如何工作的例子。它基于一种基于结构化论证发展的方法



结构化的论点



让我们想象一下在两个连续步骤中开发参数的过程(图8)。第一步,称为推理步骤(RS),是对子目标(SC)的分析,旨在实现主要目标(C)。在这一步,论证的结构得以发展。在称为证据步骤(ES)的第二步中,制定确认(Evidece,E)以支持在上一步中生成的子目标(SC)。为了进一步规范RS和ES步骤,使用了典型的结构化文本(ST)模板。





图8.结构化参数的步骤和组成



需求层次



想象一下形成与“保证案例”列相对应的结构的需求层次结构或金字塔。计算机系统或软件的大多数法规要求具有3或4级要求结构(图9)。





图9.需求层次结构及其与论证步骤的关系



零级是一个元目标,根据此目标,被评估系统必须满足所有安全性要求。在第一级,实现了总体安全目标,例如,IEC 61508对功能安全的要求遵循以下目标:

  • 必须实施安全管理体系;
  • 在系统(或软件)开发期间,必须应用安全生命周期;
  • 系统必须采取足够的措施以防止意外故障;
  • 对于系统(或软件),必须采取足够的措施来防止系统和软件故障,包括防止网络攻击。


在第二层,需求组支持特定的全球目标。例如,安全管理要求(根据IEC 61508)包括人员管理,配置管理,文档管理和其他方面的要求组。零级,第一级和第二级之间的链接结构是一个相当简单的树。这样的结构不需要详细说明参数,因为这些参数是典型的,并且已经在各种项目中反复测试。但是,当从第二级转到较低级时,需要结构化的参数。在这种情况下,较低级别的需求可以是复合的(即,包括多个单独的需求)或简单的(原子的)需求。如果所有需求都是原子需求(没有复合需求),那么该级别将成为第三个级别,然后与需求子组直接相关。如果有复合要求,那么我们将获得更复杂的四级结构。



对于最低级别,除了RS外,还应应用ES。由于向图的结构添加有关自变量内容的详细信息很不方便,因此从第二层开始,使用结构化文本(ST)标记了自变量描述,从而确保了“保证案例”图的每个节点。底部的“保证案例”图不再是树,因为同一确认(E)可以支持不同的子目标(SC)。



一组HR要求的保证案例(IEC 61508)



作为说明,请考虑与IEC 61508 HR要求(IEC 61508-1第6条相关的保证案例摘要



描述和结合所有相关要求的推理步骤(RS)的结构化文本
Reasoning Step (Human Resource Management)

Context

Connection between the group of Human Resource Management requirements of the Assurance Case Level 2 and composite and separate requirements of Level 3

Docs

Human Resource Management Plan

Claim

Human Resource Management complies with IEC 61508 requirements

Subclaim SC1 (IEC 61508-1, 6.2.1), SEPARATE

Persons responsible for specific activities shall be appointed

Subclaim SC2 (IEC 61508-1, 6.2.3), SEPARATE

Project participants shall understand their roles and responsibilities

Subclaim SC3 (IEC 61508-1, 6.2.4), SEPARATE

Communications of the project participants shall be defined

Subclaim SC4 (IEC 61508-1, 6.2.13), SEPARATE

Evaluation and assurance of the project participants’ competencies shall be performed

Subclaim SC5 (IEC 61508-1, 6.2.14a,…,k), COMPOSITE

Competencies shall be considered in relation to the particular application, taking into account all relevant factors

Subclaim SC6 (IEC 61508-1, 6.2.15), SEPARATE

Competencies of all responsible persons shall be documented

Subclaim SC7 (IEC 61508-1, 6.2.16), SEPARATE

Human resource management activities shall be implemented and monitored

Justification

Structure and content of the Human Resource Management Plan

END Reasoning Step



从IEC 61508中提取了总共七个人员管理要求。从结构论证的角度来看,这些要求是子目标(SC1,...,SC7)。子目标(SC5)中只有一个是复合目标,其他所有子目标都是原子的。为了从复合子目标(SC5)迁移到原子(SC5.1,...,SC5.11),需要执行推理的另一步骤(RS)。可以理解,根据IEC 61508的要求,为与抽象产品创建相关的项目制定了人力资源管理计划。该计划在项目范围内解释了标准的要求。



确认步骤(ES)的结构化文本
Evidential Step ES1,…,ES6

Context

Connection with the subclaims of the Levels 3 and the Level 4

Docs

Human Resource Management Plan; Communications Plan; Training Plans; Training Reports

Claim

SC1,…, SC7

Evidence E1

Organizational Chart

Evidence E2

Project Roles Description

Evidence E3

Participants and Signature List

Evidence E4

Participants Communications Plan

Evidence E5

Competency Matrix

Evidence E6

Training Plans and Reports

Claim -> Evidence

SC1 -> E1&E2; SC2 -> E3; SC3 -> E4; SC4 -> E5&E6; SC5 -> E5&E6; SC6 -> E5&E6; SC7 -> E1&E2

Justification

Structure and content of E1,…,E6

END Evidential Step



对于所有确认步骤(ES),建议使用共同的结构化文本来指示确认(E)的子目标(SG)之间的链接。我们将使用关系SG-> E来表示相应子目标(SG)与支持该目标的确认(E)之间的关系。



SC5综合需求分析
S5 . , (ES). , (RS) (ES). .







«» (RS), , , (ES).



根据GSN表示法,可以将所有获得的关系SG-> E转换为Assurance Case列,并为结构化论点进行修改(图10)。该图反映了符合IEC 61508的与人员管理有关的整个要求组。该图还可以用作评估是否符合IEC 61508要求的模板





图10.保证案例图是从一组HR要求的结构化参数中得出的(IEC 61508)



乍看之下,这一切都是漫长而复杂的,但是,尽管如此,保证案例仍具有实际应用价值。这是我们在认证RdICS PLC符合IEC 61508时使用的方法



结论



保证案例(安全案例)方法已经使用了20多年,用于分析CII设施的安全性。这种方法在英国和许多英联邦国家中最广泛地用于医疗保健,航空,核能,汽车,国防,石化和铁路等行业。



保证案例的优势包括通过可视化复杂主题领域中的关系,改善我们的感知和理解所获得的所有优势。缺点是由于该方法的主观性取决于其对评估人员的专业知识的依赖。此处描述保证案例应用程序中最著名的“史诗失败”...简而言之:2006年9月2日,英国空军Nimrod飞机在阿富汗发生大火。该问题起因于燃油泄漏。船上所有14人被杀。较早的《安全案例》报告确认了飞机的安全性。调查表明,在生产型飞机上对燃油系统的改装并不完全正确,以前也曾出现过类似的问题,但由于某种原因,没有人将其视为系统错误。在这份长达600页的报告中,该事件仅被称为“领导,文化和优先事项的失败”。



顺便说一下,Nimrod的报告中未使用图形符号。这场灾难的后果之一是在论据构建领域的研究不断深入。但是,尚未开发出满足所有人的通用方法。



今天,保证案例实施的主要驱动力是法规和法律要求,而不是便利性,可行性或成本效益。显然,在“保证案例”领域中,人工智能有很大的机会,但不知何故,我还没有遇到有关该主题的出版物。

然而,与评估复杂系统的安全性相关的问题仍然存在。积极实施“保证案”可能会在这一领域取得一些进展,因为这种方法是基于从哲学研究开始就占据人类的所有重要观点。



All Articles