Projects / MOdelchecking Programs for Security

MOdelchecking Programs for Security

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.


Recent releases

  •  01 Mar 2003 19:44

    No changes have been submitted for this release.


    Project Spotlight


    A Fluent OpenStack client API for Java.


    Project Spotlight

    TurnKey TWiki Appliance

    A TWiki appliance that is easy to use and lightweight.