摘要:提出一種基于行為時(shí)序邏輯的入侵取證的形式化方法,其描述語言能夠準(zhǔn)確描述入侵證據(jù)、系統(tǒng)知識(shí)以及攻擊行為,并具有在部分?jǐn)?shù)據(jù)缺失的情況下進(jìn)行非確定性推理的能力;其自動(dòng)驗(yàn)證工具能夠?qū)で箢~外的證據(jù)并可檢查是否有可能的攻擊與這些證據(jù)相符。實(shí)例研究表明,這種方法不依賴于具體的攻擊技術(shù)和操作系統(tǒng),不懼證據(jù)的缺失,能夠有效搜尋更多的證據(jù)并重建可能的攻擊場(chǎng)景。