Check out the new USENIX Web site. next up previous
Next: Acknowledgments Up: Using CQUAL for Static Previous: Related Work


This paper presented a novel approach to the verification of LSM authorization hook placement using CQUAL, a type-based static analysis tool. With a simple CQUAL lattice configuration and some simple GCC analysis, we were able to verify complete mediation of operations on key kernel data structures. Our results revealed some potential security vulnerabilities in the current LSM framework, one of which we demonstrated to be exploitable. We further showed that given authorization requirements, CQUAL could be used to verify complete authorization as well. Our results demonstrate that combinations of conceptually simple tools can be powerful enough to carry out fairly complex analyses.

Our main problem is the elimination of false positives. Static analysis generally errs on the conservative side, so we initially had a large number of type errors. However, we have identified techniques for secondary analyses that can eliminate many of those false positives. Extensions to CQUAL are necessary to eliminate some types of false positives, but this is ongoing work.

Catherine Zhang 2002-05-13