Complete Mediation

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.

Figure 2: The complete mediation problem.

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:

1. Determine the function in which this variable is initialized (initializing function).
2. Identify its controlled operations and their functions (controlling functions).
3. Determine the function in which this variable is authorized (authorizing function).
4. Verify that all controlled operations in an authorizing function are performed after the security check.
5. Verify that there is no re-assignment of the variable after the security check.
6. Determine the inter-procedural paths between the initializing function and the controlling functions.
7. Verify that all inter-procedural paths from an initializing function to a controlling function contain a security check.

If a re-assignment is found in step #5, then the verification is restarted from the location of the new assignment.