【形式化验证】在汽车网络及功能安全研发发挥重要作用

形式化验证 （Formal Verification）有望在汽车安全中发挥越来越重要的作用，这是基于它已经在安全关键型应用中的广泛使用。

形式已成为汽车半导体验证的重要组成部分。甚至在ADAS和半自动驾驶汽车问世之前，例如ISO 26262之类的功能安全规范和ISO / SAE 21434之类的网络安全规范，汽车中的数字系统内容都在迅速增长。多年来，诸如博世和英飞凌等领先的汽车IC提供商一直在使用形式验证作为其验证流程的一部分。实际上，早期的主流形式采用方式很好地满足了汽车芯片制造商的需求，汽车芯片制造商的需求始于系统控制IC。

Cadence产品管理总监Pete Hardee说：“汽车系统由通过CAN总线连接的联网ECU组成。” “这引入了许多连接系统可以交互的场景。这不仅提供了许多驱动程序可用性方面的优势，同时还为安全性至关重要的系统引入了许多潜在的故障模式和攻击漏洞。

Hardee指出，考虑验证目标功能的验证方法很容易涵盖这些模式。他说：“验证工程师可能会设想出某些失败情况，以及结果测试的某些“受限随机”变体，例如基于UVM的验证中常见的变体。” “但是故障模式和漏洞通常以与这些系统的已知功能完全无关的方式表现出来。”

除了仿真之外，形式验证还可以用于集成电路的功能验证。Tortuga Logic的安全应用工程师Anders Nordstrom说，形式化的详尽性意味着它适合发现可能影响汽车应用安全性的极端错误。形式验证也可以用来证明设计中没有嵌入特洛伊木马。

OneSpin的技术营销经理Sergio Marchese说，形式考虑两个方面：所需的信任度和验证成本。他说：“在验证签字方面，仿真和仿真无法达到形式提供的质量。” “汽车芯片供应商通常会向关键IP和子系统应用形式认证，以证明关键芯片功能中没有错误。随着他们开发许多产品衍生产品，他们还可以自动化流程并达到这一质量水平，同时节省了工作量。”

形式版也适用于模拟量有限或没有价值的任务。Marchese说：“例如，考虑内存中的纠错功能。” “创建测试平台和覆盖范围以测试所有可能的组合是不可能的。即使只是进行一些随机测试，仍然比形式测试需要更多的工作。可以使用类似的参数来验证具有内置冗余的容错配置寄存器。例如，英飞凌（Infineon）在各种论文和演示中已经证明，形式属性检查和基于模型的突变覆盖比仿真要有效得多。”

此外，形式的验证技术还可以通过确保遵守协议和规范来提高对系统功能正确性的信心。

Synopsys的VC Formal产品PMM Guillaume Boillet指出：“它们还有助于实现汽车行业所需的更高级别的可靠性和安全性。”形式验证通常与更传统的验证方法结合使用，以增加覆盖范围并减少周转时间。这样的重要例子之一就是应用形式技术来减少故障空间并进行故障分类，通过在给定的设计中形式检查其可控性和可观察性，从而将安全与危险相区分。

汽车IC是当今开发的最复杂的半导体之一，即使对于资深的设计和验证团队而言，它们也具有挑战性。要使这些芯片在整个预期寿命（可能超过十年）内更加可靠，就需要更加集中精力消除潜在的问题。模拟显示了可预见的错误的存在，但仅限于专家可以设想哪些错误。相反，形式是决定性的，但范围较窄。

西门子业务部门Mentor的功能安全解决方案经理Jacob Wiltgen表示：“形式功能包括时钟/复位验证，覆盖范围分析，逻辑等效性等。“最终，部署形式版可加快汽车生命周期，同时实现任何安全关键产品，零缺陷和零缺陷的主要目标。”

特别是，发现迄今尚未从已知功能中移除的故障模式所需的验证技术通常被统称为否定测试，这从根本上就是为什么形式验证对于安全性至关重要的系统来说是有吸引力的技术的原因。

“形式自然是一种“负面测试”方法。形式而言，您无需以构想测试的方式来构想测试，而是以断言或属性的形式捕获所需的行为。然后，形式工具会像使用硬件黑客一样，使用各种可能的输入组合来破坏所需的行为。”

形式起着越来越重要作用的新领域涉及车辆内部和外部的安全性。这包括车辆到基础设施（V2I）和车辆到车辆通信。形式可用于检测关键IP或整个芯片结构中潜在的违反机密性和完整性属性的行为。

OneSpin的Marchese说：“真正的挑战是将其提升到一个新的水平，并支持有效的事件响应流程以及如何遵守即将到来的ISO / SAE 21434标准。”他指出，这对于发现无法预料的滥用案例场景特别有用。

汽车的安全性至关重要，因为它会影响安全性。根据Tortuga Logic的Nordstrom的说法，如果有人可以禁用发动机或远程踩刹车，则未经授权访问车辆数据和未经授权控制汽车功能可能会导致严重事故。“在这一领域，安全威胁来自直接访问汽车系统的人，或者通过V2I或V2V基础架构远程访问汽车系统的人。验证整个汽车系统的安全性将需要多种验证方法，”他说。

使用信息流跟踪的形式安全性验证可有效验证IC中的数据完整性和数据泄漏问题。不允许将芯片内部的敏感数据泄漏给外部观察者，也不允许外部代理控制芯片的设置和行为。

“形式可以确保与电路的接口是安全的，但是验证多个芯片或大型IP模块可以安全地通信而不会发生数据泄漏或违反数据完整性的行为，可能不在形式范围之内，” Nordstrom说。“这更适合基于仿真的信息流跟踪技术。正规汽车仍然可以通过确保组件没有任何安全性弱点来解决车辆内部，从车辆到基础设施以及其他车辆的安全问题。这是重要的一步，但不足以解决整个汽车系统的安全问题。”

汽车系包含多个运行嵌入式固件的处理器。他说：“这在系统中创建了许多安全漏洞。” “正规的机构可能能够确保未经授权的用户不会覆盖固件。还需要验证硬件/软件交互不会创建任何安全漏洞。该验证需要在仿真模型或仿真中运行固件指令。这也超出了形式的范围，最好在仿真或仿真中使用信息流跟踪技术进行验证。”

同时，车辆通信系统已经处于概念和计划阶段多年，并且最近已成为现实，哈迪说。“具有巨大优势的前景广阔-包括物流效率大大提高，交通管理以及朝着车辆安全和自动驾驶迈出的重要一步。无论是V2I还是V2V，它们也为汽车系统验证带来了更多注意事项。首先，它们会带来更多的计算能力和软件，从而进一步增加系统复杂性。其次，它们为潜在的黑客提供了导致问题的远程通信路径。V2I和V2V之间的差异是双重的-远程程度以及可以直接与哪些系统通信。V2I可能会增加黑客可以访问给定系统并且黑客可能影响更多车辆的机会，而V2V则意味着黑客需要与目标非常接近。但是黑客可以直接访问安全关键的ADAS或控制制动，加速或转向的自动驾驶汽车系统。”

YouTube上有许多关于被盗车辆和远程控制车辆的视频，并且有许多关于各种车辆发生类似事件的报告。V2I和V2V技术的上线无疑将增加这些实例的数量，甚至可能增加严重性。

Hardee说，在一定程度上，黑客可以使攻击看起来像是对某种外部威胁的有效通信，以激发车辆执行不安全的操作，而接收端的系统几乎没有形式的服务。“但是只有一部分攻击看起来像那样。在许多其他攻击方法中，黑客通过软件获得访问权限，但利用硬件平台中的弱点来获得对作为攻击目标的系统的访问权限。”

通过这种方式利用的弱点包括：

操纵访问控制寄存器以访问安全或安全关键系统。

引发重置序列以创建和利用未初始化状态。

通过调试或测试结构获得访问权限。

利用预取和投机/无序执行（如Meltdown和Spectre）。

提升访问安全系统的特权。

事实证明，形式验证可以通过检测此类漏洞来增强SoC的安全性。

Synopsys的Boillet说：“验证是否不可能从内部病毒或外部来源未经身份验证的访问是一个非常复杂的问题，对于形式路径验证而言，这是非常有效的。” “基于设计人员对各个安全区域的声明，可以使用形式技术来识别潜在的数据泄漏和完整性问题，以确保机密数据对非安全区域不可见并且不能被非法修改。”

Wiltgen指出，形式的结构分析功能非常适合分析设计连接以保护芯片的安全部分，从而确保不存在会损害安全性的“隐秘路径”。“这包括往返IP的路径分析，这些IP提供无线V2I和V2V功能。考虑到当今IC的复杂性，过去的方法（例如专家检查或仿真）是不够的。与形式化增强功能验证的方式类似，形式化的详尽性可以识别“空白区域”中的安全违规行为，这是人类编写基于安全性的测试所无法预见的情况和异常情况。”