公开(公告)号：CN116415256A

公开(公告)日：2023-07-11

申请号：CN202310396695.9

申请日：2023-04-14

Applicant: 北京邮电大学

Inventor： 王春露 ,  叶青瑜 ,  柯谦 ,  王海霞 ,  吕勇强 ,  汪东升 ,  邱朋飞

IPC: G06F21/57 ,  G06F9/38

Abstract: 本发明公开了一种处理器分支预测攻击漏洞形式化验证方法，包括以下步骤：S1、建立分支预测攻击所违反的安全属性，所述安全属性描了述安全的分支预测器设计应当遵守的安全规范；S2、建立分支预测行为模型，将分支预测攻击描述为一系列抽象分支操作的组合；所述分支操作为操作者、操作类型、操作地址、跳转方向和跳转地址组成的五元组，是某条分支指令的抽象表示；S3、将分支预测器设计建模为接受分支预测行为指令，并根据输入的不同指令设计出不同变化的分支预测模型状态机，输出预测结果，检查安全规范，并将分支预测攻击转换为在状态机上的路径规范；S4、对分支预测器设计的状态机进行模型检验，判断其是否存在分支预测攻击漏洞。