1樓：
我完全可以用乙個非易失的儲存器插在記憶體那個地方，等你執行起來，啪一關，把儲存器插到別的機器上dump出來。
防禦？？不可能的，別做夢了。╮（╯＿╰）╭
2樓：
形式化驗證的目的是確保軟體在任何時刻的行為完全符合乙個既定的標準，不會出現意料之外的輸出。當然，前提是硬體的實現（如cpu指令集）不存在bug。
對於作業系統，這個標準可以是某個security police的enforcement，要驗證它不存在bug和漏洞可以利用。
但是具體到特定的惡意行為上，這個標準就很難界定了，說到底是乙個惡意軟體/惡意行為識別的問題。就拿題主的竊聽來說，怎麼形式化地表示一切可能的竊聽行為呢？這種惡習行為與正常軟體的行為界限很模糊，而且需要結合具體的使用情景才能做判斷。
而且竊聽這個行為不一定發生在作業系統中，存在邊通道攻擊，這個時候需要驗證的已經不只是作業系統，而是整個物理環境的綜合安全性。在軟體層面，比較實際一點的方法就是白名單策略，只允許執行符合安全策略的軟體，比如經過乙個證書簽名的軟體。這個白名單機制倒是可以利用形式驗證的方法去驗證。
3樓：
不能。1）seL4只是乙個minimum的microkernel，離真正執行的完整Linux還差很多。類似的還有certikos和deepspec，把軟硬體系統的方方面面都經過形式化證明可以說這是大概二十多年來學術界一直在推進的方向。
2）乙個fully verified kernel只是說這個kernel的實現完全地符合了specification，這些spec確保了安全特性比如integrity和confidentiality。至於specification之外的東西就沒法管了，畢竟specification也是人寫的，如果你的specification沒有正確地model你想要的安全特性，比如timing channel，那驗證了也白搭。
沒有經過形式化驗證的數學是玄學嗎？
子夏233 是當年尤拉通過 錯位相加 減 的方式得到所有自然數之和是負十二分之一，以及所有自然數偶數次冪和為0，夠不夠玄學。這還沒完。後來這個 結果 被黎曼解析延拓zeta函式嚴格 形式上 的得到了。從某種意義上當初尤拉得到了正確結果。而且這個玄學結果還在量子力學上得到了應用。 必然是玄學。比如，P...
目前有哪些較好的電腦作業系統可以替代windows系統？
胤粲 換系統的這個問題這得看一下你自己了，系統最終是乙個平台，有價值的是這個平台上的軟體。windous有很多支援的軟體程式，這些就有可能工作生活生就會需要。如果不需要這些程式的話那倒是無所謂了，最多也就看看電影，聽聽歌之類的，這個基本上在任何乙個作業系統上都會實現，也就沒必要追究很多，多多嘗試找自...
半個月可以寫出乙個電腦作業系統嗎？
牛奶巧克力小逗比 不可能，如何你能寫出來，自研中國產的pc端系統就靠你了。乙個安卓，乙個蘋果，乙個鴻蒙，你說安卓之後多少年才出現中國產手機系統鴻蒙。 可以啊，我覺得可能不都不用半個月。當然也可能一輩子都寫不出。如果你本身就會，可能都不用寫，你是怎麼會寫的？肯定之前寫過一些吧？直接複製過來不就行了？如...