MOPS (MOdelchecking Programs for Security) is a tool for finding security bugs in C programs and for verifying conformance to rules of defensive programming. This is targeted at developers writing security-critical programs and at security auditors reviewing the security of existing C code. MOPS is designed to check for violations of rules that can be expressed as temporal safety properties. A temporal safety property dictates the order of a sequence of operations. For example, in Unix systems, we might verify that the C program obeys the following rule: a setuid-root process should not execute an untrusted program without first dropping its root privilege. The current release is an early version of a research tool.
