@37:00 システムが安全であることを証明する問題が決定不可能であるという証拠があります。議論は、保護システムがTMを正確にシミュレートするため、問題は決定できないということです。「停止権」を定義した場合、TMが「停止権」をリークするかどうかという問題は決定不能です。
「停止権」の具体例は?
@37:00 システムが安全であることを証明する問題が決定不可能であるという証拠があります。議論は、保護システムがTMを正確にシミュレートするため、問題は決定できないということです。「停止権」を定義した場合、TMが「停止権」をリークするかどうかという問題は決定不能です。
「停止権」の具体例は?
HRU
(Harrison-Ruzzo-Ullman) モデルについて説明します。
どこ:
S -被験者のセット
オブジェクトのOセット
およびA - アクセス マトリックス。
主なアクセス モードは次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 を表し、qf 漏えいが決定可能問題の停止を意味するかどうかを判断します (これは NP であることが知られています)。 -難しい問題)。
それが明確になることを願っています、乾杯。