在雅虎破解后,芯片制造商需要增加关注安全验证。
雅虎的消息上周的黑客,影响大约5亿用户发送冲击波的焦虑。现在还不清楚如何通过什么手段大规模数据发生违约或黑客访问网络。它可以驱动网络的芯片,经常容易受到攻击他们的操作的完整性。
毫无疑问,半导体公司正在寻找一个可行的验证策略,可以实现在设计和验证流阻止安全漏洞在芯片供电电网的信息。找到简单的解决方案是一个不小的努力考虑到复杂的黑客已经成为,尤其是那些国家赞助的。
解决方案可以是正式的验证和,事实上,越来越多的验证组转向这个通用的工具。几个例子有助于说明其优势。
首先是一个意想不到的信号路径的使用数据传输或操作控制,创建一个通用的硬件漏洞通过常规操作的渠道设计或次要组件。这些可能包括扫描路径、调试接口或一个未预料到的内存读/写。
另一个例子是操纵装置的电源轨跟踪私人数据访问,所谓的“边信道攻击。当然,常规的渠道也开放可用于目标设备安全的漏洞。
最有效的方法来跟踪一个不存在的路径是检查每个州一块可以进入并确认这些州允许保密违反或一个操作完整性的问题。
形式验证的工具选择安全验证时,由于检查的详尽的性质可能应用。例如,正式擅长确保一个意想不到的路径在一个保密的关键可能读不存在,或任何操作场景不能一起发生,可能导致一个完整性的问题。
特洛伊战争(公元前1260 - 1180)教给我们一种托词策略称为“特洛伊木马。“这是更新一个现代旋转,恶意代码段插入到设计实现之前,后来被激活。这样的FPGA设计容易受到攻击时最后一个比特流是加载到FPGA中。等效性检查(EC),形式验证的一个子集,可以用来确定后期的代码添加了通过比较它与早期设计编码,寻找额外的段或操作。
当然EC只是有效,那里是一个原始设计段比较最终代码,这不是通常情况下在RTL设计。一个有效的选项来阻止木马破坏在RTL级是一个迭代的过程,一组断言,检查设计操作运行代码。覆盖率分析应用于理解剩余部分设计代码的测试和额外的断言被写入。任何部分的代码没有明显关系预期行为将挑出和消除。
雅虎黑客是芯片制造商的另一个警钟。他们需要保持一两步之前,黑客和视图形式验证作为一个优秀的解决方案彻底地测试一个SoC设计,防止可能的灾难。
|
|
|
|
|
|
|
|
|
|
留下一个回复