MOPS: an infrastructure for examining security properties of software

By Hao Chen, David A. Wagner. Conference on Computer and Communications Security, 2002

474 citations recorded by the source corpus.

Subfields: Artificial Intelligence, Software

View Paper: https://www.semanticscholar.org/paper/aff94f59f947661e5edcd2ba530193ed927a1f17

How researchers see this paper

The researchers whose trusted networks rank it highest, strongest advocate first. Every researcher gets a different order.

In Artificial Intelligence

In Software

Citations in the corpus

Visibly pushdown languages (2004, background): “bounds on stack size such as “if the number of interrupthandlers in the call-stack currently is less than 5, then a property p holds” require inspection of the stack, and decision procedures for certain classes of stack properties already exist [17, 13, 14, 12].”
Countering code-injection attacks with instruction-set randomization (2003, methodology): “MOPS [20] is an automated formal-methods framework for finding bugs in securityrelevant software, or verifying their absence.”
The software model checker Blast (2007, background): “Secure programming practice requires that certain system calls that run untrusted programs should not be made with root privileges [18], because the privileged process has full permission to the system.”
Predicting vulnerable software components (2007, methodology): “Another approach is to use model checking [3, 4].”
Web application security assessment by fault injection and behavior monitoring (2003, methodology): “In: DARPA Information Survivability Conference & Exposition II, 2, 257-262, 2001.”
Perracotta: mining temporal API rules from imperfect traces (2006, background): “This section provides background on temporal properties and program verification, and discusses related work in static and dynamic property inference.”
A survey on automated dynamic malware-analysis techniques and tools (2012, methodology): “If the source code is available, static analysis tools can help finding memory corruption flaws [Chen et al. 2004; Chen and Wagner 2002; Feng et al. 2004] and prove the correctness of models for a given system.”
DECOR: A Method for the Specification and Detection of Code and Design Smells (2010, background): “Model checkers such as BLAST [41] and MOPS [42] also”
Semantics-aware malware detection (2005, result): “Our work is closely related to previous results on static analysis techniques for verifying security properties of software [1, 3–5, 19, 24].”
A Temporal Logic of Nested Calls and Returns (2004, methodology): “" It is worth noting that the relevance of stack inspection for specifying correctness of security properties and calling sequences of interrupt handlers has been identi ed by many researchers, and decision procedures for checking speci c properties already exist [18, 10, 13, 9].”