基于行為時序邏輯的入侵取證研究

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