[發(fā)明專利]旁路攻擊漏洞形式化驗(yàn)證方法及裝置

有效

• 申請?zhí)枺?/td>: 202110481070.3
• 申請日: 2021-04-30
• 公開（公告）號(hào): CN113138721B
• 公開（公告）日: 2022-11-29
• 發(fā)明（設(shè)計(jì)）人: 王海霞;呂勇強(qiáng);忽朝儉;汪東升;徐子涵
• 申請（專利權(quán)）人: 清華大學(xué);華為技術(shù)有限公司
• 主分類號(hào): G06F3/06
• 分類號(hào): G06F3/06;G06F21/57
• 代理公司: 北京路浩知識(shí)產(chǎn)權(quán)代理有限公司 11002
• 代理人: 張雅娜

本發(fā)明提供一種旁路攻擊漏洞形式化驗(yàn)證方法及裝置，方法包括：將緩存旁路攻擊描述為訪存操作的組合，以建立訪存操作模型；將緩存模型建立為緩存狀態(tài)機(jī)；根據(jù)安全規(guī)范、時(shí)間結(jié)果和第一路徑規(guī)范對緩存狀態(tài)機(jī)進(jìn)行形式化驗(yàn)證，以確定緩存狀態(tài)機(jī)是否存在緩存旁路攻擊漏洞。所述裝置用于執(zhí)行上述方法。本發(fā)明提供的旁路攻擊漏洞形式化驗(yàn)證方法及裝置，對處理器訪存操作和緩存設(shè)計(jì)進(jìn)行建模，建模方式具有可擴(kuò)展性，適用于多種硬件或軟件緩存設(shè)計(jì)，只需編寫要測試的緩存設(shè)計(jì)模型，就可以高效自動(dòng)地對緩存設(shè)計(jì)是否存在旁路攻擊漏洞進(jìn)行全面分析以及自動(dòng)化的驗(yàn)證，可以適用于不同的處理器和指令集平臺(tái)。

技術(shù)領(lǐng)域

本發(fā)明涉及計(jì)算機(jī)系統(tǒng)安全技術(shù)領(lǐng)域，尤其涉及一種旁路攻擊漏洞形式化驗(yàn)證方法及裝置。

背景技術(shù)

處理器緩存位于計(jì)算機(jī)處理器和主存之間，用于暫時(shí)存儲(chǔ)主存中的數(shù)據(jù)以加速內(nèi)存訪問的速度，是現(xiàn)代處理器中必不可少的重要組成部分。然而，處理器緩存的存在也會(huì)有潛在的安全隱患。對于帶有緩存的處理器，訪存指令的執(zhí)行時(shí)間會(huì)根據(jù)緩存狀態(tài)存在差異。攻擊者可以利用訪存指令的執(zhí)行時(shí)間差異，發(fā)起緩存旁路攻擊。例如，對于存取類訪存指令，若緩存中存有對應(yīng)的內(nèi)存地址，則不需要訪問主存，指令執(zhí)行速度較快。否則，需要向主存發(fā)起訪存請求，指令執(zhí)行速度則較慢。利用訪存操作的時(shí)間差異，攻擊者可以辨識(shí)緩存的內(nèi)部狀態(tài)，竊取被攻擊進(jìn)程秘密信息。

最近，研究人員發(fā)現(xiàn)的一系列Spectre、Meltdown等利用處理器緩存旁路攻擊的新型漏洞的出現(xiàn)，對處理器安全構(gòu)成了嚴(yán)重威脅。為此，防御緩存旁路攻擊已成為處理器設(shè)計(jì)的重要因素。為了防御緩存旁路攻擊，目前也已有提出了多種緩存防護(hù)設(shè)計(jì)，可以防御特定類型的緩存旁路攻擊漏洞。然而，這些緩存防護(hù)設(shè)計(jì)只能防御特定類型的緩存旁路攻擊，不能證明其是否能防御全部類型的緩存旁路攻擊。

目前，學(xué)術(shù)界和工業(yè)界缺乏一種方法，可以對特定處理器緩存設(shè)計(jì)實(shí)行形式化的驗(yàn)證，確認(rèn)其是否可以防御任何處理器緩存旁路攻擊，并尋找出所有可能的緩存旁路攻擊。因此，設(shè)計(jì)一種可以對處理器緩存旁路攻擊進(jìn)行全面分析的驗(yàn)證方法是很有必要的。

發(fā)明內(nèi)容

本發(fā)明提供的旁路攻擊漏洞形式化驗(yàn)證方法，用于克服現(xiàn)有技術(shù)中存在的上述問題，能夠?qū)μ幚砥骶彺媾月饭暨M(jìn)行全面分析及形式化驗(yàn)證。

本發(fā)明提供的一種旁路攻擊漏洞形式化驗(yàn)證方法，包括：

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

將緩存模型建立為緩存狀態(tài)機(jī)；

根據(jù)安全規(guī)范、時(shí)間結(jié)果和第一路徑規(guī)范對所述緩存狀態(tài)機(jī)進(jìn)行形式化驗(yàn)證，以確定所述緩存狀態(tài)機(jī)是否存在緩存旁路攻擊漏洞；

其中，所述緩存狀態(tài)機(jī)，用于接收緩存行為指令，輸出所述時(shí)間結(jié)果，并將所述緩存旁路攻擊描述為所述第一路徑規(guī)范；

所述緩存行為指令是根據(jù)所述緩存模型面對所述訪存操作所表現(xiàn)出的緩存行為確定的；

所述第一路徑規(guī)范為存在可到達(dá)目標(biāo)狀態(tài)節(jié)點(diǎn)的訪存操作序列，在所述目標(biāo)狀態(tài)節(jié)點(diǎn)下所述訪存操作存在可判斷的時(shí)間差異；

所述安全規(guī)范為不存在可到達(dá)目標(biāo)狀態(tài)節(jié)點(diǎn)的訪存操作序列，在所述目標(biāo)狀態(tài)節(jié)點(diǎn)下，所述訪存操作存在可判斷的時(shí)間差異；

所述可判斷的時(shí)間差異為對于不同的相對關(guān)系，所述時(shí)間結(jié)果確定且所述時(shí)間結(jié)果存在差異。

根據(jù)本發(fā)明提供的一種旁路攻擊漏洞形式化驗(yàn)證方法，

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

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

其中，所述操作者包括攻擊者進(jìn)程和受害者進(jìn)程；