攻擊圖的自動生成和可視化及其在計算機和SCADA網(wǎng)絡(luò)中的應(yīng)用

為了確保信息物理系統(tǒng)(CPS)和物聯(lián)網(wǎng)系統(tǒng)的安全，我們需要識別對手如何利用現(xiàn)有原子漏洞之間的相互依賴性來組織可能危及系統(tǒng)的攻擊。因此，在系統(tǒng)安全中，生成準(zhǔn)確的攻擊圖十分重要。

基于手動構(gòu)建攻擊圖繁瑣且容易出錯的原因，Alaa T. Al Ghazo等人2019年5月在《IEEE系統(tǒng)：人和控制論會刊》發(fā)表文章，提出了一種基于模型檢驗的自動攻擊圖生成器和可視化工具(A2G2V)。A2G2V算法使用現(xiàn)有的模型檢驗工具、架構(gòu)描述工具和自編代碼來生成攻擊圖，該攻擊圖列舉了原子級漏洞可能被利用來危及系統(tǒng)安全的所有可能序列集。

架構(gòu)描述工具給出了網(wǎng)絡(luò)系統(tǒng)、其原子漏洞和前后條件以及相關(guān)安全屬性的形式化表達。模型檢測器自動識別表現(xiàn)為反例形式的攻擊序列。自編代碼與模型檢測器集成在一起，解析反例，放寬規(guī)范對反例進行編碼，并迭代直到揭示所有攻擊序列。最后，A2G2V還集成了可視化工具，用圖形展示已生成的攻擊圖。實驗結(jié)果在計算機和控制(SCADA)網(wǎng)絡(luò)中的應(yīng)用得到了驗證。