欢迎光临第五届中国汽车网络信息安全峰会2020!

形式化验证对于汽车网络和功能安全愈发重要

发布日期:2020-09-13

GRCC IoVSecurity 今天 

手机阅读

点击上方蓝色字体,关注我们







障碍仍然存在,但采用率正在增长。




形式化验证 (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的复杂性,过去的方法(例如专家检查或仿真)是不够的。与形式化增强功能验证的方式类似,形式化的详尽性可以识别“空白区域”中的安全违规行为,这是人类编写基于安全性的测试所无法预见的情况和异常情况。”



FuSa和形式验证



随着功能安全性验证(FuSa)与汽车安全性并驾齐驱,式的验证技术在这里也发挥了作用。


Marchese说:“在开发需要符合功能安全标准的芯片的许多公司中,已经在生产中使用式验证。” “例如,让我们考虑针对ISO 26262的定量FMEDA。您需要提供证据证明所报告的安全指标正确并达到ASIL目标。对于航空电子设备,您可能必须使用元素分析来证明所有RTL代码都映射到指定要求,如DO-254中所述。另一个应用是综合工具的独立输出评估,并具有针对FPGA流程的形式等效检查。遗憾的是,在许多项目中仍在使用替代方法,即运行缓慢且难以调试的门级仿真,并避免可能在网表中引入错误的高级综合优化。在所有这些情况下,式的验证,无论是向用户公开还是与其他分析引擎一起在幕后运行,都可以实现非常有效且严格的解决方案。”


此外,ISO 26262标准和汽车安全完整性等级系统可以对故障施加很高的抵抗力。这通常是通过安全机制(例如三重模块冗余(TMR)或双核锁步架构)来实现的,这些安全机制会在存在错误或损坏的行为时触发。通过注入固定故障,桥梁故障,过渡故障甚至瞬态故障,可以肯定地通过结构检查和仿真来验证这些要求,而式方法可以在整个故障过程中极大地加快诊断和覆盖范围。


“实际上,使用求解器在识别故障是否可控制(在这种情况下可能是潜在的危险)或是否不可观察(在这种情况下是安全的)时特别有效。好处是多方面的。式引擎提供了一定的感觉,并且也非常通用,因为它们可以在仿真之前或之后与无缝的同一个故障数据库进行交互时应用。” Synopsys的Boillet说。


Cadence的Hardee补充说,功能安全性验证是指即使发生意外或意外事件(故障),整个系统也将保持预期的可靠性和功能,以避免发生不可接受的人身伤害或损坏风险。


“取决于系统的关键级别(例如,ISO 26262中定义了ASIL A至D级别),可能有多种设计技术可以达到该级别-从没有特殊的故障检测电路,通过故障检测,故障校正或冗余系统。”哈迪说。“通常通过引入故障并测量系统对故障的检测和相应的纠正措施,来验证系统满足所需安全级别的能力。”


他同意形式验证已经在功能安全验证中发挥了重要作用,因为可以通过形式引入故障,但是通常,对于通常需要检查的故障数量,故障模拟会更有效。形式验证通常有助于故障模拟前后的分析。


在故障仿真之前,在故障注入之前对故障列表进行形式化分析,以通过将每个故障标记为不可测试或不可观察到的故障来减少故障集。这可以显着减少故障仿真时间,同时改善覆盖率指标。


故障模拟后,FSV应用程序分析故障传播以改善故障分类,以达到或超过ISO 26262等安全规范。ASIL分类提供了必须满足的概率,具体取决于是否在检查器输出处检测到故障,并且可以传播至功能输出。最严重的故障是那些可以传播到未检测到的功能输出的故障。形式分析提供了更大的确定性,即故障永远不会传播到功能输出或始终由检查程序检测到。故障仿真仅取决于测试台的质量才能得出这些结论。


从安全分析到安全验证,形式技术解决了对安全至关重要的工作流程中的许多挑战,包括结构分析以减少故障活动范围,利用形式上的等效性执行工具链评估以及执行详尽的故障注入和度量计算等。


式技术的穷举性非常适合用于安全性至关重要的应用程序,以确保产品正确运行并安全地进行故障处理。” Mentor的Wiltgen说。


此外,Maxim Integrated汽车安全,微技术,安全和软件业务部门总监Michael Haight断言,要进行形式验证,必须定义规则集。谁定义规则?如果它们是可公开访问的标准,则攻击者似乎可以看到如何测试设备,因此可以通过做未经测试的事情来利用系统中的某些弱点。另一方面,安全性并不容易受到黑客的攻击,其目的是证明其符合标准。因此,式验证也许比安全性更适合安全性。”



形式采用



式解决方案的采用随着易用性的提高以及与更广泛的验证平台的更紧密集成而不断加速,同时还进行了进一步的增强,以提供涵盖RF,模拟,电源管理和端到端的端到端解决方案。Boillet说,MCU / CPU。


为了向设计人员提供**价值,这是通过确保所有组件对安全技术(例如TMR和统一数据库)有共同的了解来实现的。根据故障模式影响分析(FMEA)计划,使用诸如仿真,形式,仿真和模拟混合信号验证等各种技术的统一解决方案可以确认安全机制的质量。


Hardee说,标准当然有助于采用,但是功能安全性和安全性标准存在很大差异。“希望新的ISO / SAE 21434网络安全标准将朝正确的方向迈出一步,但是与安全验证相比,总体上缺少针对安全验证的特定指标。没有度量标准,流行的方法是验证可以合理地做的事情,尤其是检查已知漏洞。目前,**实践是将系统移交给攻击实验室(“红色团队”或“白帽”黑客)以尝试破解它。常见的漏洞数据库有帮助,但仍有许多工作要做。”


归根结底,尽管理想情况下式验证是安全关键型工作流程中的一部分,但由于需要除传统设计和验证之外的新技能,它仍然面临采用方面的挑战。“新的汽车和安全专用自动化式应用的创建将推动更高水平的采用。此外,对在较大的安全工具链中何时何地部署式功能进行更好的教育,将有助于增加采用率。


作者:Ann Steffora Mutschler是“半导体工程” 的执行编辑。

原文链接:https://semiengineering.com/formal-verification-becoming-critical-to-auto-security-safety/



相关文章

『自动驾驶安全第一』白皮书解读:功能安全,信息安全,预期功能安全…
下载 | 《自动驾驶安全第一》白皮书
目前最全的汽车信息安全攻防工具和资料清单






SELECTED EVENTS




 

长按二维码识别关注



我就知道你“在看”


  • 电话咨询
  • 15021948198
  • 021-22306692
None