我正在研究安全关键软件的开发,特别是编程语言的选择对这种开发的影响.
请详细说明常用的语言及其原因.
Ada和SPARK(这是一种带有静态验证钩子的Ada方言)被用于航空航天领域,用于构建航空电子系统等高可靠性软件.这些语言有一些代码验证工具生态系统,尽管这种技术也适用于更多主流语言.
二郎是从地面设计为撰写高可靠性的电信码.它旨在促进错误恢复的关注点分离(即生成错误的子系统与处理错误的子系统不同).它也可以接受正式证明,尽管这种能力并没有真正远离研究界.
由于语言的声明性,Haskell等功能语言可以通过自动化系统进行形式化证明.这允许具有副作用的代码包含在monadic函数中.对于正式的正确性证明,可以假设其余代码除了指定的内容之外什么都不做.
但是,这些语言是垃圾收集的,垃圾收集对代码是透明的,因此无法以这种方式进行推理.垃圾收集语言对于硬实时应用程序通常不足以预测,尽管有时正在研究时间限制增量垃圾收集器.
Eiffel及其后代内置了对Design By Contract技术的支持,该技术提供了一种强大的运行时机制,用于合并不变量的前后检查. 虽然Eiffel从未真正流行起来,但开发高可靠性软件往往包括在实际编写功能之前预先为故障模式编写检查和处理程序.
尽管C和C++并非专门针对此类应用而设计,但由于多种原因,它们被广泛用于嵌入式和安全关键型软件.注意的主要属性是对内存管理的控制(例如,它允许您避免垃圾收集),简单,良好调试的核心运行时库和成熟的工具支持.当今使用的许多嵌入式开发工具链最初是在20世纪80年代和90年代开发的,当时这是当前的技术并且来自当时流行的Unix文化,因此这些工具在这类工作中仍然很受欢迎.
虽然必须仔细检查手动内存管理代码以避免错误,但它允许对应用程序响应时间进行一定程度的控制,这是依赖于垃圾收集的语言所不具备的.C和C++语言 的核心运行时库相对简单,成熟且易于理解,因此它们是最稳定的平台之一.大多数(如果不是全部)用于Ada的静态分析工具也支持C和C++,还有许多其他此类工具可用于C语言.有也 几个 广泛 使用的 C/C++ 基于 工具 链 ; 用于Ada的大多数工具链也有支持C和/或C++的版本.
诸如Axiomatic Semantics(PDF),Z Notation 或Communicating Sequential Processes之类的形式化方法允许对程序逻辑进行数学验证,并且通常用于安全关键软件的设计,其中应用程序足够简单以应用它们(通常是嵌入式控制系统) .例如,我以前的一位讲师对德国铁路网的信号系统进行了正式的正确性证明.
形式方法的主要缺点是它们在被证明的基础系统方面呈指数级增长的趋势.这意味着证明存在重大错误风险,因此它们实际上仅限于相当简单的应用程序.正式方法被广泛用于验证硬件的正确性,因为硬件错误的修复非常昂贵,特别是在大众市场产品上.自Pentium FDIV漏洞以来,正式方法已经引起了很多关注,并且自Pentium Pro以来已被用于验证所有Intel处理器上FPU的正确性.
许多其他语言已被用于开发高度可靠的软件. 关于这个问题已经做了很多研究. 可以合理地论证方法比平台更重要,尽管有简单和选择以及依赖关系控制等原则可能会妨碍使用某些平台.
正如其他许多人所指出的那样,某些O/S平台具有提升可靠性和可预测行为的功能,例如看门狗定时器和保证的中断响应时间.简单性也是可靠性的强大驱动力,并且许多RT系统被故意保持非常简单和紧凑. QNX(我熟悉的唯一这样的O/S,曾经使用过基于它的混凝土配料系统)非常小,适合单张软盘.出于类似的原因,制作OpenBSD的人- 以其强大的安全性和彻底的代码审计而闻名 - 也不遗余力地保持系统简单.
编辑: 这篇文章有一些链接到关于安全关键软件的好文章,特别是这里和这里.向S.Lott和Adam Davis道具的道具.THERAC-25的故事在这个领域是一个经典的作品.
对于C++,联合攻击战斗机(F-35)C++编码标准是一个很好的阅读:
http://www.stroustrup.com/JSF-AV-rules.pdf
我相信Ada仍然在一些安全和/或关键任务的政府项目中使用.我从来没有使用过该语言,但它和我一起在"学习"列表中,还有埃菲尔.Eiffel提供Design By Contract,旨在提高可靠性和安全性.
首先,安全关键软件遵循您在经典机械和电气工程领域中看到的相同原理.冗余,容错和故障安全.
顺便说一句,正如之前的海报所暗示的那样(并且由于某种原因被低估),能够实现这一目标的最重要因素是让您的团队对所发生的一切事情有一个坚如磐石的理解.毫无疑问,良好的软件设计是关键.但它也意味着一种可访问,成熟且得到良好支持的语言,其中有许多公共知识和经验丰富的开发人员可用.
许多海报已经评论说,操作系统是这方面的关键因素,这一点非常正确,因为它必须是确定性的(参见QNX或VxWorks).这排除了大多数为您幕后操作的解释语言.
ADA是一种可能性,但是那里的工具和支持较少,更重要的是,人们并不那么容易获得.
只有在严格执行子集时才有可能使用C++.在这方面它是魔鬼的工具,承诺让我们的生活更轻松,但往往做得太多,
C是理想的.它非常成熟,快速,拥有多样化的工具和支持,许多经验丰富的开发人员在那里,跨平台,而且极其灵活,可以靠近硬件工作.
我开发了从smalltalk到ruby的所有东西,欣赏并享受高级语言提供的一切.但是,当我正在进行关键系统开发时,我会咬紧牙关并坚持使用C.根据我的经验(防御和许多II级和III级医疗设备),更少.
如果它比其他一切安全的话,我会选择haskell.我建议使用haskell,因为它具有非常严格的静态类型检查,并且它促进了编程,在这种编程中,您可以非常容易地测试它们.
但后来我不太关心语言.通过让您的项目整体处于有条件状态并且没有最后期限的工作,您可以获得更高的安全性而不会影响太多.总体而言,所有基本项目管理都已到位.我可能会专注于广泛的测试,以确保一切都像它应该的那样,测试涵盖所有角落案例+更多.
语言和操作系统很重要,但设计也是如此.尽量保持简单,简单易行.
我将从最少的状态信息(运行时数据)开始,以最小化它变得不一致的可能性.然后,如果您希望为容错目的而拥有冗余,请确保您有简单的方法从数据中恢复不一致.没有办法从不一致中恢复的冗余只是在寻找麻烦.
当请求的操作未在合理的时间内完成时,始终有后备.正如他们在空中交通管制中所说的那样,一个未经确认的许可是没有许可的.
不要害怕投票方法.它们简单可靠,即使它们可能浪费几个周期.回避仅依赖于事件或通知的处理,因为它们很容易丢弃,重复或错误.作为民意调查的辅助手段,他们没事.
我的一位APOLLO项目的朋友曾经说过,他知道当他们决定依靠投票而不是事件时他们会变得严肃起来,即使计算机速度非常慢.
PS我刚刚阅读了C++ Air Vehicle标准.它们没问题,但它们似乎假设会有很多类,数据,指针和动态内存分配.这正是应该没有绝对必要的东西.应该有一个带有大镰刀的数据结构沙皇.
操作系统比语言更重要.使用实时内核,如VxWorks或QNX.我们研究了控制工业机器人的问题,并决定选择VxWorks.我们使用C进行实际的机器人控制.
对于真正关键的软件,例如飞机自动着陆系统,您需要独立运行多个处理器来交叉检查结果.
实时环境通常具有"安全关键"要求.对于那种事情,你可以看一下流行的实时操作系统VxWorks.它目前在许多不同的领域使用,如波音飞机,宝马iDrive内部,RAID控制器和各种航天器.(看看吧.)
VxWorks平台的开发可以使用多种工具完成,其中包括Eclipse,Workbench,SCORE等.支持C,C++,Ada和Fortran(是的,Fortran)以及其他一些.
既然你没有提供平台,我就不得不说C/C++.在大多数实时平台上,无论如何,您的选项相对有限.
C倾向于让你自己在脚下射击的缺点被验证代码的工具数量以及代码的稳定性和直接映射到平台的硬件功能所抵消.此外,对于任何关键的事情,您将无法依赖尚未经过广泛审查的第三方软件 - 这包括大多数库 - 甚至包括硬件供应商提供的许多库.
由于一切都是您的责任,因此您需要稳定的编译器,可预测的行为以及与硬件的紧密映射.
这里有一些我尚未见过的工具的更新,我最近一直在玩这些相当不错的工具.
LLVM编译器基础结构,主页上的简短介绍(包括C和C++的前端.用于Java,Scheme和其他语言的前端正在开发中);
编译器基础结构 - 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,如前后条件以及类型不变量.使用Boogie工具将带注释的程序转换为逻辑公式,该工具将它们传递给自动SMT求解器Z3以检查其有效性.
VCC使用最近发布的Common Compiler Infrastructure.
这两个工具,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
对于硬实时性，汤姆·霍金斯做了一些有趣的Haskell东西。请参阅：ImProve（语言包含SMT求解器以检查验证条件）和Atom（EDSL用于不使用实际线程或任务的硬实时并发编程）。
京公网安备 11010802040832号 | 京ICP备19059560号-6 