L4虛擬內(nèi)存子系統(tǒng)的形式化驗證

摘要： 第二代微內(nèi)核L4在靈活度和性能方面極大地彌補了第一代微內(nèi)核的不足,這引起學術(shù)界和工業(yè)界的關(guān)注.內(nèi)核是實現(xiàn)操作系統(tǒng)的基礎(chǔ)組件,一旦出現(xiàn)錯誤,可能導致整個系統(tǒng)癱瘓,進一步對用戶造成損失.因此,提高內(nèi)核的正確性和可靠性至關(guān)重要.虛擬內(nèi)存子系統(tǒng)是實現(xiàn)L4內(nèi)核的關(guān)鍵機制,聚焦于對該機制進行形式建模和驗證.構(gòu)建了L4虛擬內(nèi)存子系統(tǒng)的形式模型,該模型涉及映射機制所有操作、地址空間所有管理操作...