[發明專利]旁路攻擊漏洞形式化驗證方法及裝置

有效

• 申請號: 202110481070.3
• 申請日: 2021-04-30
• 公開（公告）號: CN113138721B
• 公開（公告）日: 2022-11-29
• 發明（設計）人: 王海霞;呂勇強;忽朝儉;汪東升;徐子涵
• 申請（專利權）人: 清華大學;華為技術有限公司
• 主分類號: G06F3/06
• 分類號: G06F3/06;G06F21/57
• 代理公司: 北京路浩知識產權代理有限公司 11002
• 代理人: 張雅娜

1.一種旁路攻擊漏洞形式化驗證方法，其特征在于，包括：

將緩存旁路攻擊描述為訪存操作的組合，以建立訪存操作模型；

將緩存模型建立為緩存狀態機；

根據安全規范、時間結果和第一路徑規范對所述緩存狀態機進行形式化驗證，以確定所述緩存狀態機是否存在緩存旁路攻擊漏洞；

其中，所述緩存狀態機，用于接收緩存行為指令，輸出所述時間結果，并將所述緩存旁路攻擊描述為所述第一路徑規范；

所述緩存行為指令是根據所述緩存模型面對所述訪存操作所表現出的緩存行為確定的；

所述第一路徑規范為存在可到達目標狀態節點的訪存操作序列，在所述目標狀態節點下所述訪存操作存在可判斷的時間差異；

所述安全規范為不存在可到達目標狀態節點的訪存操作序列，在所述目標狀態節點下，所述訪存操作存在可判斷的時間差異；

所述可判斷的時間差異為對于不同的相對關系，所述時間結果確定且所述時間結果存在差異；

將緩存模型建模為緩存狀態機，包括：

將所述緩存模型建模為包括緩存行為模型、并行緩存模型和子模型的所述緩存狀態機：

根據所述緩存模型面對訪存操作所表現出的緩存行為建立所述緩存行為模型；

根據緩存行初始狀態下的不同緩存狀態和時間結果建立所述并行緩存模型；

根據不同的所述相對關系及所述相對關系所屬的緩存行建立所述子模型；

其中，所述相對關系為與探測地址的相對位置在體系結構上存在差異，且導致不同的訪存操作耗時的，最小的不可區分分類；

所述根據安全規范、時間結果和第一路徑規范對所述緩存狀態機進行形式化驗證，以確定所述緩存狀態機是否存在緩存旁路攻擊漏洞，包括：

根據所述安全規范、時間結果和第一路徑規范對所述緩存狀態機進行形式化驗證，并在確定存在可到達目標狀態節點的訪存操作序列，在所述目標狀態節點下，所述訪存操作存在可判斷的時間差異，確定所述緩存狀態機存在緩存旁路攻擊漏洞。

2.根據權利要求1所述的旁路攻擊漏洞形式化驗證方法，其特征在于，所述將緩存旁路攻擊描述為訪存操作的組合，以建立訪存操作模型，包括：

將所述緩存旁路攻擊描述為包括操作者、操作類型和操作地址的所述訪存操作的組合，以建立所述訪存操作模型；

其中，所述操作者包括攻擊者進程和受害者進程；

所述操作類型包括處理器進行的各種操作和訪問緩存的指令行為類型；

所述操作地址為所述攻擊者進程和所述受害者進程操作的地址集合。

3.根據權利要求1所述的旁路攻擊漏洞形式化驗證方法，其特征在于，所述相對關系，包括：

與所述探測地址為同一地址的第一相對關系；

與所述探測地址為同一緩存行的不同地址的第二相對關系；

與所述探測地址為不同緩存行的不同地址的第三相對關系。

4.根據權利要求1所述的旁路攻擊漏洞形式化驗證方法，其特征在于，在所述確定所述緩存狀態機存在緩存旁路攻擊漏洞之后，還包括：

獲取在所述緩存狀態機上的路徑的最短路圖，并基于所述最短路圖，確定非冗余反例路徑；

其中，所述非冗余反例路徑為到達新的反例狀態的最短路徑，且所述新的反例狀態不能以更短的緩存狀態變遷次數到達；

所述獲取在所述緩存狀態機上的路徑的最短路圖，并基于所述最短路圖，確定非冗余反例路徑，包括：

從初始狀態集合出發，不斷用下一步可到達的狀態節點擴充當前可到達狀態節點集合，直到沒有新的可到達的狀態節點，以確定從初始狀態集合出發的正向最短路樹；

對于從初始狀態集合經第一預設步可到達第一狀態集合出發，不斷用上一步能到達所述第一狀態集合的狀態節點擴充所述第一狀態集合，直到沒有新的狀態節點可到達所述第一狀態集合，確定可到達所述第一狀態集合的反向最短路樹；

根據所述正向最短路樹的第二預設層和所述反向最短路樹的第三預設層的交集，確定所述最短路圖的第二預設層的節點；

根據寬度優先搜索算法在所述最短路圖上進行路徑搜索，以獲取所述非冗余反例路徑；

其中，所述第一狀態集合為存在所述緩存旁路攻擊漏洞的狀態節點的集合；

所述第三預設層＝第一預設層-所述第二預設層。