形式验证成为关键汽车安全、安全

正式确认将承担越来越重要的角色在汽车安全,建筑在其已经广泛使用在对安全性要求苛刻的应用程序。

正式一直是汽车的重要组成部分半导体验证一段时间。之前ADAS的出现和半自治车辆-和功能安全规范ISO 26262和网络安全规范ISO / SAE 21434 -数字系统内容在汽车快速增长。领先的汽车等IC供应商博世和英飞凌已经使用形式验证多年来作为验证流的一部分。事实上,早期的主流正式采用网状与汽车芯片制造商的需求,从系统控制电路。

“网络化汽车系统由ecu通过CAN总线连接,”皮特荷迪说,产品管理主管节奏。“这介绍了许多场景连接系统可以交互。提出了许多驱动程序可用性的优点,同时引入许多潜在的失效模式和攻击漏洞,安全至上的系统必须考虑。”

荷迪指出,这些模式很容易被验证方法,考虑应有验证功能。“也许有一些失败场景验证工程师可以怀孕,再加上一些约束随机的变异等合成测试中常见UVM的验证,”他说。“但失效模式和漏洞显现的方式常常与这些系统的已知功能完全无关。”

形式验证可用于集成电路功能验证除了模拟。正式的详尽的性质意味着它适用于发现问题的错误,会影响汽车安全与安全应用,Anders Nordstrom说,安全应用工程师龟岛的逻辑。正式的验证也可以用来证明没有木马嵌入到设计中。

塞吉奥Marchese、技术营销经理OneSpin说,有两个方面需要考虑正式——所需的自信程度和验证的成本。“验证签字时,模拟和仿真不能匹配质量由正式的,”他说。“汽车芯片提供商经常正式应用于关键IPs和子系统来证明没有bug的关键芯片的功能。开发许多产品衍生品,他们也可以自动化流程和实现这一质量水平而储蓄的努力。”

正式的也适用于任务模拟有限或没有价值的地方。“考虑记忆的纠错功能,例如,“Marchese说。“创建一个testbench和报道测试所有可能的组合是不可能的。即使只是做一些随机测试还需要更多的努力,而不是正式的。类似的争论可以验证的配置寄存器内置冗余容错。例如,英飞凌已经证明在各种论文和演讲,正式财产检查和基于模型的突变比模拟覆盖更有效。”

此外,正式的验证技术可以提高系统的信心水平功能通过确保正确性,除此之外,遵守协议和规范。

“他们还可以有助于实现更高水平的可靠性和安全性要求的汽车行业,“Guillaume Boillet指出,PMM VC正式产品Synopsys对此。”形式验证通常与更传统的验证方法来提高覆盖率,减少周转时间。这样一个重要的例子是正式的技术来减少故障空间的应用程序并执行故障分类,区分免受危险的正式检查他们的可控制性和可观测性在一个给定的设计。”

汽车ICs是最复杂的半导体今天正在开发,让他们挑战即使对经验丰富的设计和验证团队。制造这些芯片更可靠的在他们的预期寿命,这可能是十年以上,需要更多关注消除潜在的问题。仿真,显示的存在可预见的错误,是限于缺陷可以由专家构想出来的。相比之下,正式是结论性的,但范围窄一些。

“正式的功能包括时钟/重置验证、覆盖率分析,逻辑等价,”Wiltgen雅各说,功能安全解决方案经理导师,西门子业务。“最终,正式部署加快了汽车生命周期同时关闭任何安全关键产品的主要目标,零缺陷和零缺陷”。

具体地说,发现失效模式所需的验证技术所以远离已知的功能通常被统称为负面测试,这从根本上是为什么形式验证是一个有吸引力的技术安全至上的系统中,荷迪说。

“正式的自然是一个“负面测试的方法。而不是验证工程师不得不怀孕测试,在正式捕获所需的断言的形式或财产的行为。然后正式工具练习的所有可能的组合输入所需的行为,就像一个硬件黑客”。

验证相互作用
正式的新领域发挥着越来越大的作用涉及到安全、内外。这包括vehicle-to-infrastructure (V2I)和vehicle-to-vehicle沟通。正式的可以用来检测潜在违反机密性和完整性属性在芯片关键IPs或织物。

“真正的挑战是将更上一层楼,支持高效的事件响应流程和合规与即将到来的ISO / SAE 21434标准,“OneSpin的Marchese说。他指出,这是对不可预测发现滥用情况下特别有用。

汽车的安全是至关重要的,因为它会影响安全。未经授权的访问汽车功能的车辆数据和未经授权的控制可能导致严重事故如果有人可以禁用远程引擎或踩下刹车,根据龟岛逻辑的诺。“在这个领域,安全威胁来自某人有直接访问汽车系统,或有人访问汽车系统远程通过V2I或V2V基础设施。验证整个汽车系统是安全的,需要多个验证方法,”他说。

正式使用信息流跟踪安全验证是有效的在ICs验证数据完整性和数据泄漏问题。敏感数据在一个芯片不能泄露给外部观察者,和外部代理不能控制芯片的设置和行为。

“正式可以确保接口电路是安全的,但验证几个芯片或大型IP模块可以安全地交流没有数据泄漏或违反数据完整性可能超出了正式的范围,”诺德斯特姆说。“这是更适合基于仿真的信息流跟踪技术。不过,正式在车辆可以解决安全问题,从汽车到基础设施和与其他车辆,确保没有任何安全漏洞的组件。这是一个重要的步骤,但不足以解决整个汽车系统安全问题。”

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

同时,车载通信系统多年来一直在概念和计划阶段,最近成为现实,荷迪说。“有巨大的优势——包括巨大的承诺更高效的物流、交通管理、以及重大走向安全和自主驾驶车辆。是否他们V2I V2V,他们也带来更多考虑汽车系统验证。首先,他们进一步增加系统的复杂性和更多的计算能力和软件。其次,他们提供一个潜在的黑客远程通信路径导致的问题。V2I之间的差异和V2V是双重的,多么遥远,系统可以直接沟通。V2I可能增加的可能性黑客可以访问给定系统和黑客可能影响更多的车辆,虽然V2V意味着黑客需要接近目标。但一个黑客可以直接访问安全性至关重要的ADAS或自主车辆系统控制制动,加速度或转向”。

有很多视频在YouTube上的车辆被攻击和远程控制,以及众多报道出现在一系列类似的车辆。V2I和V2V技术生活无疑会增加这些实例,也许在数量和严重程度。

形式验证如何帮助?
在某种程度上,黑客可以让攻击看起来像一个有效沟通的一些外部威胁引发车辆做一些不安全的,几乎是没有正式的能做的系统在接收端,荷迪说。“但是看起来只有一个子集的攻击。在许多其他的攻击方法,通过软件的黑客获得访问权,但利用一个弱点在硬件平台进入系统攻击的目标。”

的各种弱点利用这种方式包括:

• 操作访问控制寄存器访问安全或关键安全系统。
• 引起复位序列创建和利用未初始化的状态。
• 获得通过调试或测试结构。
• 利用预取和投机/无序执行(如危机和幽灵)。
• 获得晋升的特权访问安全的系统。

正式的验证证明能够强化soc等这些类型的攻击检测漏洞。

“验证任何未经身份验证的访问病毒从内部或外部源可能是一个非常复杂的问题,正式的路径验证证明是非常有效的,“说Synopsys对此Boillet。“基于设计师的宣言的各种安全领域,正式的技术可以应用于识别潜在的数据泄漏和完整性问题,确保机密数据不可见到不安全的地区,不能非法修改。”

Wiltgen指出,正式的理想结构分析功能分析设计芯片的连接到安全的地方,确保不存在任何“通路”,危及安全。“这包括路径分析与IPs提供无线V2I和V2V功能。鉴于当今集成电路的复杂性,以往的方法如专家检查或模拟是不够的。类似于正式的增强功能验证,正式的详尽的性质确定安全违规的黑色空间,场景和异常条件没有预见到人类编写基于安全性的测试。”

FuSa和正式的验证
功能安全验证(FuSa)汽车与安全相辅相成,形式验证技术发挥作用。

“正式确认已经在生产使用在许多公司发展中芯片需要符合功能安全标准,“Marchese说。“让我们考虑定量FMEDA ISO 26262,例如。你需要把证据表明报道安全指标是正确的和实现ASIL目标。在航空电子设备的情况下,您可能必须证明所有的RTL代码映射到指定要求用元素分析,所做的- 254。另一个应用程序是独立输出评估合成工具形式对等检查FPGA流。另一种选择——遗憾的是仍在使用在许多项目是运行缓慢、难以调试的门电路级模拟和避免先进的合成优化,可以在网表引入bug。在所有这些情况下,形式验证,是否暴露于用户或与其他分析引擎罩下运行,使非常有效和严格的解决方案”。

此外,ISO 26262标准和汽车安全完整性水平系统可以征收非常高的电阻的缺点。这通常是通过安全机制来实现,如三模冗余(咯)或双核架构,同步触发的故障或损坏的行为。当然这些需求可以与结构检查和验证仿真通过注入停留在,桥,过渡,甚至瞬态故障,正式的方法可以大大加快诊断和覆盖关闭整个断层运动。

”的确,连接器的使用是特别有效地识别故障如果是可控的,在这种情况下,它可能是危险的,或者如果它是不易观察,在这种情况下,它是安全的。的好处是多种多样的。正式的引擎提供了明确的和也很多才多艺,他们可以应用仿真之前,之后,无缝地与相同的故障数据库交互时,“Synopsys对此Boillet说。

节奏的荷迪补充道,功能性安全验证是指整个系统仍将按计划可靠和功能,即使在计划外的事件或意想不到的事件(故障),以避免人身伤害或损坏的不可接受的风险。

”根据系统的临界水平(如水平ASIL通过D在ISO 26262中定义)可能有各种设计技术来实现水平——从没有特殊故障检测电路,通过故障检测,故障修正,或冗余系统,”荷迪说。”系统的能力来满足所需的安全级别通常通过引入故障验证和测量系统检测和纠正措施结果的。”

他同意形式验证已经起着很大的作用在功能安全验证的缺点可以通过正式的,但通常,介绍了故障模拟更有效的故障,通常需要检查。正式的验证通常有助于分析之前和之后故障模拟。

故障仿真之前,正式执行分析故障列表之前设定的注射为了减少出错将错误标记为不可测试或不可见的仿真测试。这可以大大减少故障仿真的时间同时提高覆盖率。

故障仿真后,一个FSV应用分析故障传播,提高故障分类,以满足或超过安全规范ISO 26262。ASIL分类提供必须满足的概率取决于检测到故障检查器输出和传播功能输出。最严重的错误是那些可以传播功能输出未被发现。正式的分析提供了更大的确定性,缺点从来没有传播功能输出或总是被检查。故障模拟仅取决于testbench的质量达到这些结论。

安全分析和安全验证,正式的技术应对很多挑战在安全至上的工作流中,包括结构分析减少断层活动范围,利用正式执行工具链评估相等,和执行详尽的故障注入和指标计算,等等。

正式的详尽的性质技术非常适用于安全关键应用,确保产品正确操作和安全失败,“导师Wiltgen说道。

此外,迈克尔·海特导演,汽车安全、微指令,安全&软件业务单元马克西姆集成形式验证断言,一个规则集定义。“谁定义的规则?如果他们公开标准,似乎攻击者可以看到设备测试,因此可能会利用一些弱点系统中通过做一些测试。安全,另一方面,不容易受到黑客和目的是证明标准是满足。因此也许形式验证是比安全更适合安全。”

正式采用
而采用正式的解决方案正在加速提高易用性和与更广泛的紧密集成验证平台,进一步增强也正在提供一个端到端解决方案,跨越射频、模拟、电源管理,和单片机/ cpu, Boillet说。

为了向设计师提供最高的价值,这是通过确保所有组件有一个共同的理解的安全技术,如咯和统一的数据库。统一的解决方案,使用各种技术,如模拟、正式、仿真和模拟混合信号验证确认的质量安全机制的失效模式影响分析(FMEA)计划。

标准肯定帮助收养,荷迪说,但是有很大的差异在功能安全标准和安全。“希望新的ISO / SAE 21434网络安全标准将在正确的方向迈出的一步,但总的来说缺乏安全验证的具体指标与安全验证。没有度量,普遍的方法是验证合理可以做什么,特别是检查已知的漏洞。最佳实践是当前系统交给实验室的攻击(“红色团队”或“白帽子”黑客)试图打破它。常见的漏洞数据库的帮助,但仍有很多工作要做。”

在一天结束的时候,虽然形式验证是理想的放置在安全关键工作流,它继续经验采用挑战由于需要新技能超出了传统设计和验证。“创建新的汽车和安全特定的自动化正式应用将推动更高水平的应用。此外,更好的教育在何时何地部署正式能力更大的安全工具链将有助于增加收养,导师的Wiltgen说道。