Module 4 slides 14-17

[franzose]

Hello,

I have a question concerning the faithfulness of the primitive requests for creating and destroying subjects and object. For each interpretation of the formalization there is this statement refering to \(\forall s' \in S', o' \in O', a' \in ATTRIBS. (s',o',a') \in A' \Leftrightarrow (s',o',a') \in A\):

The fourth clause ensures that authorizations for subjects and objects remain unchanged by the primitive request.

In my opinion this is true for the "create" requests but not for both "destroy" requests, because the authorization relation should change in a way that all authorizations in A having the destroyed subjects and/or objects are no longer present in the new relation A'.

I must admit that I'm even not quite sure, whether the formula has any constraints on what should happen with the destroyed entities within the authorization relation, because it is only quantifying over the new sets where the destroyed subjects and objects are already removed. So am I right that there is nothing said about the destroyed entities and that they could still remain in the autorizations, but that this is not mandatory?

Thank you in advance for your help

[Sarah Ereth]

Hi,

a protection state in the HRU model is a triple (S,O,A) where
\(S \subseteq SUBJECTS\),
\(O \subseteq OBJECTS\) and \(S \subseteq O\), and
\(A \subseteq S \times O \times ATTRIBS\).

From the last requirement, an answer to your question can be derived. If it is not clear yet, please ask me in the exercise session tomorrow .

Best wishes,
Sarah

[franzose]

\(A' \subseteq S' \times O' \times ATTRIBS\).

That one made it clear, thank you very much! See you tomorrow

[DanielSchoepe]

I realize this is an old thread, but while preparing for the midterm I noticed that I'm a bit skeptical about this explanation:

I don't think we actually require that \(A' \subseteq S' \times O' \times ATTRIBS\) is ensured after updates, since when defining the induced relation \(\Longrightarrow\) it is only required that the constraints of the primitive requests are fulfilled, but I don't see any mention of the property we assume here. In consequence, this definition would allow ill-formed protection states as results (we don't seem to require somewhere that \((S', O', A')\) has to be a protection state, so this argument would rely on highly implicit assumptions).

Also, if the condition would be allowed to be violated for some primitive request and that the resulting protection state is somehow "magically" corrected to satisfy it afterwards, there's
the question of whether such a correction is always possible and unambiguous. This is probably fullfilled here though, since one can take the biggest subset of \(A'\) satisfying it, but it would deserve to be mentioned somewhere.

In any event, I'd find it a lot clearer to just write, e.g. in the "destroy subject" case, \(A' = \{ (s',o,a) | (s',o,a) \in A \land s' \not = s \land o \not = s \}\), because this does not rely on such constraints that may or may not actually be stated somewhere.