MOdelchecking Programs for Security properties


We are now announcing a second public release of MOPS.

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.


The following releases are available:

MOPS 0.9.2 release: mops-0.9.2.tar.gz


Model Checking An Entire Linux Distribution for Security Violations. PDF PS Unabridged Abstract Benjamin Schwarz, Hao Chen, David Wagner, Geoff Morrison, Jacob West, Jeremy Lin, and Wei Tu. To appear in Proceedings of the 2005 Annual Computer Security Applications Conference (ACSAC), Tucson, AZ, December 2005.

Using Build-Integrated Static Checking to Preserve Correctness Invariants. PDF PS Abstract Hao Chen and Jonathan Shapiro. In Proceedings of the 11th ACM Conference on Computer and Communications Security (CCS), Washington, DC, October 2004.

Model checking one million lines of C code. PDF PS PPT slides Abstract Hao Chen, Drew Dean, and David Wagner. In Proceedings of the 11th Annual Network and Distributed System Security Symposium (NDSS), San Diego, CA, February 2004.

Setuid demystified. PDF PS PPT slides Abstract Hao Chen, David Wagner, and Drew Dean. In Proceedings of the 11th USENIX Security Symposium, pages 171--190, San Francisco, CA, August 2002.

MOPS: an infrastructure for examining security properties of software. PDF PS Abstract Hao Chen and David Wagner. In Proceedings of the 9th ACM Conference on Computer and Communications Security (CCS) , pages 235--244, Washington, DC, November 2002.


This software was written by Hao Chen and David Wagner, and with the assistance of Rob Johnson, Jeremy Lin, Geoff Morrison, David Schultz, Ben Schwarz, Wei Tu, and others. This work has been made possible by generous support from the DARPA CHATS program.

Contact Us

We welcome questions, comments, bugs, and other feedback about the tool via email to

Related Tools

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

The MOPS Authors (Hao Chen and David Wagner),
Last modified November 1, 2004.
Valid XHTML 1.1! Valid CSS!