Safety_Question - 不可判定的證明系統是安全的

Question

這個問題是關於在 https://itunes.apple.com/us/itunes-u/computer-science-foundations/id389259109

的iTunes U安全課程的講授2的「安全問題」，並@ 37：00有一個證明，證明的問題一個系統是安全的是不可判定的。辯論是這個問題是不可判定的，因爲一個保護系統完全模擬了一個TM，如果我們定義了一個「停止權利」，那麼TM就是否泄漏了「停止權利」這個問題是不可判定的。

什麼是「停權」的具體例子？

Answer 1

它談到了HRU（哈里森 - 魯佐 - 烏爾曼）模型。

• 我們表示的狀態作爲三重Q =（S，O，A）

其中：

小號受試者

的

ö -set -set物體

and A -the訪問矩陣。

主要的訪問模式是：read,write,append,execute and own（意思是主體是對象的所有者 - 這意味着他擁有對象的管理權限）。

在 HRU原始論文

（不含丹寧的擴展）， 通俗地說，一個系統是不安全的，如果一些主題可以得到對象o一些權力R，（這大概我們不希望發生的事情）。這被稱爲leak。 正式定義說：

a command α leaks some generic right r from configuration Q = (S, O, A), if α when run on Q, can execute the primitive operation enter r into A[s,o] which did not previously contain r.

然後是主張保護系統準確模擬TM，如果TM進入狀態QF（有限的），然後權泄露，如果安全問題可判定，然後表示TM並確定是否泄漏意味着停止可確定的問題（這被稱爲NP-Hard問題）。

希望能說清楚， 乾杯。