Axiomise 谈“硅验证通过”为何不足以保障处理器安全

Axiomise 的 Ashish Darbari 撰文指出，Meltdown 与 Spectre 暴露的安全漏洞说明安全不只是软件问题，而是系统问题，需在设计前端就纳入架构考量。他认为动态仿真难以扩展、单纯仿真也不够，应引入形式化验证等手段；文中以他协助验证一款可定制 CPU 的经历为例，形式化测试平台发现了非特权访问特权内存区域等漏洞，部分源于设计疏漏或实现与规格不符。