Verifying the Correctness of the Linux Security Modules Framework

			     Trent Jaeger
		   IBM T.J. Watson Research Center.

We present an evolution of techniques to verify that the Linux Security 
Modules (LSM) framework correctly implements a reference monitor 
interface.  The LSM framework defines an interface of function pointer 
hooks that enable a loadable module to authorize user process operations. 
In general, such an interface must ensure that all security-sensitive 
operations are authorized.  Further, the hooks must authorize the 
appropriate operations.  We have examined both static and runtime analysis 
techniques for verifying these properties.  We used the CQUAL static 
analysis tool to verify that all security-sensitive operations were 
mediated by an LSM hook.  We also built a runtime analysis framework 
called Vali that enables us to find cases where the operations authorized 
are inconsistent.  We found that static analysis has benefits in complete 
code coverage, but the model was a bit conservative which led to too many 
false positives or cases outside our scope.  With runtime analysis, we had 
only partial coverage and some flaws would go unnoticed (e.g., TOCTTOU 
attacks), but we could find inconsistencies and largely eliminate false 
positives.  The question is whether we can remove the conservative limits 
of static analysis sufficiently to gather the necessary information to do 
the analyses in the manner of the runtime tool.  If so, we would obtain 
complete coverage for analysis that consistent authorizations are made 
with low false positives.  We discuss application of the JaBA static 
analysis tool to overcoming the limitations of our previous static 
analysis.  We also examine what it might take to fully verify a reference 
monitor.

Bio:

Trent Jaeger is a Research Staff Member at the IBM T. J. Watson Research 
Center.  He works in the Network Security Department where he is the 
project lead of Linux Security Analysis project which investigates the 
development of use of tools to improve the security of Linux.  Trent's 
research interests include systems security, access control, security 
analysis tools, and operating systems.  He has published over 40 refereed 
research papers on these subjects.  Also, he has been a member of the 
program committee for several major security conferences, and is the 
inaugural Program Chair for the Industrial Experience track for ACM 
Conference on Computer and Communications Security in 2003.  Trent has an 
M.S. and a Ph.D. from the University of Michigan, Ann Arbor in Computer 
Science and Engineering in 1993 and 1997, respectively.