• 中文
    • English
  • 注册
  • 查看作者
  • 和Rust一样好,编程更安全?三年实践、员工态度反转,英伟达用 SPARK 换掉 C

     

    近日,知名编程语言 Ada 与
    所属公司 AdaCore 表示,
    的产品运行着许多经过正式验证的 SPARK 代码。对于安全较为敏感的应用程序或组件,英伟达安全团队正在用 SPARK 语言取代

     

    在将 SPARK 模块与 C 中的等效模块进行了比较后,英伟达首席软件工程师 Cameron Buschardt 表示,SPARK 生成的程序集几乎与 C 代码中的程序集相同,“我根本没有看到任何性能差异。”

    为什么选择SPARK

     

    英伟达虽以GPU闻名,但也参与嵌入式系统,并为GPU本身编写固件。这是安全关键代码。安全对英伟达至关重要,但当前的网络环境并不安全:针对固件和硬件的网络攻击呈上升趋势,但开发和验证生态系统没有跟上这些攻击的规模,同时全行业缺乏安全代码设计人员和软件安全从业人员。这些让英伟达面临着既要提供更安全的产品⼜不会⼤幅增加开发时间和成本的挑战。

     

    在全面审视自家软件开发方法后,英伟达思考哪些方面还需要改进,也因此英伟达开始注意到在开发关键嵌入式应用程序时,使用传统语言和工具集所带来的相应成本:

     

     

    英伟达软件安全副总裁 Daniel Rohre 坦言,“我们还是喜欢可量化的结果。”不过如何把这样一个难以量化、甚至不知道是否最终完成的问题,转化成能以数字衡量的明确答案,是摆在英伟达软件安全团队前面的一大难题。

     

    在查看了各种可实现量化的方法后,团队很快意识到不少方案需要依托于数学计算和形式证明,这类工具在过去十年间还发生了重大变化。

     

    “我们希望接下来的验证以可证明性作为起点,而不再满足于‘已经测试过了’。安全性是几乎无法测试验证的,因为根本就没有终极可靠的标准。”Rohrer表示,而形式证明则带来了强大的吸引力,能帮助英伟达确信其产品中不存在运行时错误和其他一些常见安全漏洞,且程序功能符合既定规范。

     

    “我们能不能调整基本方法?如果可以,具体要使用哪些工具?”这些问题,就成了软件安全团队接下来的工作重点。

     

    作为回应,安全团队给出的答案在 Rohrer 看来颇为“离经叛道”:如果我们不再用C语言,结果会如何?于是新的问题又冒了出来:还有哪些替代语言和工具,可以支持这些形式化方法?

     

    在追寻答案的过程中,英伟达发现了SPARK。

     

    SPARK是一种高级计算机编程语言,由定义明确的Ada子集组成。与之前的Ada一样,SPARK就是为开发高完整性软件而生,强调以可预测且高度可靠的状态运行。SPARK还提供一种名为“契约”(contract)的语言特性,能够为组件指定适用于静态验证的形式方法。

     

    英伟达首席软件工程师、首批SPARK用户之一Dhawal Kumar表示,“从编程语言功能的角度来看,这些范式跟C和C++非常相似。SPARK是一种命令式编程语言,可用于编写面向过程或面向对象的代码,也有不少大型编程工具可供选择。”

     

    归功于其独特设计,SPARK开发的代码中不会存在未定义的行为。该语言带有一组内置检查,能确保代码遵守所有规则,因此不会发生运行时错误(例如缓冲区溢出)。

     

    SPARK的另一个关键特性就是支持形式验证。换句话说,通过使用SPARK和形式方法求解器,即可在数学上证明我们的SPARK代码行为完全符合规范。这样的过程,就被称为形式验证。

     

    Dhawal Kumar解释道,“SPARK具备大多数其他编程语言所没有的功能,即在代码本体内指定程序要求、并使用相关工具集来确保这种合规性。简单来讲,这就是证明程序正确无误的能力。这一点非常重要。”

     

    总的来说,SPARK最能吸引英伟达的优势包括:

     

    • SPARK具有确定性。也就是说,形式证明可以确切消除运行时错误、保障规范合规。

    • SPARK代码能够与C链接。就是说英伟达不必一次性重新编码所有内容或非关键组件。SPARK组件能够被轻松集成至C/C++环境当中,这样英伟达就能灵活选择需要把哪些部分转化为能够形式验证的SPARK形式。

    • SPARK拥有可靠的生态系统。SPARK的根源语言Ada本身就非常成熟,而且自1980年代以来经历过多次升级。开发者可以通过AdaCore(Ada和SPARK的全球权威机构)及其他组织轻松获得一流支持工具。此外,Ada和SPARK还拥有上游开源软件(OSS)。

     

    概念验证:安全应用中比C/C++更优秀

     

    2018年第四季度,英伟达开展了概念验证(POC)演习,希望深入研究SPARK语言、相关工具和可用的技术支持,借此确认其是否总体适用于英伟达的应用场景。

     

    在初始概念验证中,英伟达软件安全团队将SPARK引入了两款应用程序:其一是裸机应用程序,充当其他几块安全处理器上所运行代码的信任根;其二则是实时操作系统(RTOS)应用,负责处理保护区域的大小调整。

     

    概念验证团队在三个月内将两套代码库的几乎所有代码都由C转换成了SPARK。之后团队发现,两款应用程序的安全性和稳健性都有了重大改进。由于SPARK出色的稳健性,加上将程序属性表示为“契约”的设计,英伟达发现新程序能够大大减少安全介入需求。另外,开发团队实际上很容易适应这种新的语言和工具。

     

    与安全评估员一道完成结果审查之后,英伟达还发现SPARK完全可以在安全环境下与C代码混合使用。更重要的是,安全评估员认为SPARK不仅表现过关,而且只要开发者接受过充足的培训,其在安全关键型应用程序中的表现甚至比C/C++更优秀。

     

    概念验证团队还根据测试结果评估了投资回报率(ROI),得出的结论是由SPARK转换带来的工程成本(培训、实验、新工具获取等)可以被应用程序的安全性和验证效率提升所抵消,因此转向SPARK将大有可为。

     

    最后英伟达得出结论,SPARK的支持基础设施非常出色。

     

    落地实践:受到工程师好评

     

    概念验证完成之后,英伟达决定立刻将SPARK的成本节约与功能提升实践落地。从2019年开始,英伟达在其安全策略中为指定的固件使用SPARK。与此同时,英伟达还开始培训更多SPARK开发人员,并最终建立起内部培训计划。随着公司内部SPARK专业知识的积累,语言转换成本将逐渐被抵消。

     

    目前,多个英伟达团队正将SPARK引入众多应用程序,包括整体GPU固件镜像、BootROM和安全监控程序固件中的镜像身份验证与完整性检查,以及用于嵌入式操作系统的隔离内核中的形式验证组件等等。

     

    总体来看,目前的改造目标仍然是体量较小的代码,但这也是SPARK强类型、无运行时错误且在某些情况下可实现严格形式验证等优势的绝佳场景。

     

    另外在量化采用SPARK带来的好处方面,英伟达的工程经理们纷纷表示,SPARK提供的理论保证帮助他们增强了对产品质量的信心。

     

    英伟达公司GPU软件安全高级经理James Xu的团队的职责是,确保英伟达GPU中的软件和固件处于行业领先的安全水平。

     

    Xu 解释称,“我们之所以使用SPARK,主要原因就是它能提供严格保证。其中一大关键价值就是不存在运行时错误。要知道,能相信自己的代码可以直接回避掉大多数常见陷阱,这可是很有吸引力的。在使用SPARK编码时,我们往往更有信心,因为这种语言本身就能防止人们犯下C语言编程时一些常见的错误。”

     

    作为英伟达GPU固件安全团队负责人,Varun Kumar 的团队负责GPU组件的初始化和启动、安全引导、固件更新以及设备恢复证明等。如今 Kumar 带领着20名工程师按照NIST SP800-193平台固件弹性指南开发SPARK组件。他表示,Xu提到的这些特性对于他们这些客户安全保障人士也很有吸引力。

     

    与James Xu和Varun Kumar团队使用SPARK开发新组件不同,Cameron Buschardt 的主要工作是用 SPARK 编写出与 C 版本等效的模块。从结果来看,SPARK 版既未出现代码膨胀、也不存在性能降级。他表示,“由SPARK编写成的程序集几乎跟C语言版本完全相同。我没有发现任何性能差异,而且因为所有属性都得到了严格证明,所以我们压根不需要启用运行时检查。”

     

    内部开发者:从怀疑到支持

     

    虽然现在看着效果不错,但 SPARK 的推广工作起初并不顺利,不少开发者和工程经理对其多少是抵触的。James Xu认为这些都源自于对未知的担忧,工程技术和行政管理团队都有各自担忧的事情。

     

    “Ada和SPARK在某些领域缺乏知名度,所以人们会担心未来会不会影响工程资源的扩展能力、会不会影响到开发计划、会不会很难得到可靠的技术帮助等。虽然消除运行时错误这点听起来不错,但真能在实践中落地吗?对于逻辑错误,SPARK又有哪些优势?另外,考虑到对这种语言并不熟悉,人们天然会觉得从C到SPARK会严重拖慢开发进度。”

     

    英伟达用事实回应了大部分质疑。在培训方面,英伟达最初直接使用 AdaCore 提供的课程,不久之后便开发出了自己的内部培训计划。很快,参与学习的开发者数量就迅速增加。

     

    事实证明,语言转换带来的影响远不像想象中那么严重。

     

    James Xu当初曾猜测SPARK的开发周期可能是C语言的两倍。但后来他发现,只要保证只在隔离良好且规模较小(但更有价值)的范围内使用SPARK,那实际影响就可以“几乎忽略不计”。Xu还强调,“有些开发者还担心项目进度会大大减缓,甚至觉得预算可能会超支。但事实证明这都不是问题。

     

    在亲眼目睹了SPARK和形式化方法对工作和客户关系产生的积极影响之后,很多此前抱有怀疑态度的工程师迅速转变成了热情的支持者。

     

    “说实话,刚开始那会我也非常怀疑。我在SPARK中第一次尝试证明非平凡算法,结果简直糟透了。但在经历了初步学习之后,我又对SPARK那种严格的可证明性无比钦佩。”Cameron Buschardt 表示,“SPARK不仅允许我们构建一个组件,还承诺帮我们证明它的完备性。
    这是一场变革,是其他任何语言都无法带来的至高信任。

     

    从怀疑到支持的英伟达工程师有很多。Rohrer表示,只要大家愿意直面挑战、亲身尝试,那么在克服了最初的思维惯性之后,他们就会意识到转向SPARK确实具有打破传统的变革性意义。

     

    结束语

     

    自最初部署以来,SPARK以及为其构建的形式化方法工具开始在英伟达内部快速传播和普及。

     

    在2018年底第一期概念验证结束时,英伟达里接受过SPARK培训的开发者只有5人。但到2022年第二季度,这个数字已经增长到50以上。在此期间,英伟达用SPARK实现了诸多组件,其中包括其GPU固件镜像中的各种组件、硬件引导ROM的组件,以及用于简化嵌入式操作系统内核证明的几个库。

     

    如今,许多英伟达产品都附带有SPARK组件,公司内部对这种语言的认识和兴趣也在持续增长。

     

    Buschardt表示,“我们最初用小规模概念验证证明自己,随后又用SPARK实现了规模更大的启动固件。这也向英伟达的其他团队证明,SPARK完全可以用来构建固件或者其他类似用例。它在架构讨论中出现得越来越频繁。还有客户经常讨论的关键安全属性,有了SPARK的支持,我们可以向客户证明这种安全保障不只是口头承诺、而是原理层面的严格证明。”

     

    同样消除了很多C 中易犯错误的 Rust,现在备受关注。人们难免会对这两种语言进行对比。众所周知 Rust 很难学习,SPARK 相对可能更容易些,特别是对于熟悉嵌入式编程的人。另外,Rust 专注于内存安全,而 SPARK 专注于经过验证的正确性。

     

    对于英伟达选择SPARK, AdaCore表示,“这是正确的”,并为未来选择使用SPARK的开发者铺平了道路。

     

     

     

    参考链接:

  • 0
  • 0
  • 0
  • 302
  • 请登录之后再进行评论

    登录
  • 任务
  • 实时动态
  • 发布
  • 单栏布局 侧栏位置: