In my last post I gave a brief description of the two governing principles of Multi-Level security. I then used a short-hand version of a logical framework from Chin and Older to explain how a reference monitor may use such a logic to make access control decisions.

In this post I go one step further to look at the MLS component of SELinux policy. I’ll relate the MLS constraints from SELinux to the logical framework from Chin and Older and show how I’ve used their syntax to help debug SELinux denials (AVC denied) in my own policy writing.

SELinux

The type enforcement (TE) model implemented in SELinux is very different from that of the MLS model. TE is a completely different approach to confining subjects and objects. Interesting enough though, to remain relevant in the government space (i.e. to get Common Critieria certified at the EAL4 level against the LSPP), SELinux was extended with the mechanisms necessary to implement an MLS policy. A significant portion of this work was done by TCS and is documented in a brief white-paper [1].

This paper describes the changes to the SELinux implementation in the kernel that were necessary, but assumes the reader is intimately familiar with government security policy. To fill that gap I’ve taken the logical rules from Chin and Older described previously and used them to explain the constraints that implement the MLS policy in SELinux.

SELinux Constraints

WE’ll start with a brief description of the SELinux constraint syntax. The interested reader I’ll refer the to the base constraint file in the SELinux source tree: $SELINUX_SRC/policy/constraints. In short, constraints allow for the policy author to define additional rules that must be satisfied beyond the SELinux type enforcement policy.

Let’s start with a simple example:

constrain dir_file_class_set { create relabelto relabelfrom } 
(
	u1 == u2
	or t1 == can_change_object_identity
);

The first keyword is constrain which simply identifies the constraint. Next comes a set of object types, followed by a set of permissions. When making an access control decision the security server will look at the requested permission and the object type and if they both are members of these sets the constraint will be evaluated. The constraint itself is a simple set of logical expressions. The parameters available for use in these expressions are the user, role and type component of the labels of both subject and object in the request. Components of the subject label are suffixed with 1, objects with 2.

In the expression above we see that the constraint requires that for a file or directory to be created or relabeled the user component of the subject and object labels cannot change (thus they must be equal or ==).
ASIDE: This constraint may seem like a mundane detail but it’s actually quite significant. Historically UNIX operating systems allowed users with sufficient privileges to change their identity to that of another user to perform administrative tasks. This constraint says that SELinux will never allow the user to change their identity (in the SELinux context) making attribution possible.

Examining the constraint further we see there is a loop hole that allows a subject with a specific type attribute (can_change_object_identity in this case) to change the user identity on a file or directory. Loop holes like this are unfortunate but are required for real systems to function.

MLS Constraints

The rules for MLS Constraints are the same as standard constraints. The only differences are:

• subject and object labels available for use have the additional MLS label components
• new operators which allow for the comparison of sensitivity labels

The MLS components of the SELinux labels come in two parts: the low clearance and the high clearance. These are pretty self explanatory as they represent the lowest possible clearance for a principle and the highest clearance the principle may access.
The new operators are:

1. eq: two MLS label components are equal
2. dom: one MLS label component dominates another
3. domby; same as dom but reversed
4. incomp: two MLS label components are incomparable

I’ll explain the important operators as well as an essential MLS property with an example:

mlsconstrain { dir file lnk_file chr_file blk_file sock_file fifo_file } { read getattr execute }
	(( l1 dom l2 ) or
	 (( t1 == mlsfilereadtoclr ) and ( h1 dom l2 )) or
	 ( t1 == mlsfileread ) or
	 ( t2 == mlstrustedobject ));

This rule constraints read operations on a rather large set of object types. The first line of the statement is the expected simple security property: the low clearance of the subject must dominate the low clearance of the object. Simply put this allows subjects to read at or below their lowest clearance.

The second line allows a subject to read an object if it’s highest clearance dominates that of the object AND it’s type is that of ‘mlsfilereadtoclr’ which is short hand for ‘mls file read to clearance’. This is a special set of subjects that are allowed to read to their highest clearance if they’re operating with a ranged label. Most processes will run with only one MLS label so this constraint will rarely come into play except for processes like init.

The remainig two lines are again, types that allow for loop holes. A process with this type would be considered a “trusted process” in the literature which basically means it’s a process allowed to violate the security model. We’d prefer to have none of these if possible but they exist for a number of reasons. These could be poorly coded software that can’t be fixed by those who care about these things because they’re proprietary or they’re simply processes that must violate MLS to perform their task.

Evaluating MLS Constraints in the logic

Using the logic presented in my previous post to reason through an access control decision based on the above SELinux constraints requires we have a way to evaluate expressions using the operators from the constraint language. I’ll address them in the order they’re presented above:

1. eq: equality

Testing the equality of two sensitivity levels is straightforward. Using the operator we get the sensitivity of a principle and then compare the two using a simple comparison of the strings from our partial ordering. If our reference monitor is optimized it may map the strings to integers (as is the case with SELinux) for a faster comparison but the principle holds.

2. dom: dominance

This operator is well developed by Chin and Older in their operator and was the subject of my previous post.

3. domby: variation on dominance

This is simply the reverse of the dominance rule and I think it’s included as syntactic sugar.

4. incomp: incomparable

This operator is only valid when considering the category component of an MLS label and is deferred for future discussion of the Multi-Category Security (MCS) policy.

Now that the operators are sorted out we can use the constraint in an access control decision. I’m using short hand just to keep this post from turning into a book so the logicians among your may groan a bit …
First we must state the partial ordering for secrecy lables in our system. These should be familiar by now:

Next we define a subject and an object in our system and assign them both secrecy levels:

Now that we’ve defined an Unclassified object and a Secret subject we can revisit the simple security property and the additional rules from the SELinux MLS constraint. I’m going to make up some functions and operators out of thin air so brace yourselves:

First I’ve augmented the function such that it can deal with principles having a high and low sensitivity level. I’ve done so by adding a subscript of ‘l’ for the low sensitivity and an ‘h’ for the high sensitivity.

Second I’ve added another function similar to called . Like it allows us to access a component of the security label for a principle. Instead of the classification however it returns the type component of the SELinux label. For the sake of completeness lets give our subject and object types:

Now to it’s just a matter of putting it all together. First from the type and sensitivity assignments for our subject ‘S’ and object ‘O’ we can replace instances of and . I’ve only defined one sensitivity label for each object so both low and high labels are the same.

Since neither neither subject or object we’re considering have the types listed in this constraint we can quickly mark those comparisons as failing. Further we can simplify terms that have become ‘false’ and we get:

In this simple case we’ve reduced the constraint to the simple security property. Further using the partial ordering we’ve defined we can see that Secret dominates Unclassified and our read request should be allowed by the reference monitor.

Conclusion

This very brief exercise shows the application of a relatively new logical framework to the analysis of a specific SELinux MLS constraint. I’ve found this type of reasoning extremely useful in debugging MLS policy as the available tools (audittoallow) provide no useful information about denials caused by constraints. The exercise performed in this post is equally applicable to any other MLS constraint from the reference policy so if you’re interested give it a try with the constraint for common write operations on files and prove the ★-property.

Up next is the MCS policy …

References

1 Chad Hanson, SELinux and MLS: Putting the Pieces Together, TCS

In my last post I introduced a topic I’ve been working on over the past year. That post provided a description of the problem and it’s importance, but didn’t get into the details behind the technologies used in the solution I’ve worked up. This post is the first of several to come that will fill in these details.

Purpose

I’ve been having a hard time sorting out the best way to present the relatively complex topic of computer security policy and it’s application to my specific project. My first few attempts to write this up resulted in some very convoluted ramblings.

It seemed like I was starting in the middle and missing all the background. Hoping to fix this I’m starting from the beginning with a quick explanation of the security policy that’s at the core of my project: military security policies and their implementation in SELinux.

To explain this I’m using a logical framework put forward by Chin and Older in their recent book [1]. I took a class with Dr. Chin this past fall and was particularly impressed with the contents of the book and the clear, concise syntax they developed.

Classifications

Everyone who’s seen a good spy movie has heard references to military security policy. I think it’s safe to day that every James Bond or Jason Bourne movie made a few references to Unclassified, Secret or Top Secret data. These are typically referred to as classifications or sensitivity levels in the literature. Everyone who’s seen these movies understands what the policy is, but few people have a solid grasp on the mathematical rules that govern access control systems implementing this policy.

It really is as simple as it seams though and easy to explain in the context of subjects (generally people or computer processes acting on their behalf) and objects (either physical or electronic). There are two governing principles [2]:

• the simple security property: a subject operating at a given sensitivity level can read objects at the same level or below
• the ★-property: a subject operating at a given sensitivity level can write to objects at the same level or higher

A computer system that implements these two rules is said to implement a multi-level security (MLS) policy.

Inherent in these two rules is a partial ordering among classification labels. Chin and Older describe this ordering by first defining a function that produces the sensitivity of a principle or object: . For a given object O that is classified Secret we would say:

They also define an operator: that describes the relationship between two sensitivity levels. Going back to the sensitivity levels we’re so familiar with we would say:

Simply put a TopSecret principle is more sensitive than (or dominates) a Secret principle, which dominates an principle. Combining these two operators we can now describe these relationships in an access control scenario.

The Simple Security Property

Getting back to the security properties for military data we can use the above syntax to describe the system. The simple security property requires that a subject operating at a given security level can read objects at the same level or below. We’d such a situation as:

Above we assume the ‘O’ and ‘S’ are an object and a subject in our system respectively. By the definition of we know it returns the sensitivity level of its parameter so let’s say that object O is classified Secret and subject S is classified Top Secret. We could then say:

Knowing that is true by the ordering we’ve defined and our knowledge of logical implication (modus ponens WHAT!) we can deduce from this for future use in our logical framework and we take this to mean a read operation would be granted. Chin and Older provide a more rigorous approach but for our purposes the short hand I’m using is sufficient (because I say so).

The ★-Property

The ★-property requires that the sensitivity level of a subject is lower than or equal to that of the object for a write access to be permitted. We’d represent this as:

If ‘S’ and ‘O’ are the same subject and object as in the previous example the values of and will again be top secret and secret respectively. Thus:

Using the same partial ordering defined previously we can see that the first part of the implication here is false. This time from our knowledge of logical implication we can’t say anything about the term on the right (the statement), so we cannot say a write would be granted. It would then be denied by any sane access control implementation. Again I’m using short hand.

Conclusion

This brief introduction was an attempt to frame basic MLS constructs in a simple logic developed by Chin and Older. Alone this post won’t mean much to most people but it’s intended as a foundation. In my next post I’ll introduce SELinux constraints, MLS constraints and use the logic from this post to illustrate how a reference monitor would evaluate constraints in an access control decision.

References

1 Chin, Shiu-Kai and Older, Susan. Access Control, Security and Trust CRC Press, 2011.
2 Bell, David Elliott and LaPadula, Leonard J. Secure Computer Systems: A Mathematical Model, MITRE Corporation, 1973.
3 Chad Hanson, SELinux and MLS: Putting the Pieces Together, TCS