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

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