More Web Proxy on the site http://driver.im/

Article

MOPS: an infrastructure for examining security properties of software

Authors:

David WagnerAuthors Info & Claims

CCS '02: Proceedings of the 9th ACM conference on Computer and communications security

Pages 235 - 244

https://doi.org/10.1145/586110.586142

Published: 18 November 2002 Publication History

Abstract

We describe a formal approach for finding bugs in security-relevant software and verifying their absence. The idea is as follows: we identify rules of safe programming practice, encode them as safety properties, and verify whether these properties are obeyed. Because manual verification is too expensive, we have built a program analysis tool to automate this process. Our program analysis models the program to be verified as a pushdown automaton, represents the security property as a finite state automaton, and uses model checking techniques to identify whether any state violating the desired security goal is reachable in the program. The major advantages of this approach are that it is sound in verifying the absence of certain classes of vulnerabilities, that it is fully interprocedural, and that it is efficient and scalable. Experience suggests that this approach will be useful in finding a wide range of security vulnerabilities in large programs efficiently.

References

[1]

K. Ashcraft and D. Engler. Using programmer-written compiler extensions to catch security holes. In Proceedings of IEEE Security and Privacy 2002, 2002.

Digital Library

[2]

T. Ball and S. K. Rajamani. Automatically validating temporal safety properties of interfaces. In SPIN 2001, Workshop on Model Checking of Software, 2001.

Digital Library

[3]

T. Ball and S. K. Rajamani. The SLAM project: Debugging system software via static analysis. In POPL 2002, 2002.

Digital Library

[4]

F. Besson, T. Jensen, D. L. Metayer, and T. Thorn. Model checking security properties of control flow graphs. Journal of Computer Security, 9:217--250, 2001.

Digital Library

[5]

M. Bishop and M. Dilger. Checking for race conditions in file access. Computing Systems, 9(2):131--152, 1996.

[6]

CERT. CERT Advisory CA-1997-16: ftpd signal handling vulnerability. http://www.cert.org/advisories/CA-1997-16.html.

[7]

H. Chen and D. Wagner. MOPS: an infrastructure for examining security properties of software. Technical Report UCB//CSD-02-1197, UC Berkeley, 2002.

Digital Library

[8]

H. Chen, D. Wagner, and D. Dean. Setuid demystified. In Proceedings of the Eleventh Usenix Security Symposium, San Francisco, CA, 2002.

Digital Library

[9]

D. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In OSDI, 2000.

Digital Library

[10]

J. Esparza, D. Hansel, P. Rossmanith, and S. Schwoon. Efficient algorithms for model checking pushdown systems. Technical report, Technische Universität München, 2000.

Digital Library

[11]

J. Foster, M. Fähndrich, and A. Aiken. A theory of type qualifiers. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'99), May 1999.

Digital Library

[12]

D. Greenman. Serious security bug in wu-ftpd v2.4. http://online.securityfocus.com/archive/1/6056/1997-01-04/1997-01-10/2.

[13]

J. Hopcroft and J. Ullman. Introduction to automata theory, languages, and computation. Addison-Wesley, 1979.

Digital Library

[14]

T. Jensen, D. L. Metayer, and T. Thorn. Verification of control flow based security properties. In Proceedings of the 1999 IEEE Symposium on Security and Privacy, 1999.

[15]

L. Koved, M. Pistoia, and A. Kershenbaum. Access rights analysis for java. In Proceedings of the 17th Annual ACM Conference on Object-Oriented Programming, Systems, Languages, and Applications, 2002.

Digital Library

[16]

Sendmail Inc. Sendmail workaround for linux capabilities bug. http://www.sendmail.org/sendmail.8.10.1.LINUX-SECURITY.txt.

[17]

U. Shankar, K. Talwar, J. S. Foster, and D. Wagner. Detecting format string vulnerabilities with type qualifiers. In Proceedings of the 10th USENIX Security Symposium, 2001.

Digital Library

[18]

D. Wagner, J. Foster, E. Brewer, and A. Aiken. A first step towards automated detection of buffer overrun vulnerabilities. In Proceedings of NDSS 2000, 2000.

[19]

M. Zalewski. Multiple local sendmail vulnerabilities. http://razor.bindview.com/publish/advisories/adv_sm812.html.

[20]

X. Zhang, A. Edwards, and T. Jaeger. Using CQUAL for static analysis of authorization hook placement. In Proceedings of the Eleventh Usenix Security Symposium, August 2002.

Digital Library

Cited By

Okebule TAdeyemo OOlatunji KAwe A(2022)Review of Works Content Analyzer for Information Leakage Detection and Prevention in Android Smart DevicesABUAD International Journal of Natural and Applied Sciences10.53982/aijnas.2022.0201.02-j2:1(12-28)Online publication date: 30-Mar-2022
https://doi.org/10.53982/aijnas.2022.0201.02-j
Li XWang GWang CQin YWang N(2022)Software Source Code Security Audit Algorithm Supporting Incremental Checking2022 IEEE 7th International Conference on Smart Cloud (SmartCloud)10.1109/SmartCloud55982.2022.00015(53-58)Online publication date: Oct-2022
https://doi.org/10.1109/SmartCloud55982.2022.00015
Zhang HBi YGuo HSun WLi J(2022)ISVSF: Intelligent Vulnerability Detection Against Java via Sentence-Level Pattern ExploringIEEE Systems Journal10.1109/JSYST.2021.307215416:1(1032-1043)Online publication date: Mar-2022
https://doi.org/10.1109/JSYST.2021.3072154
Show More Cited By

Index Terms

MOPS: an infrastructure for examining security properties of software

Recommendations

Model Checking of Component Protocol Conformance -- Optimizations by Reducing False Negatives

In past years, a number of works considered behavioral protocols of components and discussed approaches for automatically checking of compatibality of protocols (protocol conformance) in component-based systems. The approaches are usually model-checking ...
Bounded model checking of high-integrity software
HILT '13: Proceedings of the 2013 ACM SIGAda annual conference on High integrity language technology

Model checking [5] is an automated algorithmic technique for exhaustive verification of systems, described as finite state machines, against temporal logic [9] specifications. It has been used successfully to verify hardware at an industrial scale [6]. ...
Handling loops in bounded model checking of C programs via k-induction

The first attempts to apply the k-induction method to software verification are only recent. In this paper, we present a novel proof by induction algorithm, which is built on the top of a symbolic context-bounded model checker and uses an iterative ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CCS '02: Proceedings of the 9th ACM conference on Computer and communications security

November 2002

284 pages

ISBN:1581136129

DOI:10.1145/586110

Editor:
Vijay Atluri
Rutgers University
,
General Chair:
Sushil Jajodia
George Mason University
,
Program Chair:
Ravi Sandhu
SingleSignOn.Net and George Mason University

Copyright © 2002 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 18 November 2002

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Conference

CCS02

Sponsor:

CCS02: ACM Conference on Computer and Communications Security

November 18 - 22, 2002

Washington, DC, USA

Acceptance Rates

Overall Acceptance Rate 1,261 of 6,999 submissions, 18%

Upcoming Conference

CCS '25

Sponsor:
sigsac

ACM SIGSAC Conference on Computer and Communications Security

October 13 - 17, 2025

Taipei , Taiwan

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

198
Total Citations
View Citations
1,191
Total Downloads

Downloads (Last 12 months)25
Downloads (Last 6 weeks)3

Reflects downloads up to 04 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

Okebule TAdeyemo OOlatunji KAwe A(2022)Review of Works Content Analyzer for Information Leakage Detection and Prevention in Android Smart DevicesABUAD International Journal of Natural and Applied Sciences10.53982/aijnas.2022.0201.02-j2:1(12-28)Online publication date: 30-Mar-2022
https://doi.org/10.53982/aijnas.2022.0201.02-j
Li XWang GWang CQin YWang N(2022)Software Source Code Security Audit Algorithm Supporting Incremental Checking2022 IEEE 7th International Conference on Smart Cloud (SmartCloud)10.1109/SmartCloud55982.2022.00015(53-58)Online publication date: Oct-2022
https://doi.org/10.1109/SmartCloud55982.2022.00015
Zhang HBi YGuo HSun WLi J(2022)ISVSF: Intelligent Vulnerability Detection Against Java via Sentence-Level Pattern ExploringIEEE Systems Journal10.1109/JSYST.2021.307215416:1(1032-1043)Online publication date: Mar-2022
https://doi.org/10.1109/JSYST.2021.3072154
Ferles KStephens JDillig I(2021)Verifying correct usage of context-free API protocolsProceedings of the ACM on Programming Languages10.1145/34342985:POPL(1-30)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434298
Laverdière MJulien KMerlo E(2021)RBAC protection-impacting changes identificationInformation and Software Technology10.1016/j.infsof.2021.106630139:COnline publication date: 23-Aug-2021
https://dl.acm.org/doi/10.1016/j.infsof.2021.106630
Zhang GWang PYue TZhou XLu K(2021)MEBS: Uncovering Memory Life-Cycle Bugs in Operating System KernelsJournal of Computer Science and Technology10.1007/s11390-021-1593-436:6(1248-1268)Online publication date: 30-Nov-2021
https://doi.org/10.1007/s11390-021-1593-4
van Oorschot Pvan Oorschot P(2021)Software Security—Exploits and Privilege EscalationComputer Security and the Internet10.1007/978-3-030-83411-1_6(155-182)Online publication date: 14-Oct-2021
https://doi.org/10.1007/978-3-030-83411-1_6
Ispoglou KAustin DMohan VPayer MCapkun SRoesner F(2020)FuzzGenProceedings of the 29th USENIX Conference on Security Symposium10.5555/3489212.3489340(2271-2287)Online publication date: 12-Aug-2020
https://dl.acm.org/doi/10.5555/3489212.3489340
Wang PLu KLi GZhou X(2019)DFTrackerFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-016-6383-813:2(247-263)Online publication date: 1-Apr-2019
https://dl.acm.org/doi/10.1007/s11704-016-6383-8
Bueno DSakallah K(2019)euforia: Complete Software Model Checking with Uninterpreted FunctionsVerification, Model Checking, and Abstract Interpretation10.1007/978-3-030-11245-5_17(363-385)Online publication date: 11-Jan-2019
https://doi.org/10.1007/978-3-030-11245-5_17
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents