哪些语言用于安全关键软件？[关闭]
https://stackoverflow.com/questions/243387
-
04-07-2019 - |
italiano
english
français
española
中国
日本の
العربية
Deutsch
한국어
Português
Russian题
我正在研究安全关键软件的开发，特别是编程语言的选择对此类开发的影响。
请详细解释哪些语言是常用的以及原因。
解决方案
Ada 和 SPARK （这是一种带有静态验证钩子的Ada方言）被用于航空航天领域，用于构建航空电子系统等高可靠性软件。有一些这些代码验证工具的生态系统虽然这种技术也适用于更多主流语言。
Erlang 编写高可靠性电信代码。它被设计用于促进错误恢复的关注点的分离（即，生成错误的子系统与处理错误的子系统不同）。它也可以接受正式的证明，尽管这种能力并没有真正远离研究界。
功能语言，例如 Haskell 可以通过自动系统进行正式证明，因为声明性质。这允许具有副作用的代码包含在monadic函数中。对于正式的正确性证明，可以假设其余代码除了指定的内容之外什么都不做。
但是，这些语言是垃圾收集的，垃圾收集对代码是透明的，因此不能以这种方式进行推理。垃圾收集语言对于硬实时应用程序通常不足以预测，尽管有时正在研究时间限制增量垃圾收集器。
Eiffel 及其后代内置支持名为
虽然 C 和 C ++ 并非专为此类应用而设计，由于多种原因，它们被广泛用于嵌入式和安全关键型软件。注意的主要属性是控制内存管理（例如，允许您避免垃圾收集），简单，良好调试的核心运行时库和成熟的工具支持。当今使用的许多嵌入式开发工具链最初是在20世纪80年代和90年代开发的，当时这是当前的技术并且来自当时流行的Unix文化，所以这些工具在这类工作中仍然很受欢迎。 p>
虽然必须仔细检查手动内存管理代码以避免错误，但它允许对a进行一定程度的控制应用响应时间不适用于依赖于垃圾回收的语言。 C和C ++语言的核心运行时库相对简单，成熟且很好理解，因此它们是最稳定的平台之一。大多数（如果不是全部）用于Ada的静态分析工具也支持C和C ++，并且有很多 C可用的其他此类工具。 还 几个 广泛 使用过的 C / C ++ 基于 工具 链;用于Ada的大多数工具链也有支持C和/或C ++的版本。
正式方法，例如 Axiomatic Semantics （PDF）， Z符号 或通信顺序流程允许对程序逻辑进行数学验证，并经常用于安全设计应用程序足够简单以应用它们的关键软件（通常是嵌入式控制系统）。例如，我之前的一位讲师做了信号系统的正式正确性证明为德国铁路网络。
正式方法的主要缺点是它们在被证明的基础系统方面的复杂性呈指数增长趋势。这意味着证明存在重大错误风险，因此它们实际上仅限于相当简单的应用程序。正式方法被广泛用于验证硬件的正确性，因为硬件错误的修复非常昂贵，特别是在大众市场产品上。自 Pentium FDIV bug 以来，正式的方法引起了很多关注，并且已经用于验证自Pentium Pro以来所有英特尔处理器上FPU的正确性。
许多其他语言已用于开发高度可靠的软件。 已就此主题进行了大量研究。有人可以合理地争辩说方法比平台更重要尽管有简单性以及依赖性的选择和控制等原则可能会使排除使用某些平台。
正如其他许多人所指出的那样，某些O / S平台具有提升可靠性和可预测行为的功能，例如看门狗定时器和保证的中断响应时间。小号
其他提示
对于C ++，联合攻击战斗机（F-35）C ++编码标准是一个很好的阅读：
我相信 Ada 仍然在一些安全和政府项目中使用/或任务关键。我从来没有使用过这种语言，但是在我的“学习”列表中，还有埃菲尔。 Eiffel提供Design By Contract，旨在提高可靠性和安全性。
首先，安全关键软件遵循您在经典机械和电气工程领域中看到的相同原则。冗余，容错和故障安全。
顺便说一句，正如之前的海报提到的那样（并且由于某种原因被低估），能够实现这一目标的最重要的一个因素是让你的团队对所有的东西有一个坚如磐石的理解。继续毫无疑问，良好的软件设计是关键。但它也意味着一种可访问，成熟且得到良好支持的语言，其中有许多公共知识和经验丰富的开发人员可用。
许多海报已经评论说，操作系统是这方面的关键因素，这是非常正确的，因为它必须是确定性的（参见QNX或VxWorks）。这排除了大多数为你幕后做事的解释性语言。
ADA是一种可能性，但是那里的工具和支持较少，更重要的是，人们并不那么容易获得。
C ++是一种可能性，但前提是您严格执行子集。在这方面，它是魔鬼的工具，承诺让我们的生活更轻松，但往往做得太多，
C是理想的。它非常成熟，快速，拥有多样化的工具和支持，许多经验丰富的开发人员在那里，跨平台，而且极其灵活，可以靠近硬件工作。
我开发了从smalltalk到ruby的所有东西，欣赏并享受高级语言提供的一切。但是，当我正在进行关键系统开发时，我会咬紧牙关并坚持使用C.根据我的经验（防御和许多II级和III级医疗设备），更少。
如果它比其他一切安全的话，我会选择haskell。我建议使用haskell，因为它具有非常严格的静态类型检查，并且它促进了编程，在这种编程中，您可以非常容易地测试它们。
但后来我不太关心语言。通过让您的项目整体处于有条件状态并且没有最后期限的工作，您可以获得更高的安全性而不会影响太多。总体而言，所有基本项目管理都已到位。我可能会集中精力进行广泛的测试，以确保一切都像它应该的那样，测试覆盖所有角落情况+更多。
语言和操作系统很重要，但设计也是如此。尽量保持简单，简单易行。
我首先要获得最少的状态信息（运行时数据），以尽量减少它变得不一致的可能性。然后，如果您希望为容错目的而拥有冗余，请确保您有简单的方法从数据中恢复不一致。没有办法从不一致中恢复的冗余只是在寻找麻烦。
在请求的操作未在合理时间内完成时，始终有后备。正如他们在空中交通管制中所说的那样，未经确认的许可是没有许可的。
不要害怕投票方法。它们简单可靠，即使它们可能浪费几个周期。回避仅依赖于事件或通知的处理，因为它们很容易丢弃，重复或错误。作为民意调查的辅助手段，他们没事。
我的一位APOLLO项目的朋友曾经说过，当他们决定依靠投票而不是事件时，他知道他们会变得严肃，即使计算机速度非常慢。
P.S。我刚刚阅读了C ++ Air Vehicle标准。它们没问题，但它们似乎假设会有很多类，数据，指针和动态内存分配。这正是应该没有绝对必要的东西。应该有一个带有大镰刀的数据结构沙皇。
操作系统比语言更重要。使用实时内核，如VxWorks或QNX。我们研究了控制工业机器人的问题，并决定选择VxWorks。我们使用C进行实际的机器人控制。
对于真正关键的软件，例如飞机自动着陆系统，您需要独立运行多个处理器以交叉检查结果。
由于你没有提供平台，我不得不说C / C ++。在大多数实时平台上，无论如何，你的选项都相对有限。
C倾向于让你自己射击的缺点被用于验证代码的工具数量以及代码的稳定性和直接映射到平台的硬件功能所抵消。此外，对于任何关键的事情，您将无法依赖尚未经过广泛审查的第三方软件 - 这包括大多数库 - 甚至包括硬件供应商提供的许多库。
由于一切都是您的责任，您需要稳定的编译器，可预测的行为以及与硬件的紧密映射。
这里有一些我尚未见过的工具的更新，我最近一直在玩这些相当不错的工具。
LLVM编译器基础结构，主页上的简短介绍（包括C和C ++的前端。 -End for Java，Scheme和其他语言正在开发中）;
编译器基础结构 - LLVM也是源代码的集合 实现语言和 编制策略。首要的 LLVM基础结构的组件 是一个基于GCC的C＆amp; C ++前端，a 链接时优化框架 越来越多的全球和 过程间分析和 转换，静态后端 X86，X86-64，PowerPC 32/64，ARM， 拇指，IA-64，Alpha，SPARC，MIPS和 CellSPU架构，后端 它发出便携式C代码，和 适用于X86，X86-64的即时编译器， PowerPC 32/64处理器，以及 MSIL的发射器。
VCC ;
VCC是一种证明正确性的工具 注释并发C程序或 发现问题。 VCC扩展了C. 通过合同特征设计，如 前后条件以及类型 不变量。带注释的程序是 使用转换为逻辑公式 Boogie工具，将它们传递给 一个自动SMT求解器Z3来检查 他们的有效性。
VCC使用最近发布的通用编译器基础结构。
这两个工具，LLVM或VCC都是为支持多种语言和架构而设计的，我确实认为它们是通过合同和其他形式验证实践进行编码的。
WPF （不是MS框架:)，如果你想尝试的话，这是一个很好的起点评估程序验证空间中的一些最新研究和工具。
WG23 是主要资源，但对于当前和特定的关键系统开发语言详细信息。它们涵盖了Ada，C，C ++，Java，C＃，Scripting等所有内容......并且至少提供了一套不错的参考和指导，以指导更新有关语言特定缺陷和漏洞的信息。
http://www.dwheeler.com 上有很多很好的参考资料（“保证软件“）。
对于汽车用品，请参阅MISRA C标准。 C但你不能使用两个以上的指针级别，以及其他类似的东西。
adahome.com有关于Ada的良好信息。我喜欢这个C ++到Ada的教程： http://adahome.com/Ammo/cpp2ada.html
对于硬实时，Tom Hawkins做了一些有趣的Haskell。请参阅：ImProve（语言包含用于检查验证条件的SMT求解器）和Atom（用于硬实时并发编程的EDSL，无需使用实际线程或任务）。
强加模式的语言可能会有所帮助，但您可以使用任何语言（甚至是汇编程序）强加小心模式。关于每个值的每个假设都需要用于测试假设的代码。例如，在除法之前总是将除数除以零。
您可以信任的可重用组件越多，任务就越容易，但可重用组件很少被认证用于关键用途，并且无法帮助您完成监管安全流程。您应该使用一个微小的操作系统内核，然后构建使用随机输入进行单元测试的微型模块。像埃菲尔这样的语言可能有所帮助，但没有银弹。
任何软件产品都可以使用任何工具通过DO-178b认证流程，但问题是它有多难。如果编译器未经过认证，您可能需要证明您的代码在程序集级别是可跟踪的。因此，对您的编译器进行认证很有帮助。我们在项目中使用了C，但是必须在汇编级别进行验证并使用代码标准，包括关闭优化器，有限的堆栈使用，有限的中断使用，透明的可认证库等.ADA不是小精灵尘埃，但它使得PSAC计划看起来更容易实现。
随着应用程序变大，汇编代码变得不那么可行。 ARM处理器只是邀请C ++，但是如果你问像Kiel这样的公司，他们的工具是经过认证的，那么他们将返回“huh？”。不要忘记，验证工具也需要经过认证。尝试验证LabView测试程序。
一个新的 Java 的安全关键标准 目前正在开发中—— JSR 302：安全关键的 Java 技术.
这 安全关键的 Java (SCJ) 基于 RTSJ 的子集。目标是建立一个适合安全关键认证（DO-178B、A 级和其他安全关键标准）的安全关键程序的开发和分析的框架。
例如，SCJ 删除了 RTSJ 中仍然存在的堆，它还定义了应用程序和 VM 实现都可以符合的 3 个合规级别，定义合规级别是为了简化各种复杂应用程序的认证。
资源:
我不知道我会使用什么语言，但我确实知道我不会使用哪种语言：
关于JAVA支持的说明。该软件产品可能包含对JAVA中编写的程序的支持。 JAVA技术不是容错的，并非设计，制造或有意使用或转售为危险环境中的在线控制设备，需要无故障安全性能，如核设施，飞机导航或通信系统的运行，空气交通控制，直接生命支持机器或武器系统，其中JAVA技术的失败可能导致死亡，人身伤害或严重的物理或环境损害。
HAL / S用于航天飞机。
