MOPS

MOdelchecking Programs for Security properties

We are now announcing a second public release of MOPS.

What. MOPS 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. In the long term, we envision building a database of rules of defensive programming that can be easily used to check software. At present, the release comes only with the code analysis tool, and the user must supply the properties to be checked. In the future, we hope to be able to distribute an extensive database of rules of defensive programming that can be used to guide the use of MOPS, but at present, we supply only the infrastructure to allow you to codify and verify security properties of interest to you. Also, we have not yet focused on the user interface and useability, so please think of the current version as a research prototype.

Where. The MOPS release is available here.

Who. This software was written by Hao Chen, in collaboration with David Wagner and with the assistance of Rob Johnson, David Schultz, and others. This work has been made possible by generous support from the DARPA CHATS program.

Feedback. We welcome questions, comments, bugs, and other feedback about the tool via email to mops@taverner.cs.berkeley.edu,

Paper trail. This tool was developed as part of the software security research project. We have written a research paper on the tool:

MOPS: an Infrastructure for Examining Security Properties of Software
Hao Chen and David Wagner. To appear at ACM CCS 2002. [also available in pdf]
You can also find a survey talk on MOPS given at the CHATS Summer 2002 PI meeting here. See also the paper "Setuid Demystified" for related work.

Related tools. ITS4, RATS, flawfinder, Splint, MC, Cqual, SLAM, ESC/Java, Blast. Moped.


The MOPS Authors (Hao Chen and David Wagner), mops@taverner.cs.berkeley.edu, http://www.cs.berkeley.edu/~daw/mops/.