MOPS

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

MOPS: an infrastructure for examining security properties of software

Full text

Pdf (237 KB)

Source

Conference on Computer and Communications Security archive
Proceedings of the 9th ACM conference on Computer and communications security table of contents

Washington, DC, USA

SESSION: Analysis and verification table of contents

Pages: 235 - 244

Year of Publication: 2002

ISBN:1-58113-612-9

Authors

Hao Chen	University of California at Berkeley, Berkeley, CA
David Wagner	University of California at Berkeley, Berkeley, CA

Sponsors

ACM: Association for Computing Machinery
SIGSAC: ACM Special Interest Group on Security, Audit, and Control

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 11, Downloads (12 Months): 102, Citation Count: 72

Additional Information:

abstract references cited by index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/586110.586142 What is a DOI?

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

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Ken Ashcraft , Dawson Engler, Using Programmer-Written Compiler Extensions to Catch Security Holes, Proceedings of the 2002 IEEE Symposium on Security and Privacy, p.143, May 12-15, 2002
	2	Thomas Ball , Sriram K. Rajamani, Automatically validating temporal safety properties of interfaces, Proceedings of the 8th international SPIN workshop on Model checking of software, p.103-122, May 2001, Toronto, Ontario, Canada
	3	Thomas Ball , Sriram K. Rajamani, The SLAM project: debugging system software via static analysis, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-3, January 16-18, 2002, Portland, Oregon
	4	Frédéric Besson , Thomas Jensen , Daniel Le Métayer , Tommy Thorn, Model checking security properties of control flow graphs, Journal of Computer Security, v.9 n.3, p.217-250, January 2001
	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	Hao Chen , David A. Wagner, MOPS: an Infrastructure for Examining Security Properties of Software, University of California at Berkeley, Berkeley, CA, 2002
	8	Hao Chen , David Wagner , Drew Dean, Setuid Demystified, Proceedings of the 11th USENIX Security Symposium, p.171-190, August 05-09, 2002
	9	D. Engler, B. Chelf, A. Chou, and S. Hallem. Checking system rules using system-specific, programmer-written compiler extensions. In OSDI, 2000.
	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.
	11	Jeffrey S. Foster , Manuel Fähndrich , Alexander Aiken, A theory of type qualifiers, Proceedings of the ACM SIGPLAN 1999 conference on Programming language design and implementation, p.192-203, May 01-04, 1999, Atlanta, Georgia, United States
	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	John E. Hopcroft , Jeffrey D. Ullman, Introduction To Automata Theory, Languages, And Computation, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1990
	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	Larry Koved , Marco Pistoia , Aaron Kershenbaum, Access rights analysis for Java, Proceedings of the 17th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications, November 04-08, 2002, Seattle, Washington, USA
	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.
	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	Xiaolan Zhang , Antony Edwards , Trent Jaeger, Using CQUAL for Static Analysis of Authorization Hook Placement, Proceedings of the 11th USENIX Security Symposium, p.33-48, August 05-09, 2002

CITED BY 72

	Yao-Wen Huang , Shih-Kun Huang , Tsung-Po Lin , Chung-Hung Tsai, Web application security assessment by fault injection and behavior monitoring, Proceedings of the 12th international conference on World Wide Web, May 20-24, 2003, Budapest, Hungary
	Antony Edwards , Trent Jaeger , Xiaolan Zhang, Runtime verification of authorization hook placement for the linux security modules framework, Proceedings of the 9th ACM conference on Computer and communications security, November 18-22, 2002, Washington, DC, USA
	Daniel C. DuVarney , V. N. Venkatakrishnan , Sandeep Bhatkar, SELF: a transparent security extension for ELF binaries, Proceedings of the 2003 workshop on New security paradigms, August 18-21, 2003, Ascona, Switzerland
	Emmanuel Geay , Eran Yahav , Stephen Fink, Continuous code-quality assurance with SAFE, Proceedings of the 2006 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 09-10, 2006, Charleston, South Carolina
	Gaurav S. Kc , Angelos D. Keromytis , Vassilis Prevelakis, Countering code-injection attacks with instruction-set randomization, Proceedings of the 10th ACM conference on Computer and communications security, October 27-30, 2003, Washington D.C., USA
	Dirk Beyer , Adam J. Chlipala , Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar, Invited talk: the blast query language for software verification, Proceedings of the 2004 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, p.201-202, August 24-25, 2004, Verona, Italy
	R. Sekar , V.N. Venkatakrishnan , Samik Basu , Sandeep Bhatkar , Daniel C. DuVarney, Model-carrying code: a practical approach for safe execution of untrusted applications, Proceedings of the nineteenth ACM symposium on Operating systems principles, October 19-22, 2003, Bolton Landing, NY, USA
	Brian Chess , Gary McGraw, Static Analysis for Security, IEEE Security and Privacy, v.2 n.6, p.76-79, November 2004
	Yao-Wen Huang , Fang Yu , Christian Hang , Chung-Hung Tsai , Der-Tsai Lee , Sy-Yen Kuo, Securing web application code by static analysis and runtime protection, Proceedings of the 13th international conference on World Wide Web, May 17-20, 2004, New York, NY, USA
	Rajeev Alur , P. Madhusudan, Visibly pushdown languages, Proceedings of the thirty-sixth annual ACM symposium on Theory of computing, June 13-16, 2004, Chicago, IL, USA
	Darrell Reimer , Edith Schonberg , Kavitha Srinivas , Harini Srinivasan , Bowen Alpern , Robert D. Johnson , Aaron Kershenbaum , Larry Koved, SABER: smart analysis based error reduction, ACM SIGSOFT Software Engineering Notes, v.29 n.4, July 2004
	Trent Jaeger , Antony Edwards , Xiaolan Zhang, Consistency analysis of authorization hook placement in the Linux security modules framework, ACM Transactions on Information and System Security (TISSEC), v.7 n.2, p.175-205, May 2004
	Ted Kremenek , Ken Ashcraft , Junfeng Yang , Dawson Engler, Correlation exploitation in error ranking, ACM SIGSOFT Software Engineering Notes, v.29 n.6, November 2004
	Darrell Reimer , Edith Schonberg , Kavitha Srinivas , Harini Srinivasan , Julian Dolby , Aaron Kershenbaum , Larry Koved, Validating structural properties of nested objects, Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 24-28, 2004, Vancouver, BC, CANADA
	Hao Chen , Jonathan S. Shapiro, Using build-integrated static checking to preserve correctness invariants, Proceedings of the 11th ACM conference on Computer and communications security, October 25-29, 2004, Washington DC, USA
	Angelos D. Keromytis , Janak Parekh , Philip N. Gross , Gail Kaiser , Vishal Misra , Jason Nieh , Dan Rubenstein , Sal Stolfo, A holistic approach to service survivability, Proceedings of the 2003 ACM workshop on Survivable and self-regenerative systems: in association with 10th ACM Conference on Computer and Communications Security, p.11-22, October 31-31, 2003, Fairfax, VA
	Dirk Beyer , Adam J. Chlipala , Thomas A. Henzinger , Ranjit Jhala , Rupak Majumdar, Invited talk: the blast query language for software verification, Proceedings of the 6th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.1-2, August 24-26, 2004, Verona, Italy
	Vinod Ganapathy , Sanjit A. Seshia , Somesh Jha , Thomas W. Reps , Randal E. Bryant, Automatic discovery of API-level exploits, Proceedings of the 27th international conference on Software engineering, May 15-21, 2005, St. Louis, MO, USA
	Jay-Evan J. Tevis , John A. Hamilton, Methods for the prevention, detection and removal of software security vulnerabilities, Proceedings of the 42nd annual Southeast regional conference, April 02-03, 2004, Huntsville, Alabama
	Crispin Cowan, Software Security for Open-Source Systems, IEEE Security and Privacy, v.1 n.1, p.38-45, January 2003
	Christian Skalka, Trace effects and object orientation, Proceedings of the 7th ACM SIGPLAN international conference on Principles and practice of declarative programming, p.139-150, July 11-13, 2005, Lisbon, Portugal
	Sam Weber , Paul A. Karger , Amit Paradkar, A software flaw taxonomy: aiming tools at security, ACM SIGSOFT Software Engineering Notes, v.30 n.4, July 2005
	Ranjit Jhala , Rupak Majumdar, Path slicing, ACM SIGPLAN Notices, v.40 n.6, June 2005
	Godmar Back , Wilson C. Hsieh, The KaffeOS Java runtime system, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.4, p.583-630, July 2005
	Rajeev Alur , Michael Benedikt , Kousha Etessami , Patrice Godefroid , Thomas Reps , Mihalis Yannakakis, Analysis of recursive state machines, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.4, p.786-818, July 2005
	Michael Gegick , Laurie Williams, Matching attack patterns to security vulnerabilities in software-intensive system designs, ACM SIGSOFT Software Engineering Notes, v.30 n.4, July 2005
	Rajeev Alur , Swarat Chaudhuri , P. Madhusudan, A fixpoint calculus for local and global program flows, ACM SIGPLAN Notices, v.41 n.1, p.153-165, January 2006
	Thomas Reps , Gogul Balakrishnan , Junghee Lim, Intermediate-representation recovery from low-level code, Proceedings of the 2006 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 09-10, 2006, Charleston, South Carolina
	Thomas Reps , Stefan Schwoon , Somesh Jha , David Melski, Weighted pushdown systems and their application to interprocedural dataflow analysis, Science of Computer Programming, v.58 n.1-2, p.206-263, October 2005
	Jun Xu , Peng Ning , Chongkyung Kil , Yan Zhai , Chris Bookholt, Automatic diagnosis and response to memory corruption vulnerabilities, Proceedings of the 12th ACM conference on Computer and communications security, November 07-11, 2005, Alexandria, VA, USA
	Jinlin Yang , David Evans , Deepali Bhardwaj , Thirumalesh Bhat , Manuvir Das, Perracotta: mining temporal API rules from imperfect traces, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China
	Olga Gelbart , Bhagirath Narahari , Rahul Simha, SPEE: a secure program execution environment tool using code integrity checking, Journal of High Speed Networks, v.15 n.1, p.21-32, January 2006
	Xiaolan Zhang , Larry Koved , Marco Pistoia , Sam Weber , Trent Jaeger , Guillaume Marceau , Liangzhao Zeng, The case for analysis preserving language transformation, Proceedings of the 2006 international symposium on Software testing and analysis, July 17-20, 2006, Portland, Maine, USA
	Junfeng Yang , Ted Kremenek , Yichen Xie , Dawson Engler, MECA: an extensible, expressive system and language for statically checking security properties, Proceedings of the 10th ACM conference on Computer and communications security, October 27-30, 2003, Washington D.C., USA
	Diomidis Spinellis , Panagiotis Louridas, A framework for the static verification of api calls, Journal of Systems and Software, v.80 n.7, p.1156-1168, July, 2007
	David Brumley , Juan Caballero , Zhenkai Liang , James Newsome , Dawn Song, Towards automatic discovery of deviations in binary implementations with applications to error detection and fingerprint generation, Proceedings of 16th USENIX Security Symposium on USENIX Security Symposium, p.1-16, August 06-10, 2007, Boston, MA
	Dan Tsafrir , Tomer Hertz , David Wagner , Dilma Da Silva, Portably solving file TOCTTOU races with hardness amplification, Proceedings of the 6th USENIX Conference on File and Storage Technologies, p.1-18, February 26-29, 2008, San Jose, California
	Mithun Acharya, Automatic generation and inference of interface properties from program source code, Companion to the 21st ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 22-26, 2006, Portland, Oregon, USA
	Nic Volanschi, Condate: a proto-language at the confluence between checking and compiling, Proceedings of the 8th ACM SIGPLAN symposium on Principles and practice of declarative programming, July 10-12, 2006, Venice, Italy
	Magiel Bruntink , Arie van Deursen , Tom Tourwé, Discovering faults in idiom-based exception handling, Proceeding of the 28th international conference on Software engineering, May 20-28, 2006, Shanghai, China
	Michael Gegick , Laurie Williams, On the design of more secure software-intensive systems by use of attack patterns, Information and Software Technology, v.49 n.4, p.381-397, April, 2007
	Wei Le , Mary Lou Soffa, Refining buffer overflow detection via demand-driven path-sensitive analysis, Proceedings of the 7th ACM SIGPLAN-SIGSOFT workshop on Program analysis for software tools and engineering, p.63-68, June 13-14, 2007, San Diego, California, USA
	David Brumley , Dawn Song, Privtrans: automatically partitioning programs for privilege separation, Proceedings of the 13th conference on USENIX Security Symposium, p.5-5, August 09-13, 2004, San Diego, CA
	Rob Johnson , David Wagner, Finding user/kernel pointer bugs with type inference, Proceedings of the 13th conference on USENIX Security Symposium, p.9-9, August 09-13, 2004, San Diego, CA
	Jinpeng Wei , Calton Pu, TOCTTOU vulnerabilities in UNIX-style file systems: an anatomical study, Proceedings of the 4th conference on USENIX Conference on File and Storage Technologies, p.12-12, December 13-16, 2005, San Francisco, CA
	Mihai Christodorescu , Somesh Jha, Static analysis of executables to detect malicious patterns, Proceedings of the 12th conference on USENIX Security Symposium, p.12-12, August 04-08, 2003, Washington, DC
	Stelios Sidiroglou , Michael E. Locasto , Stephen W. Boyd , Angelos D. Keromytis, Building a reactive immune system for software services, Proceedings of the USENIX Annual Technical Conference 2005 on USENIX Annual Technical Conference, p.11-11, April 10-15, 2005, Anaheim, CA
	Karl Mazurak , Steve Zdancewic, ABASH: finding bugs in bash scripts, Proceedings of the 2007 workshop on Programming languages and analysis for security, June 14-14, 2007, San Diego, California, USA
	Ted Kremenek , Paul Twohey , Godmar Back , Andrew Ng , Dawson Engler, From uncertainty to belief: inferring the specification within, Proceedings of the 7th symposium on Operating systems design and implementation, November 06-08, 2006, Seattle, Washington
	John Kodumal , Alex Aiken, Regularly annotated set constraints, ACM SIGPLAN Notices, v.42 n.6, June 2007
	Mark Grechanik, Finding errors in components that exchange xml data, Proceedings of the twenty-second IEEE/ACM international conference on Automated software engineering, November 05-09, 2007, Atlanta, Georgia, USA
	Mark Grechanik, Finding Errors in Interoperating Components, Proceedings of the Second International Workshop on Incorporating COTS Software into Software Systems: Tools and Techniques, p.3, May 20-26, 2007
	Dirk Beyer , Adam J. Chlipala , Rupak Majumdar, Generating Tests from Counterexamples, Proceedings of the 26th International Conference on Software Engineering, p.326-335, May 23-28, 2004
	Stephan Neuhaus , Thomas Zimmermann , Christian Holler , Andreas Zeller, Predicting vulnerable software components, Proceedings of the 14th ACM conference on Computer and communications security, October 28-31, 2007, Alexandria, Virginia, USA
	Wei Le , Mary Lou Soffa, Marple: a demand-driven path-sensitive buffer overflow detector, Proceedings of the 16th ACM SIGSOFT International Symposium on Foundations of software engineering, November 09-14, 2008, Atlanta, Georgia
	Christian Skalka, Types and trace effects for object orientation, Higher-Order and Symbolic Computation, v.21 n.3, p.239-282, September 2008
	Gang Tan , Jason Croft, An empirical security study of the native code in the JDK, Proceedings of the 17th conference on Security symposium, p.365-377, July 28-August 01, 2008, San Jose, CA
	Lin Tan , Xiaolan Zhang , Xiao Ma , Weiwei Xiong , Yuanyuan Zhou, AutoISES: automatically inferring security specifications and detecting violations, Proceedings of the 17th conference on Security symposium, p.379-394, July 28-August 01, 2008, San Jose, CA
	Mark Gabel , Zhendong Su, Symbolic mining of temporal specifications, Proceedings of the 30th international conference on Software engineering, May 10-18, 2008, Leipzig, Germany
	A. Prasad Sistla , V. N. Venkatakrishnan , Michelle Zhou , Hilary Branske, CMV: automatic verification of complete mediation for java virtual machines, Proceedings of the 2008 ACM symposium on Information, computer and communications security, March 18-20, 2008, Tokyo, Japan
	Nic Volanschi , Christian Rinderknecht, Unparsed patterns: easy user-extensibility of program manipulation tools, Proceedings of the 2008 ACM SIGPLAN symposium on Partial evaluation and semantics-based program manipulation, January 07-08, 2008, San Francisco, California, USA
	Deguang Kong , Quan Zheng , Chao Chen , Jianmei Shuai , Ming Zhu, ISA: a source code static vulnerability detection system based on data fusion, Proceedings of the 2nd international conference on Scalable information systems, June 06-08, 2007, Suzhou, China
	Octavian Udrea , Cristian Lumezanu , Jeffrey S. Foster, Rule-based static analysis of network protocol implementations, Information and Computation, v.206 n.2-4, p.130-157, February, 2008
	Emre C. Sezer , Peng Ning , Chongkyung Kil , Jun Xu, Memsherlock: an automated debugger for unknown memory corruption vulnerabilities, Proceedings of the 14th ACM conference on Computer and communications security, October 28-31, 2007, Alexandria, Virginia, USA
	Mithun Acharya , Tao Xie , Jian Pei , Jun Xu, Mining API patterns as partial orders from source code: from usage scenarios to specifications, Proceedings of the the 6th joint meeting of the European software engineering conference and the ACM SIGSOFT symposium on The foundations of software engineering, September 03-07, 2007, Dubrovnik, Croatia
	Christian Skalka , Scott Smith , David Van horn, Types and trace effects of higher order programs, Journal of Functional Programming, v.18 n.2, p.179-249, March 2008
	Arshad Jhumka , Felix Freiling , Christof Fetzer , Neeraj Suri, An approach to synthesise safe systems, International Journal of Security and Networks, v.1 n.1/2, p.62-74, September 2006
	Eric Larson, Assessing work for static software bug detection, Proceedings of the 1st ACM international workshop on Empirical assessment of software engineering languages and technologies: held in conjunction with the 22nd IEEE/ACM International Conference on Automated Software Engineering (ASE) 2007, p.7-12, November 05-05, 2007, Atlanta, Georgia
	Dan Tsafrir , Tomer Hertz , David Wagner , Dilma Da Silva, Portably solving file races with hardness amplification, ACM Transactions on Storage (TOS), v.4 n.3, p.1-30, November 2008
	Laura Bozzelli, CaRet With Forgettable Past, Electronic Notes in Theoretical Computer Science (ENTCS), 231, p.343-361, March, 2009
	Rajeev Alur , P. Madhusudan, Adding nesting structure to words, Journal of the ACM (JACM), v.56 n.3, p.1-43, May 2009
	Syrine Tlili , Mourad Debbabi, Interprocedural and Flow-Sensitive Type Analysis for Memory and Type Safety of C Code, Journal of Automated Reasoning, v.42 n.2-4, p.265-300, April 2009