We are unaware of any other research work on static verification of LSM. However, a number of static analysis tools that were successfully applied to the security domain. Here, we compare their work to ours.
Wagner et. al. [14] used CQUAL to identify format string vulnerabilities. Their work motivated us to apply CQUAL to the more complicated problem of LSM verification. The main difference between our usage of CQUAL and theirs lies in the annotation process. In their work, the target code for annotations is well-defined and has a limited number of occurrences. Therefore, the annotations are done by hand. In our case, the scope of annotated code is much larger, and thus we employ GCC to automatically detect the code to be annotated. We automate the process of marking as well.
Engler et al enables extension of GCC, called xgcc, to do source analyses, which they refer to as meta-compilation [7,1]. A rule language, called metal, is used to express the necessary analysis annotations in a higher-level language. Since the rules match multiple statements, the amount of annotation effort is reduced. A variety of software bugs, including security vulnerabilities, have been found by this tool. While it appears that xgcc could be used for the static analysis we perform, xgcc is not available at this time, so we are unable to evaluate it. A key difference may be that metal rule expressions will have to be extended to reference GCC AST structures rather than the source directly.
Larochelle et. al. [11] enhanced their LCLint tool to detect likely buffer overflows in C programs. The LCLint tool bases static analysis on annotations of the programs (or the libraries) that restrict the range of values a reference can have. The strength of LCLint is that the analysis is flow-sensitive, and thus more accurate. The downside of the LCLint tool is its inflexibility. The current LCLint tool is customized to deal with a set of predefined software bugs. It appears that extending LCLint for LSM verification would require a significant amount of effort (i.e. adding new annotation types). CQUAL, on the other hand, is more extensible by employing user-defined type qualifier lattices.
Necula et. al. [12] define the CCured type system. CCured leverages the fact that most C source is written in a type-safe manner to perform a variety of static checks on the source during compilation for things like buffer overflows. For things that cannot be checked statically, CCured introduces runtime checks into the code. This enables certain kinds of errors to be caught regardless of whether they can be found statically or dynamically. While we agree with this approach to verification, as yet the types of errors that CCured can find do not include authorization hook placement.
Koved et. al. [10] presented a technique for computing the access rights requirements of Java applications. Their approach uses more powerful programming analysis techniques: a context-sensitive interprocedural data flow analysis is employed. Although the analysis is performed on Java code, it is conceivable that such techniques can be applied to our problem domain as well.