When we first examined this problem, it appeared that an extensive static analysis tool with inter-procedural data-flow analysis capability was needed. Such tools either are not available to the public, do not work on Linux kernel (due to scalability issues or C coding style issues), or are too complicated to customize for our problem. A closer look at the nature of the verification problem, however, reveals that a less-powerful static analysis tool might be sufficient. For verification purposes, we do not care about the exact value of the controlled object. We only care about its authorization state (i.e., authorized or non-authorized) and that its variable is not re-assigned. Some limited source analysis may be necessary to verify that the expected conditions apply, but this should be quite simple in most cases.