questions about the undecidability proof of HRU safety

Beiträge: 140
Registriert: 2. Mai 2010 17:55

questions about the undecidability proof of HRU safety

Beitrag von AlexanderF »

I have a few questions and remarks about the undecidability proof of the safety (non leakage) property for the HRU model in the pdf document.

First I observed that the set Sigma in the definition in the turing machine is defined, but used nowhere in the document, is it?

Secondly, I think the conditional requests in the set LABELS in Definition 1.6. should not have parameters but rather should they have indices q, gamma and s to distinguish the different labels. I think otherwise it is not possible to express the constraints on the right of the bars.

Thirdly, in the proof of Lemma 8, the two lines beginning with
“forall s’’, s’’’ …” look a little bit strange, at least from the point of parentheses.


Dennis Albrecht
Beiträge: 222
Registriert: 4. Okt 2010 18:15

Re: questions about the undecidability proof of HRU safety

Beitrag von Dennis Albrecht »


let me try to answer some of your questions (although I'm just a student, too :) )

1.) This is a general problem that I have with Turing machines, or to rephrase this: I have seen some Turing machines in the last years and none of them has used Sigma (or at least used it in a meaningful way). I think Sigma is meant to be the content of the tape in the beginning, in a way that the tape may only contain Sigma (and Blank for every cell left and right of the input) before the first step happens. Afterwards you may write every element from Gamma onto the tape. Don't know, why to distinguish the two phases. But if Gamma is Sigma with {Blank} (and no additional elements), the problem is solved, such that the only (!) element that is in Gamma but not in Sigma is Blank (as required for Turing machines).

2.) Labels are defined in a functional way, so that the system administrator could let the system call those functions if users press some specific button on an UI or so (at least my interpretation of this way of writing labels). Therefore they don't have indices (or if they would have, you would have multiple different labels that are some kind of family, but for the admin and users they would appear as different ones). If we now come back to the proof: As we are simulating a Turing maching with an HRU-model (and not the other way), you can think of a situation like this: Imagine some users. If the Turing machine does some step, imagine some user to have some kind of divine inspiration ("göttliche Eingebung") to trigger some action such that this action fulfills all the constraints on the right. As I said, we are just looking for the right action to simulate the Turing machine's step, so you know what you want to achieve and you do not press arbitrary buttons. But all possible steps of the Turing machine would fulfill the constraints.

Greets Dennis


Zurück zu „Archiv“