Research

Linux Security Analysis Tools

IBM T. J. Watson Research Center
19 Skyline Drive
Hawthorne, NY 10532

Trent Jaeger , Xiaolan (Catherine) Zhang , Reiner Sailer

The Linux Security Analysis Tools project team is looking at how to improve Linux security by building analysis tools for verifying Linux kernel source properties and access control policies. Based on our initial findings, we are optimistic that such tools are useful and usable for improving our confidence in Linux security.

The Vali project uses static and runtime analyses to verify the authorization hook placement of the Linux Security Modules (LSM) framework, a kernel patch designed to enable mandatory access control enforcement for Linux.

The Gokyo project uses an extended graphical access control model to examine the role-based or type-based access control models, such as the extended Type Enforcemen access control model of the SELinux LSM module.

Project Members

Trent Jaeger
Xiaolan Zhang
Reiner Sailer
Guillaume Marceau(grad student at Brown University)
Antony Edwards (at Symbian Ltd)
Jon Tidswell (grad student at UNSW, Australia)

Other Projects of Interest:

IBM Java Security includes static analysis tools for Java
UC Berkeley's CQUAL uses C type qualifiers to express and verify program properties
UC Berkeley's MOPS uses modelchecking for C security properties
Stanford Meta-Compilation for finding C program bugs

Vali Papers -- Vali: Norse God of Justice (and Program Verifcation, maybe)

Runtime Verification of Authorization Hook Placement for the Linux Security Modules Framework. Antony Edwards, Trent Jaeger, Xiaolan Zhang. ACM Computer and Communications Security. 11/2002. Recommended for publication to ACM TISSEC.
Using CQUAL for Static Analysis of Authorization Hook Placement. Xiaolan Zhang, Antony Edwards, Trent Jaeger. USENIX Security Symposium. 8/2002.
Maintaining the Correctness of the Linux Security Modules Framework. Trent Jaeger, Xiaolan Zhang, Antony Edwards. Ottawa Linux Symposium. 6/2002.

Gokyo Papers -- Gokyo (Ri): More attainable mountain near Everest

Analyzing Integrity Protection in the SELinux Example Policy. Trent Jaeger, Reiner Sailer, Xiaolan Zhang. USENIX Security Symposium. 8/2003.
Policy Management Using Access Control Spaces. Trent Jaeger, Antony Edwards, Xiaolan Zhang. ACM Transactions on Information Systems Security. 8/2003. Extended version of ACM SACMAT 2002.
Managing Access Control Policies Using Access Control Spaces. Trent Jaeger, Antony Edwards, Xiaolan Zhang. ACM SACMAT. 6/2002.
Practical Safety for Flexible Access Control Models. Trent Jaeger and Jonathon Tidswell. ACM Transactions on Information Systems Security. 02/2001.
An Access Control Model to Simplify Constraint Expression. Jonathon Tidswell and Trent Jaeger. ACM CCS. 11/2000.
Integrating Constraints and Inheritance in DTAC. Jonathon Tidswell and Trent Jaeger. ACM RBAC. 7/2000.

Other Papers

Secure Coprocessor-Based Intrusion Detection. Xiaolan Zhang, Leendert van Doorn, Trent Jaeger, Ron Perez, Reiner Sailer. ACM European SIGOPS. 9/2002.
Gaining and Maintaining Confidence in Operating Systems Security. Trent Jaeger, Antony Edwards, Xiaolan Zhang. ACM European SIGOPS. 9/2002.
Flexible Control of Downloaded Executable Content. Trent Jaeger, Atul Prakash, Jochen Liedtke, Nayeem Islam. ACM Transactions on Information Systems Security. 5/1999.