在汽车工业中排名首位的毫无疑问是安全性，是从根源上加强安全性能。伴随着现代汽车电子器件在汽车部件比重的逐步增加，如何确保硬件、固件、操作系统和应用层的使用安全是一个重要课题。从硬件的观点来看，如果从根源上可以保证硬件系统安全得到保障没有漏洞，那么在此之上建立的固件、操作系统和应用层也会得到根本性保障。在最近汽车电子的安全设计当中，数字签名作为加密钥匙被保存在每一辆车当中。我们为您选中的这篇文章《How Formal Techniques Can Keep Hackers from Driving You into a Ditch》就在介绍如何使用形式验证技术来确保存储在车辆A当中的数字秘钥在根源上无法被被非授权方B盗取或者意外泄露出去。
Andy Greenberg / Wired magazine
在实际的工业案例当中，2015年7月黑客就曾经远程攻破一辆切诺基吉普车的安全系统并使得刹车系统失灵，最终该车驶进了壕沟。另外一组研究者竟然可以通过汽车数字广播系统来侵入汽车的刹车和其它关键系统，通过这种攻击，可以同时对多辆车造成潜在的安全威胁。幸好的是没有人在上述实验中受伤，而汽车的制造商们也针对性地做出了系统修复。但是，这两则故事显然证明了一点，现今的汽车数字电子系统的安全性是多么的重要！
我们可以预见到今后汽车电子供应商会加强他们在数字电路上的安全性能，这其中使用数字秘钥——针对每一个数字系统个体（不同系统和不同车辆均需要有不同的数字秘钥），并且将它们存储在车辆当中。有了这个数字签名，在汽车电子系统内部网络当中传输的数据包就会被加密，同时接收到数据的一方也会利用数据发起方的秘钥来解密，或者接收从生产商授权的系统更新加密数据。
然而，目前主流的总线协议在定义的过程中没有将安全保护考虑进来，这使得CAN（Controller Area Network）总线和LIN（Local Interconnect Network）总线由于带宽或者总线结构的限制，无法来支持安全性能。同时，汽车以太网（Automotive Ethernet）的兴起使得数据包的实时加密解密变成了可能。秘钥会被保存在一块安全存储单元上或者一个独立的寄存器区域上面，为此，RTL设计师和验证师要做的就是确保这块被保护的安全区域不能被非法侵入。
在这一过程中，验证师需要考虑的主要有两点：
- 机密性：秘钥是否会被未授权一方读取或者发生偶然泄露？
- 健全性：秘钥是否会被黑客修改、覆盖、擦除或者由于硬件和固件的缺陷发生更改？
尽管有多种合法的可能路径来访问秘钥，但是在这些合法路径背后的电路组合当中，会有更多数量的禁止情况。从经验来看，即便是一个颗粒度相对小型的设计，设计师也会百密一疏，无法缜密考虑所有可能的情形，进而留下一些漏洞来为以后的不速之客开启窃取之门。那么，我们首先来看一看当前流行的验证形式：
- 安全模糊处理：这是从设计方开始，未在用户文档当中留下跟安全有关的只言片语，当然这本身也假设那些黑客们不会通过不断地实验来发现设计中的缺陷。也许这种方法会阻碍一阵儿黑客的进程，但我们没有充足的信心确保他们没有攻入城堡的那一天。
- 白帽侵入：这一手段是雇佣一些工程师们专门去攻击我们设计的产品，来发现一些潜在的缺陷。但伴随着电路的复杂性日益提高，这种方法的效率也随着不断降低。
- 专家检视：邀请系统设计师有有经验的设计专家进行代码回顾检查，是一个不错的办法，可是就连这些专家自己们都清楚他们无法穷尽思考完所有可能的情形。
- 直接测试：这种常用的验证方法主要针对着既定划分的验证计划和应用场景来编写测试用例，但是这种方法也无法考虑到所有的极端情况。
- 约束随机验证：所有基于仿真的验证最大的限制条件就在于无法产生足够多的测试向量来遍历整个设计，而约束随机验证就是主要来解决这个问题的。它自身有两个好处，第一个是它非常有助于发现一些没有关注到的设计缺陷，第二个是它的随机向量生成种子（random seed）可以使得通过用运算量换取时间的方法在同一时间运行多个仿真来更快验证设计。当然，完全的随机验证（不添加任何约束）是没有意义和低效率的，所以添加有约束的、用户自定义的约束随机测试向量就是这一过程的重要部分。但是同时，由于我们采用了约束随机方法，我们也主动放弃了一些认为不重要的测试情景，这样的情况下，我们就仍然无法遍历整个设计。退一步来讲，即使是约束本身的随机范围，我们也会在功能覆盖率完成部分遇到覆盖率曲线增长瓶颈，尤其当覆盖率超过80%以后的增长率更是缓慢。
所以从上面列举的方法无法穷举测试目标设计，即便是相对小的设计模块，我们也无法在设计的状态组合空间内完全测试。
而能够在数学意义上用来证明或者反证一个系统设计完整性的方法就是形式验证。形式验证依赖于将设计的功能描述转化为形式（property）语言描述。目前主要的两种形式验证语言有IEEE SystemVerilog Assertion（SVA），和Property Specification Language（PSL）。对于形式验证而言，设计师和验证师都可以将两种甚至更多信号之间的功能描述和时序信息通过形式语言明确规定出来，而形式验证工具会将设计和这些形式验证语言组合在一起，通过数学方法来比较设计中的信号所有可能的组合情形是否均符合形式语言编写的规则。由于形式验证工具的分析是建立在所有可能信号输入的布尔等式上的，因此形式验证工具最终给出的结果是一种数学意义上的穷尽结果。
也因此，通过形式语言的规则编写和形式验证工具的协助，我们可以确信在汽车上存储的秘钥A只会被授权方读取或者修改，而不可能被非法的一方B进行数据窃取和篡改。通过这种方式，我们会将任何有违反这一安全规则的设计缺陷在产品被交付到客户之前被发现并且修复。
Rocker
形式验证这一技术本身不算新鲜，毕竟它已经被提出来超过20年了。但是由于形式语言本身编写的颗粒度难于掌握，验证师无法将功能和时序划分为可有效被形式验证工具采纳的规则，同时也由于验证师很难做到全貌编写出与设计描述保持一致的形式规则，这使得形式验证无法像仿真验证一样广泛推广或者只能运用在有限的可以掌控的验证情景当中。只是近5年以来，EDA厂商才考虑生成自动化的形式规则来将验证师从这一泥潭中拯救出来。同样可以考虑引用的方法也包括采用公共的SVA/PSL断言库，以及积极促进设计师也将一些重要的功能和时序通过形式语言预置到设计中去，与验证师一同完成可验性设计的理念（Design for Verification）。
