Fun and Progress with Security Analysis Tools

Security, in particular access control, has been a best-effort
endeavor. In the case of Linux, significant advancements have been
made in access control by the addition of a reference monitor
interface, called the Linux Security Modules (LSM) framework, capable
of implementing mandatory access control (MAC) policies and modules
that enforce comprehensive MAC policies, such as SELinux, but neither
the LSM interface nor the SELinux policies were designed against
precise security properties. In this talk, we examine the types of
security properties that can be tested, tools for testing these
properties, and approaches for using these tools. For security
policies, system integrity is of particular interest, so we define our
view of managing integrity, describe our Gokyo tool that identifies
potential integrity problems in our SELinux MAC policy, and show how
Gokyo supports managing system integrity. For interfaces, we describe
two properties, complete mediation and complete authorization, that
define that all security-sensitive operations must be mediated and
mediated by the correct authorizations, respectively. In this case,
we descibe the use of the CQual and JaBA source code analysis tools in
achieving accurate and robust verification of the LSM framework. In
both cases, we have found significant issues that require policy and
interface modifications to achieve our expected goals.

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 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.