For complete mediation, we must verify that each controlled operation
in the Linux kernel is mediated by some LSM authorization hook. A
controlled operation consists of an object to which we want to
control access, the controlled object, and an operation that we
execute upon that object. An LSM authorization hook consists of a
hook function identifier (i.e., the policy-level operation for which
authorization is checked, such as
security_ops->file_ops->permission
) and a set of arguments to the
LSM module's hook function. At least one of these arguments refers to
a controlled object for which access is permitted by successful
authorization (sometimes these objects are referred to indirectly).
The first problem is to find the controlled objects in the Linux kernel. In general, there are a large number of kernel objects to which access must be controlled in order to ensure the system behaves properly. Based on the background work done for the runtime analysis tool [6], we have found that effective mediation of access to kernel objects is provided through user-level abstractions identified by particular controlled data types and global variables. Operations on these objects define a mediation interface to the kernel objects at large. Of course, there may be a bug that enables circumvention of this interface, but this is a separate verification problem beyond the scope of this paper.
We identify the following data types as controlled data types:
files, inodes, superblocks, tasks, modules, network devices, sockets,
skbuffs, IPC messages, IPC message queue, semaphores, and shared
memory. Therefore, operations on objects of these data types and
user-level globals compose our set of controlled operations. In this
paper, we focus on the verification of controlled operations on
controlled data types only. Now we can define our complete mediation
verification problem: verify that an LSM authorization hook is
executed on an object of a controlled data type before it is used in
any controlled operation. For example, because the variable
file
in Figure 1's function sys_lseek
is of a
controlled data type, any operations on this variable must be preceded
by a security check on file
. Figure 2 shows
the problem graphically.
In order to solve the complete mediation verification problem, there are a few important subproblems to solve. First, we must be able to associate the authorized object with those used in controlled operations. In a runtime analysis, this is easily done by using the identifiers of the actual objects used in the security checks and controlled operations. In a static analysis, we only know about the variables and the operations performed upon them. Simply following the variable's paths is insufficient because the variable may be reassigned to a new object after the check.
Next, we need to identify all the possible paths to the controlled operation. While the kernel source can take basically arbitrary paths, in practice typical C function call semantics are used. Thus, we assume that each controlled operation belongs to a function and can only be accessed by executing that function.
Thus, all inter-procedural paths are defined by a call graph, but we must also identify which intra-procedural paths require analysis. Note that the only intra-procedural paths that require analysis are those where authorization is performed or those where the variable is (re-)assigned. These are the only operations that can change the authorization status of a variable. Since variables to controlled objects are typically assigned in the functions where their use is authorized and are rarely re-assigned, this often limits our intra-procedural analysis to the functions containing the security checks. Further, security checks should be unconditional with respect to the scope for which the check applies, so such analyses should be straightforward.
Thus, we envision that the complete mediation problem will be solved by following this sequence of steps for each controlled object variable:
If a re-assignment is found in step #5, then the verification is restarted from the location of the new assignment.