Introduction

Linux Security Modules (LSM) is a framework for implementing flexible access control in the Linux kernel [3]. LSM consists of a set of generic authorization hooks that are inserted into the kernel source that enable kernel modules to enforce system access control policy for the kernel. Thus, the Linux kernel is not hard-coded with a single access control policy. Module writers can define different access control policies, and the community can choose the policies that are most effective for their goals.

The code segment in Figure 1 shows an example of how LSM hooks are inserted in the kernel. The function sys_lseek() implements the system call lseek. The security hook, security_ops->file_ops->llseek(file), is inserted before the actual work (call to function llseek()) takes place.

/* Code from fs/read_write.c */
sys_lseek(unsigned int fd, ...)
{
  struct file * file;
  ...
  file = fget(fd);
  retval = security_ops->file_ops
           ->llseek(file);
  if (retval) {
    /* failed check, exit */
    goto bad;
  }
  /* passed check, perform operation */
  retval = llseek(file, ...);
  ...
}

Figure 1: An example of LSM hook.

System administrators can provide an implementation of the corresponding hook functions (e.g. security_ops->file_ops->llseek()) by selecting a kernel module that implements their desired policy. Examples of LSM modules under development include SubDomain [4], Security-enhanced Linux [13], and OpenWALL.

While much effort has been devoted to placing hooks in the kernel, this has been a manual process, so it is subject to errors. Even though the LSM developers are highly-skilled kernel programmers, errors are unavoidable when dealing with complicated software. Thus far, little work has been done to verify that the hooks indeed provide complete mediation over access to security-sensitive kernel objects and enforce the desired authorization requirements. Such verification would help gain acceptance for the LSM approach and enable maintenance of the authorization hooks as the kernel evolves. The verification task for LSM is not a simple one because LSM authorization hooks are embedded within the kernel source, rather than at a well-defined interface like the system call boundary. While this improves both performance and security, it makes it impractical to verify the hook placements manually [6].

As a first step, we began the development of runtime analysis tools for verifying LSM authorization hook placement [6]. These tools are easy to run, have helped us identify the requirements of a verification system, and have enabled us to find some hook placement errors. However, runtime analysis is limited by the coverage of its benchmarks and requires some manual investigation of results to verify errors. Given the recent spate of efforts in static analysis tools [7,11,14], we were curious whether any of these tools could be applied effectively to authorization hook verification. Given a brief evaluation of tools, we chose to use CQUAL [9], a type-based static analysis tool. It was chosen mainly because it was conceptually simple (type-based and flow-insensitive), available to use without significant modification, and was supported by formal foundations.

This paper presents a novel approach to the verification of LSM authorization hook placement using CQUAL. We have found that with a simple CQUAL lattice and some additional analyses using GCC we can verify complete mediation of operations on key kernel data structures. Complete mediation means that an LSM authorization occurs before any controlled operation is executed. Further, we have found that using the authorization requirements found by our runtime analysis tools, we can build a manageable lattice that enables verification of complete authorization. Complete authorization means that each controlled operation is completely mediated by hooks that enforce its required authorizations. Our results reveal some potential security vulnerabilities of the current LSM framework, one of which we demonstrate to be exploitable. The findings and a code patch were posted to the LSM mailing list [5], and the fix was incorporated in later kernel releases. The resultant contribution is that through the use of a small number of conceptually simple tools, we can perform a fairly complex analysis.

The rest of the paper is organized as follows. Section 2 defines the verification problem. Section 3 describes our approach in detail. Section 4 presents the potential vulnerabilities discovered through our static analysis. Section 5 discusses effectiveness of our approach and possible extensions to CQUAL. Section 6 describes related work, and Section 7 concludes the paper.