Part of the project I'm working on is an MCS policy that I want to describe and (hopefully) proof correct in this posting. I do not expect anyone to read this through, but if maybe someone is interested in stuff like this, I'd really appreciate any quick look over it. These are the specifications I want my policy to meet: I want a user to have 100 compartments, each one totally separated from every other. The user (called main user) has full access over every compartment. For each compartment C there shall be 9 subcompartments of C each one totally separated from every other subcompartment or compartment, but accessible from C. No compartment or subcompartment shall have the possibility to access or leak data "horizontally", i.e. to any other compartment or subcompartment that is not of his own. Neither shall any compartment or subcompartment be able to access "upwards", i.e. from a subcompartment to its compartment or from a compartment to the main user. The only allowed data flow is reading, writing and transitioning from the main user to the compartments and from every compartment to its subcompartments. (Set aside practical exceptions like sigchild, fd use, some X11 stuff that needs to be shared among all compartments etc.) My Implementation: I have a user user_u with range s0 - s0:c0.c999 starting off as main_t:s0. main_t is not mcs constrained. main_t can transition to sub_t which is mcs constrained and has no access to main_t. I call a range of s0:c(N*10).c((N*10)+9), 0<=N<=99, a compartment with id N. E.g. compartment 01 with range s0:c10.c19. I call s0:cI, (N*10) < I <= ((N*10)+9), a subcompartment of N with id I. E.g. subcompartment 5 of compartment 01 with range s0:c15. A process of compartment N is run as: sub_t:s0:c(N*10) - s0:c(N*10).c((N*10)+9) A process of subcompartment I of N as: sub_t:s0:c((N*10)+I) The mlsconstrain (in princip, set aside practical exceptions) is: 01: ( t1 != is_mcsconstrained ) 02: or ( t2 != is_mcsconstrained ) 03: or ( 04: ( l1 domby h1 ) 05: and ( l2 domby h2 ) 06: and ( h1 dom h2 ) 07: and ( h1 dom l2 ) 08: and ( l1 domby l2 ) 09: ) Proof: It is sufficient to proof this for any compartment, say s0:c10.c19. As there is only one sensitivity, the relation of dominance is that of inclusion of category sets. Set inclusion shall be denoted by < > = <= >=. 04 and 05 are just to prevent any "weird" contexts. (I'm pretty sure the kernel already enforces those and gives 'invalid context' if low range > high range. But definite specifications are hard to find, so I put them in to be sure.) It needs to be shown that a process running as s0:c10 - s0:c10.c19 can not access any categories -- directly or through transition -- other than c10.c19. For files created or processes transitioned to it holds true that low range as well as high range can only be a subset of c10.c19. This is ensured by 06 and 07. So the process can neither access nor leak data to either the compartments numerically below hin (s0:c0.c9) or above him (s0:c20.c29, ...). But note that the empty set is also subset of c10.c19. So the process would be able to jeopardise his own integrity by transitioning to or leaking data to s0 -- which in turn would then be accessible form any other compartment. So the source low range must always be a subset of the target low range. This is ensured by 08. For a subcompartment, say s0:c15, it holds true that the process s0:c10 - s0:c10.c19 can transition to, give and write files to etc. as c15 > c10 and c15 < c10.c19. For any subcompartment it is obvious from the above that it cannot access or transition to anything else than itself.
Attachment:
signature.asc
Description: Digital signature
