Model checking is a method for formally verifying that a model satisfies a specified property [vJ11, p. 1255].
Model checking algorithms typically entail enumerating the program state space to determine if the desired properties hold.
Example 1 [CDW04]
Developed by UC Berkeley, MOdelchecking Programs for Security properties (MOPS) is a static (compile-time) analysis tool, which given a program and a security property (expressed as a finite-state automaton), checks whether the program can violate the security property.
The security properties that MOPS checks are temporal safety properties, i.e., properties requiring that programs perform certain security-relevant operations in certain orders.
An example of a temporal security property is whether a setuid-root program drops root privileges before executing an untrusted program; see Fig. 1.
Fig. 1: An example of a finite-state automaton specifying a temporal security property [CDW04, Figure 1(a)]
References
[CDW04]
H. Chen, D. Dean, and D. Wagner, Model Checking One Million Lines of C Code, in NDSS, 2004.
