MOdelchecking Programs for Security properties
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.
Model Checking An Entire Linux Distribution for Security Violations. PDF PS Unabridged Abstract 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 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 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 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 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.
We welcome questions, comments, bugs, and other feedback about the tool
via email to
mops@taverner.cs.berkeley.edu
