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.