[redhat-lspp] MLS security context invariants

[Frank Mayer]

I'm trying to get my head wrapped around the "invariants" for security
contexts in the MLS policy. Given that we are implementing these invariants
via state transition constraints makes it all the more challenging.

What I'm trying to convince myself is that we have the simple invariant in
place that says "For all security contexts C, hi(C) dom low(C)." Seems like
an straightforward necessity to me. 

Looking at "file" objects, we indirectly get this invariant via:

mlsconstrain { file lnk_file fifo_file } { create relabelto }
	( l2 eq h2 );

for "ordinary" files assuming that create and relabelto are the only ways to
set a file context (correct?). For the "unordinary" files we have:

mlsconstrain { dir file lnk_file chr_file blk_file sock_file fifo_file }
relabelto
	( h1 dom h2 );

which doesn't give us this invariant nor does the create constraint later
(at least not directly). So I looked at the mlsvalidatetrans constraints and
didn't see it either. 

On quick look I didn't see anything for processes either. I guess I was
looking for (l2 domby h2) as a constraint on any possible label transition.

Am I missing something? Frank