哪些语言用于安全关键软件?[关闭]

Ada 和 SPARK (这是一种ADA方言,有一些钩子用于静态验证)在航空航天界用于构建高可靠性软件,如航空电子系统。有点像 ecosystem of code verification tooling for these languages 尽管这种技术也存在于 more mainstream languages as well .

Erlang 是 designed from the ground up 对于 writing high-reliability 电信代码。它的设计是为了便于分离错误恢复的关注点(即生成错误的子系统与处理错误的子系统不同)。它也可以接受正式的证明,尽管这种能力并没有真正远离研究领域。

Functional languages 如 Haskell 由于 declarative nature 语言。这使得带有副作用的代码可以包含在一元函数中。对于正式的正确性证明,可以假定其余代码只做指定的事情。

但是,这些语言是垃圾收集的,垃圾收集对代码是透明的,因此不能以这种方式进行推理。垃圾收集语言通常不足以预测硬实时应用程序,尽管在时间限制的增量垃圾收集器方面有大量的研究正在进行。

Eiffel 它的后代已经内置了一种称为 Design By Contract 它提供了一个强大的运行时机制,用于合并 invariants. 虽然埃菲尔从未真正流行过,但开发高可靠性软件往往包括在实际编写功能之前预先编写故障模式的检查和处理程序。

虽然 C 和 C++ 它们不是专门为这类应用而设计的,由于多种原因,它们被广泛用于嵌入式和安全关键软件。Note的主要属性是对内存管理的控制(例如,它允许您避免垃圾收集)、简单、调试良好的核心运行时库和成熟的工具支持。今天使用的许多嵌入式开发工具链最初是在80年代和90年代开发的,当时这是当前的技术,来自当时流行的Unix文化,因此这些工具在这种工作中仍然很流行。

虽然必须仔细检查手动内存管理代码以避免错误,但它允许对依赖于 garbage collection. 这个 core run time libraries C语言和C++语言相对简单、成熟和理解得很好,因此它们是最稳定的平台之一。如果不是所有的静态分析工具,大多数用于艾达也支持C和C++,并且有很多。 other such tools available for C . 有 also several widely used C/C++ based tool chains 艾达所使用的大多数工具链也有支持C和/或C++的版本。

Formal Methods 如 Axiomatic Semantics (PDF) Z Notation 或 Communicating Sequential Processes 允许对程序逻辑进行数学验证,并且通常用于安全关键软件的设计,其中应用程序足够简单,可以应用它们(通常是嵌入式控制系统)。例如, one of my former lecturers 为德国铁路网的信号系统做了正式的正确性证明。

形式化方法的主要缺点是相对于被证明的底层系统,其复杂性呈指数增长的趋势。这意味着在证明中存在很大的错误风险,因此它们实际上仅限于相当简单的应用程序。正式的方法被广泛地用于验证硬件的正确性,因为硬件错误修复起来非常昂贵,特别是在大众市场的产品上。自从 Pentium FDIV bug 形式方法得到了广泛的关注,并且 used to verify the correctness of the FPU 在奔腾Pro之后的所有英特尔处理器上。

许多其他语言被用来开发高度可靠的软件。 A lot of research has been done on the subject. 有理由认为 methodology is more important than the platform 尽管存在一些原则,比如简单性、选择和控制依赖性,但是 preclude the use of certain platforms .

正如其他许多平台所指出的,某些O/S平台具有提高可靠性和可预测行为的功能,如看门狗定时器和保证的中断响应时间。简单性也是可靠性的强大驱动力,许多RT系统故意保持非常简单和紧凑。 QNX (我唯一熟悉的O/S,曾与 concrete batching system 基于它)非常小,可以放在一张软盘上。出于同样的原因, OpenBSD -它以其强大的安全性和彻底的代码审计而闻名,也不遗余力地保持系统的简单。

编辑: This posting 有一些链接到关于安全关键软件的好文章,特别是 Here 和 Here . 向S.Lott和Adam Davis提供来源的道具。关于 THERAC-25 在这个领域有点经典。

对于C++,联合攻击战斗机(F-35)C++编码标准是一个很好的读数:

http://www.stroustrup.com/JSF-AV-rules.pdf

我相信 Ada 仍在一些安全和/或任务关键的政府项目中使用。我从来没有用过这种语言,但它和埃菲尔在我的“要学”名单上。埃菲尔铁塔提供合同设计,旨在提高可靠性和安全性。

首先,安全关键软件遵循与经典机械和电气工程领域相同的原则。冗余、容错和故障安全。

作为旁白,正如前一张海报所暗示的(出于某种原因被否决),能够实现这一目标的最重要因素是让你的团队对正在发生的一切有一个坚定的理解。毫无疑问,优秀的软件设计是关键。但它也意味着一种语言是可访问的、成熟的、得到良好支持的,对于这种语言,有许多公共知识和经验丰富的开发人员可用。

许多海报已经评论说,操作系统在这方面是一个关键元素,这是非常正确的,因为它必须是确定性的(参见QNX或VXWorks)。这排除了大多数为您做幕后工作的解释语言。

ADA是一种可能性,但那里的工具和支持较少,更重要的是,明星人物并没有那么容易获得。

C++是一种可能性,但前提是严格执行子集。在这方面,它是魔鬼的工具,承诺让我们的生活更容易,但往往做得太多,

C是理想的。它非常成熟、快速,拥有一套多样化的工具和支持,很多有经验的开发人员都在那里,跨平台,并且非常灵活,可以在硬件附近工作。

我在从Smalltalk到Ruby的每一个领域都得到了发展,并且非常欣赏和享受高级语言所提供的一切。但是,当我进行关键系统开发时,我会咬紧牙关,坚持使用C。在我的经验中(国防和许多II级和III级医疗设备),少就多。

如果安全的话,我会去接哈斯克尔。我建议使用haskell,因为它具有非常严格的静态类型检查,并且它可以在构建部件时促进编程,使它们非常容易测试。

但我不太在乎语言。你可以得到更大的安全性,而不需要牺牲同样多的条件,让你的项目整体条件和工作没有最后期限。总的来说,所有的基本项目管理都到位了。我可能会集中精力进行广泛的测试,以确保一切正常工作,测试涵盖了所有的角落案例+更多。

语言和操作系统很重要,但是设计也很重要。尽量保持简陋,简单地说。

我将从最少的状态信息(运行时数据)开始,以最小化它变得不一致的可能性。然后,如果为了容错的目的想要有冗余,请确保有万无一失的方法从变得不一致的数据中恢复。没有办法从不一致中恢复的冗余只不过是在自找麻烦。

当请求的操作不能在合理的时间内完成时,总是有一个回退。正如他们在《空中交通管制》中所说,未经确认的通关是没有通关的。

不要害怕投票方法。它们简单可靠,即使它们可能会浪费几个周期。避免只依赖事件或通知的处理,因为它们很容易被删除、复制或排序错误。作为投票的附属物,他们很好。

我在阿波罗计划上的一个朋友曾经说,当他们决定依靠投票而不是事件时,他知道他们正在变得认真,即使计算机速度非常慢。

我刚刚读完了C++的飞行器标准。它们是可以的,但它们似乎假定将有许多类、数据、指针和动态内存分配。这正是绝对必要的。应该有一个拥有大镰刀的数据结构沙皇。

操作系统比语言更重要。使用实时内核,如vxworks或qnx。我们研究了控制工业机器人的方法,并决定使用VXWorks。我们使用C来进行实际的机器人控制。

对于真正关键的软件,如飞机自动着陆系统,您希望多个处理器独立运行以交叉检查结果。

实时环境通常有“安全关键”要求。对于这类事情,你可以看看 VxWorks 一个流行的实时操作系统。它目前正在许多不同领域使用,如波音飞机,宝马iDrive内部,RAID控制器和各种航天器。( Check it out )

VxWorks平台的开发可以使用多种工具来完成,其中包括 Eclipse , Workbench , SCORE 以及其他。支持C、C++、艾达和FORTRAN(是,FORTRAN),以及其他一些。

既然你不给一个平台,我就不得不说C/C++。在大多数实时平台上,无论如何,您的选择相对有限。

C倾向于让你自己陷入困境的缺点被验证代码的工具数量、代码的稳定性和直接映射到平台的硬件能力所抵消。此外,对于任何重要的事情,您将无法依赖未经广泛审查的第三方软件-包括大多数库-甚至硬件供应商提供的许多库。

因为一切都将由您负责,所以您需要一个稳定的编译器、可预测的行为和到硬件的紧密映射。

以下是一些我最近还没有讨论过的工具的更新,这些工具非常好。

The LLVM Compiler Infrastructure 在他们的主页上有一个简短的短文(包括C和C++的前端)。Java、Stand和其他语言的前端正在开发中;

编译器基础结构-llvm也是一个源代码集合, 实现语言和 汇编策略。初级 LLVM基础结构的组件 是基于GCC的C&+C++前端吗? 时间优化框架与 越来越多的全球和 程序间分析和 转换,静态后端 x86,x86-64,PowerPC 32/64,ARM, Thumb、IA-64、Alpha、SPARC、MIPS和 Cellspu架构,后端 它发出可移植的C代码, 用于x86、x86-64的实时编译器, PowerPC 32/64处理器,以及 用于MSIL的发射器。

VCC ;

VCC是一种证明正确性的工具。 注释的并发C程序或 发现问题。VCC扩展C 具有按合同设计的功能,例如 前置和后置以及类型 不变量。带注释的程序是 转换为逻辑公式使用 将它们传递给 要检查的自动SMT解算器Z3 它们的有效性。

VCC使用最近发布的 Common Compiler Infrastructure .

这两种工具,LLVM或VCC都是为支持多种语言和体系结构而设计的,我确实认为它们是通过契约和其他正式验证实践进行编码的一种增长。

WPF (而不是MS框架):如果您试图评估程序验证空间中的一些最新研究和工具,那么这是一个很好的开始。

WG23 但是,主要资源是当前和特定的 关键系统开发语言详细信息 . 它们涵盖了从艾达、C、C++、爪哇、C、脚本等各个方面。并且至少有一套适当的参考和指导,以更新语言特定缺陷和漏洞的信息。

一种强制使用谨慎模式的语言可能会有所帮助,但您可以使用任何语言(甚至汇编程序)强制使用谨慎模式。关于每个值的每个假设都需要测试假设的代码。例如,总是在除数之前测试除数是否为零。

您越信任可重用组件,任务就越容易,但可重用组件很少经过关键用途的认证,也无法通过监管安全流程。您应该使用一个很小的操作系统内核,然后构建用随机输入进行单元测试的小模块。像埃菲尔这样的语言可能会有所帮助,但没有什么好消息。

有很多很好的参考资料 http://www.dwheeler.com (高保证软件)。

有关汽车材料,请参见Misra C标准。但是你不能使用超过两级的指针,以及其他类似的东西。

adahome.com有关于ada的好信息。我喜欢这个C++到艾达教程: http://adahome.com/Ammo/cpp2ada.html

为了实现实时性,汤姆·霍金斯做了一些有趣的哈斯克尔的事情。请参阅:改进(语言结合了一个SMT解算器来检查验证条件)和Atom(EDSL用于不使用实际线程或任务的硬实时并发编程)。

任何软件产品都可以使用任何工具通过DO-178B认证过程,但问题是这有多困难。如果编译器没有经过认证,您可能需要证明您的代码在程序集级别是可跟踪的。因此,您的编译器经过认证是很有帮助的。我们在项目中使用了C,但必须在程序集级别进行验证,并使用代码标准,包括关闭优化器、限制堆栈使用、限制中断使用、透明可认证库等。ADA不是Pixie Dust,但它使PSAC计划看起来更可行。

随着应用程序越来越大,汇编代码就变得不那么可行了。ARM处理器只邀请C++,但是如果你问像Kiel这样的公司,他们的工具被认证了,他们会返回一个“HUH”?别忘了,验证工具也需要经过认证。尝试验证LabVIEW测试程序。

一个新的 Java安全关键标准 目前正在开发中- JSR 302: Safety Critical Java Technology .

这个 安全关键Java (SCJ)基于RTSJ的一个子集。目标是建立一个适用于安全关键认证(DO-178B,A级和其他安全关键标准)安全关键程序开发和分析的框架。

例如,SCJ删除了仍然存在于RTSJ中的堆,它还定义了应用程序和VM实现可能符合的3个符合性级别,定义了符合性级别以简化各种复杂应用程序的认证。

资源 :

• Java for Safety-Critical Applications.
• JSR 302:安全关键Java技术
• Developing Safety-Critical Applications with Java

HAL/S用于航天飞机。

我不知道我会用什么语言,但我知道我不会用什么语言:

关于Java支持的注意事项。软件产品可以包含对用Java编写的程序的支持。Java技术不是容错的,没有设计、制造或打算作为在线控制设备在危险环境中使用或转售,需要在核设施、航空器导航或通信系统、空中交通管制、直接生命支持机或武器系统的操作中使用故障安全性能。其中,Java技术的失败可能直接导致死亡、人身伤害或严重的物理或环境损害。