ACM通信
内部风险
对整个系统可信度
来源:Shutterstock.com
通信长期以来，《内部风险》(Inside Risks)专栏一直强调对风险情况的整体意识的重要性，其中一些情况可能很难提前识别。具体地说，整个系统的期望属性应该被指定为需求。这些期望的特性被称为涌现特性，因为它们通常不能仅仅从较低层次的组件特性中导出，而只能相对于整个系统出现。不幸的是，整个系统可能会出现额外的行为—这要么使满足所需属性的能力失效，要么表明所需属性集的指定不当。
在本专栏中，我将考虑一些情况，在这些情况下，全面系统分析是至关重要的，但通常很难做到有充分的保证。相关的故障可能是由硬件、软件、网络、操作环境以及管理员、用户和误用用户的操作中的一个事件，甚至是问题的组合导致的。这些实体之间的所有相互作用都需要考虑、评估，如果有潜在的危害，则用任何可用的手段加以控制。这里要面对的问题是试图将整个系统作为其组件的组合来分析，而不是仅仅考虑其单独的组件。在许多情况下，系统故障往往发生在这些组件之间的交互和相互依赖关系中，这取决于系统是否模块化地设计以最小化破坏性依赖关系，并仔细指定每个模块。
解决这个问题是一项艰巨的任务，即使对于经验丰富的关键系统开发人员也是如此。无论是明确定义的还是隐含的，整个系统的需求可能是高度跨学科的，包括对人类安全的严格生命关键要求;具有可靠性、鲁棒性、弹性、恢复和容错能力的系统生存能力;安全和完整性的许多方面;保证实时性能;具有法医价值的问责制、高度完整性的证据以及可靠的实时和回顾性分析;对各种物理、电子和其他不利因素的防御;并覆盖众多潜在风险。理想情况下，需求应该非常仔细地在各个体系结构层中指定，最好是在新开发的系统中尽可能正式地指定，特别是在特别脆弱的组件中。尽管这通常不适用于遗留系统，但这里将其作为未来开发的一个有远见的目标。
必须满足高可靠性保证要求的整个系统架构可能必然包含这里所描述的许多内容。然而，当在不可信的硬件和不可信的网络上执行时，操作系统和应用程序软件的行为应该受到怀疑，因为它表明整个系统的理想突发属性可能已经被破坏，或很容易被破坏(导致不良行为)。
解决这个问题是一项艰巨的任务，即使对于经验丰富的关键系统开发人员也是如此。
一个几乎不言自明的结论是，在现实的假设下，就现实的要求而言，整个系统的可信赖性是一个非常长期的目标，任何现实的保证都不可能完全实现。但是，在这方面作出的许多努力在试图抵抗今天发现的许多不利情况方面将是极为宝贵的。本专栏中提到了目前正在进行的一些工作，而且似乎是朝着新系统的方向迈出的一小步，尽管如前所述，对现有遗留系统的适用程度要低得多。然而，整个挑战的艰巨性不应阻止我们进行结构性改进，从而有助于克服今天的短视。
分层和形式化方法
分层的分层设计具有相当大的潜力，但目前主要存在于设计良好的操作系统和分层的网络协议中。这个概念经常被拒绝，因为可以通过良好的设计实践克服错误的嵌套效率论点。近年来，软件和硬件的形式化说明语言和形式化分析得到了越来越广泛的应用。系统需求、高级系统架构、硬件isa和实际硬件的正式规范也可以存在。这里只是一些早期的例子(为了简短起见，省略了许多其他的例子)。
- Dijkstra算法的系统4提供了一个概念上的证明，即精心分层的分层锁定策略永远不会导致层之间的死锁——尽管多年以后才发现单层中的死锁)。
- David Parnas在封装抽象方面的开创性工作在20世纪70年代早期提出了先进的设计考虑。它已成为结构性发展的重要组成部分。11
- SRI分层发展方法论，13PSOS的基础是什么9(其中7层硬件抽象和9层系统软件用一种非可执行语言正式指定，因此可以基于较低的层将每一层的证明缝在一起。PSOS广泛使用了帕纳斯的作品。(许多其他方法也被广泛使用，但大多不那么严格。)
- 维吉尔Gligor51998年，在同一时期率先努力使更高层次的政策问题正式化。Clark-Wilson纸2将安全需求的概念扩展为通用应用程序完整性原则的非正式表示。
- 最近,seL47，8和CertiKOS6提供软件管理程序的重大进步(后者的内部分层类似于HDM)。
- 新的CHERI-Arm Morello硬件指令集架构，具有多个操作系统14包括证明10ISA满足几个关键的硬件可靠性特性。硬件Morello芯片和系统片上板目前正由Arm有限公司试验使用。这只是迈向可靠硬件的一步;还指定了CHERI-RISC-V。与所有其他硬件一样，实际的Morello硬件与其ISA规范的一致性仍然没有得到解决—也就是说，硬件必须准确地执行指定的操作，而不能执行其他操作(例如，插入的模拟电路不能导致添加特洛伊木马等供应链妥协15)．此外，尼拉夫·戴夫的博士论文3.将Bluespec可执行规范语言(Bluespec system Verilog BSV)扩展为BSL，这可以支持扩展到硬件(较低层)和软件(较高层)的编译。
未来的一个长期目标将是拥有层次证明(从硬件到hypervisor、操作系统和应用程序代码)，以证明指定的总体系统需求(带有指定的假设)可以通过某种期望的保证措施得到满足。仍然存在许多潜在的缺陷(不完整的需求和规范、不充分的开发和保证工具、草率的编程、不可靠的系统、恶意攻击，等等)。然而，在实现这一目标的过程中，确保每一步都是必要的，同时也需要更好地分析整个系统。不幸的是，这种方法不适用于大多数遗留的硬件-软件系统，这意味着必须尽早将长期方法注入到未来的技术开发中。
整个挑战的艰巨性不应阻止我们进行结构性改进，从而有助于克服当今的短视现象。
DARPA目前正在计划一个名为PROVERS的新项目:验证器的流水线推理，使健壮的系统能够扩展正式的方法，使其在真实系统的规模上工作，这或许表明还需要更多的研发。
演示应用程序
这里考虑了几个有关的应用领域，在这些领域中，整个系统属性的妥协可能会引起很大的关注。在每一种情况下，分析相关组件都有困难，而且它们嵌入到整个系统中也有困难;要令人信服地证明任何事情都是非常困难的——如果不是完全不可能的话。此外，即使某个特定组件能够以某种方式显示其本身在逻辑上是合理的(通常情况似乎并非如此)，其兼容的整个系统行为可能会因为利用硬件和操作系统缺陷而损害其完整性，或由于糟糕的应用程序而受到损害。
- 密码学。密码学有时被认为是灵丹妙药。然而，过度依赖最好的加密实现及其应用程序尤其令人担忧，尤其是在嵌入硬件或操作系统时，它们本身可能会被破坏。
- 实时系统。具有保证性能和故障安全/故障软/故障安全需求的实时系统的设计必须比笔记本电脑预期更广泛的故障范围和故障模式。一些模拟-数字和混合信号的网络物理系统也是如此。同样，低级故障会影响满足这些需求的能力，就像简单的应用程序特定代码一样。
- 选举的完整性。此前，《内部风险》(Inside Risks)关于选举公正性的专栏曾强调，选举过程的每一个环节都是潜在的薄弱环节。现有的商业系统存在严重的缺陷，而且许多整体系统的弱点都是计算机系统之外的，如果结果被破坏，这些弱点或多或少会使技术变得无关紧要。
- 量子计算。在未来，量子计算及其与传统计算的网络融合很可能会出现意想不到的问题。此外，在量子计算机中所需要的必要的纠错编码可以在错误超过编码系统的限制时纠正结果。因此，选择适合硬件故障实际范围的编码系统变得至关重要。
- 多级安全。值得信赖的计算和通信最苛刻的领域之一是能够同时处理不同级别的关键安全(例如，最高机密到非机密)。除了极少数例外，上世纪70年代和80年代的大多数工作都假定在软件内核中实现所需的分离就足够了。不幸的是，可用的硬件过去(现在仍然)不足。唯一软件方法的显著例外包括20世纪60年代末Butler Lampson的BCC-500计算机(伯克利计算公司)，70年代初Multics的软硬件MLS改造，以及70年代中期PSOS(试图确保MLS作为一种强类型的硬件能力扩展)。
- 人工智能。在所有可能的情况下，基于深度学习、神经网络和通常被称为人工智能的许多其他方面的系统的可信性通常很难证明或评估。此外，需要自我适应或训练的AI元素可能没有被编程或训练为其预期用途;此外，算法和训练数据可能有意或无意地存在偏差。当然，一个经过训练的神经网络不能比它输入的数据做得更好。一般来说，在生命关键和其他要求严格的系统中，使用人工智能似乎是非常危险的，特别是在确定性或证明合理的结果是必不可少的地方(例如，Parnas12，一个)．尽管如此，人工智能非常受欢迎，并发现了许多不同的有用应用。
这些例子只是冰山一角，但却暗示了必须克服的困难。
还有一种可取的做法是进行一些独立的健全检查，以确保整个系统的结果是正确的。
在每一种情况下，都需要进行一些独立的健全检查，以确保整个系统的结果是正确的——或者至少在现实的范围内——与声明的需求相关。形式定理证明中的一个类比是使用可靠的证明检查器来检查证明，尽管这仍然假设了潜在的假设，证明检查器是正确和无偏的。
需要是什么?
愿望法在许多年前就已确立，但在实践中仍未得到广泛应用。一个粗略的过度简化的集合可能包括如下内容:
- 考虑整个系统开发和可信赖性的既定原则，并引用那些最相关的原则。
- 建立定义良好的整个系统需求，可以根据这些需求进行评估，并在可能的情况下正式地指定它们。
- 建立良好定义的系统架构，分层次地定义每个主要接口的可访问接口，从硬件到操作系统和应用程序(例如，Robinson-Levitt，13应用于PSOS的概念硬件和软件，以及软件中的福特航空KSOS1 MLS内核。
- 使用形式化的规格说明和形式化的方法，使形式化分析成为可能，特别是在具有特别关键需求的系统中。分析可能包括依赖关系分析(只寻找不太可信的实体的依赖关系，并避免可能导致死锁的循环依赖关系)和基本属性的证明。层次化的证明从根本上得到了理论上的支持，13但是，如果它们要尽可能地跨越硬件、操作系统、应用程序和整个系统的需求，那么它们在未来仍然潜伏着——通过逐条列出未处理或缺失的需求，并列举仍未发现的威胁，从而清楚地说明超出范围的假设。
- 在整个过程中主动解决无数其他问题。
结论
朝着整个系统可信赖性这一理想的长期目标所采取的一些步骤正在取得重大进展。当然，考虑到我们面临的所有外在问题，这一切还远远不够。然而，对于新的关键系统来说，这个目标仍然是值得追求的——只要它是现实的。这表明我们现在必须开始认识到全面长期目标的重要性。
参考文献
1.Berson, T.A.和Barksdale, g.l.， Jr. KSOS:安全操作系统的开发方法，全国计算机会议，会议论文集(1979), 365 - 371。
2.克拉克，D.和威尔逊，D. r .商业和军事计算机安全政策的比较。在1987年安全和隐私专题讨论会的会议记录。IEEE计算机学会，奥克兰，加州(1987年4月)，184-194。
3.《软硬件协同设计的统一模型》，麻省理工学院博士论文。2011.
4.多道程序设计系统的结构。Commun。ACM 11， 5(1968年5月)，341-346。
5.Gligor, V.D.和Gavrila, S.I.，面向应用的安全策略及其组成。在一九九八年安全模式研讨会论文集1998年，英国剑桥。
6.Gu, R.等。CertiKOS:一个可扩展的架构，用于构建经过认证的并发操作系统内核。在USENIX操作系统设计与实现研讨会论文集(OSDI'16)。(2016年11月),653 - 669。
7.Heiser, G.， Klein, G.和Andronick, J. seL4在澳大利亚:从研究到真实世界的可信系统。Commun。ACM 63， 4(2020年4月)，72-75。
8.Klein, G.等。操作系统微内核的全面正式验证。美国计算机学会计算机系统学报， 1(2014年2月)。
9.Neumann, P.G.等。一个可证明安全的操作系统:系统、它的应用和证明。SRI国际》1980。
10.CHERI的基本诚信原则。在A. Shrobe, D. Shrier和A. Pentland, Eds。网络安全新解决方案。麻省理工学院出版社/连接科学(2018年1月);https://bit.ly/3kgxyt6
11.Nienhuis, K.等。严格的硬件安全工程:CHERI设计和实现过程中的形式化建模和证明。在36年会议纪要thIEEE安全与隐私研讨会, 2020年5月。
12.Parnas, d.l.， Clements, p.c.和Weiss, D.M.复杂系统的模块化结构。《软件工程汇刊， 3(1985年3月)，259-266。
13.帕纳斯，D.L.人工智能的真正风险。Commun。ACM(2017年10月)。
14.Robinson, L.和Levitt, K.N.层次结构程序的证明技术。Commun。ACM 20， 4(1977年4月)，271-283。
15.沃森，R.N.M.等人。剑桥- sri CHERI-ARM Morello和CHERI-RISC-V;https://www.cl.cam.ac.uk/research/security/ctsrd/cheri/
数字图书馆是由计算机协会出版的。版权所有©2022 ACM股份有限公司
没有发现记录