哪些语言用于安全
我正在研究安全关键型软件的开发，特别是编程语言选择对这种开发有什么影响。
请详细解释一下哪些语言是常用的，以及为什么。
Ada和SPARK（这是一种带有一些用于静态验证的挂钩的Ada方言）被用于航空航天领域，用于构建诸如航空电子系统等高可靠性软件。 这些语言有一些代码验证工具生态系统，尽管这种技术也适用于更多主流语言。
Erlang从根本上设计用于编写高可靠性电信代码。 它旨在便于分离错误恢复的问题（即生成错误的子系统与处理错误的子系统不同）。 它也可以受到正式的证明，尽管这种能力并没有真正走出研究界。
由于语言的声明性，Haskell等函数式语言可以通过自动化系统进行形式化证明。 这允许带有副作用的代码包含在monadic函数中。 为了证明形式的正确性，可以假定其余的代码除了指定的内容外什么也不做。
但是，这些语言是垃圾收集的，垃圾收集对代码是透明的，所以不能以这种方式推理。 垃圾收集语言对于硬实时应用程序来说通常不足以预测，尽管在时间有限的增量垃圾收集器方面正在进行一系列研究。
Eiffel及其后代内置了对称为Design By Contract的技术的支持，该技术提供了一种强大的运行时机制，用于合并不变量的预检查和后检查。 虽然艾菲尔从未真正发现过，但开发高可靠性软件往往包括在实际编写功能之前预先编写检查和处理故障模式的处理程序。
虽然C和C ++不是专门为这种类型的应用程序设计的，但出于多种原因，它们广泛用于嵌入式和安全关键型软件。 注意的主要属性是控制内存管理（例如，您可以避免垃圾收集），简单，调试良好的内核运行时库和成熟的工具支持。 目前使用的许多嵌入式开发工具链最初是在20世纪80年代和90年代开发的，当时这种技术来自当时流行的Unix文化，所以这些工具在这类工作中仍然很流行。
虽然必须仔细检查手动内存管理代码以避免错误，但它可以对应用程序响应时间进行一定程度的控制，而这对于依赖垃圾回收的语言来说是不可用的。 C和C ++语言的核心运行时库相对简单，成熟且易于理解，因此它们是最稳定的平台之一。 大部分（如果不是全部）用于Ada的静态分析工具也支持C和C ++，并且还有许多其他此类工具可用于C.还有一些广泛使用的基于C / C ++的工具链; 用于Ada的大多数工具链也都支持C和/或C ++版本。
诸如公理化语义（PDF），Z符号或通信连续过程等形式化方法允许对程序逻辑进行数学验证，并且通常用于安全关键软件的设计，其中应用程序足够简单以应用它们（通常是嵌入式控制系统） 。 例如，我的一位前任讲师为德国铁路网做了一个正式的信号系统正确性证明。
形式化方法的主要缺点是它们倾向于在被证明的基础系统方面复杂度呈指数级增长。 这意味着证据中存在重大错误风险，所以它们实际上仅限于相当简单的应用。 形式化方法被广泛用于验证硬件的正确性，因为硬件错误的修复非常昂贵，特别是在大众市场产品上。 自从Pentium FDIV出现问题以来，形式化方法已经获得了相当多的关注，并被用于验证自Pentium Pro以来所有Intel处理器上FPU的正确性。
许多其他语言已被用于开发高度可靠的软件。 关于这个问题已经做了大量的研究。 人们可以合理地认为方法论比平台更重要，尽管有简单性，选择性和控制依赖性等原理可能会妨碍某些平台的使用。
正如其他人已经指出的那样，某些操作系统平台具有促进可靠性和可预测行为的功能，例如看门狗定时器和有保证的中断响应时间。 简单性也是可靠性的强大推动力，许多RT系统都被故意保持非常简单和紧凑。 QNX（我熟悉的唯一一个这样的操作系统，曾经使用基于它的混凝土配料系统）非常小，并且可以放在一张软盘上。 出于类似的原因，制作OpenBSD的人 - 以其强大的安全性和全面的代码审计功能而闻名 - 也能够让系统变得简单。
编辑：这篇文章有一些关于安全关键软件的好文章的链接，特别是Here and Here。 支持S.Lott和Adam Davis的来源。 THERAC-25的故事是该领域的一个经典作品。
对于C ++，联合攻击战斗机（F-35）C ++编码标准是一个很好的解读：
http://www.stroustrup.com/JSF-AV-rules.pdf
我相信Ada仍然在一些安全和/或任务关键的政府项目中使用。 我从来没有使用过这种语言，但它与我的“学习”清单一起，还有埃菲尔。 艾菲尔提供Design By Contract，旨在提高可靠性和安全性。
链接地址: http://www.djcxy.com/p/79149.html