poster

A buffer overflow benchmark for software model checkers

Authors:

Thomas E. Hart,

Marsha Chechik,

David LieAuthors Info & Claims

ASE '07: Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering

Pages 389 - 392

https://doi.org/10.1145/1321631.1321691

Published: 05 November 2007 Publication History

Abstract

Software model checking based on abstraction-refinement has recently achieved widespread success in verifying API conformance in device drivers, and we believe this success can be replicated for the problem of buffer overflow detection. This paper presents a publicly-available benchmark suite to help guide and evaluate this research. The benchmark consists of 298 code fragments of varying complexity capturing 22 buffer overflow vulnerabilities in 12 open source applications. We give a preliminary evaluation of the benchmark using the SatAbs model checker

References

[1]

T. Ball and S. Rajamani. "The SLAM Toolkit". In Proc. CAV'01, volume 2102 of LNCS, pages 260--264, 2001.

Digital Library

[2]

S. Chaki and S. Hissam. "Certifying the Absence of Buffer Overflows". Tech. Report CMU/SEI-2006-TN-030, SEI, 2006.

[3]

E. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith. "Counterexample-Guided Abstraction Refinement". In Proc. CAV'00, volume 1855 of LNCS, pages 154--169, 2000.

Digital Library

[4]

E. Clarke, D. Kroening, and F. Lerda."A Tool for Checking ANSI-C Programs". In Proc. TACAS'04, volume 2988 of LNCS, pages 168--176, 2004.

[5]

E. Clarke, D. Kroening, N. Sharygina, and K. Yorav. "SATABS: SAT--based Predicate Abstraction for ANSI-C". In Proc. TACAS'05, volume 3440 of LNCS, pages 570--574, 2005.

Digital Library

[6]

CVE - Common Vulnerabilities and Exposures. http://cve.mitre.org/.

[7]

S. Graf and H. Saïdi. "Construction of Abstract State Graphs with PVS". In Proc. CAV'97, volume 1254 of LNCS, pages 72--83, 1997.

Digital Library

[8]

B. Hackett, M. Das, D. Wang, and Z. Yang. "Modular Checking for Buffer Overflows in the Large". In Proc. ICSE'06, pages 232--241, 2006.

Digital Library

[9]

T. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. "Lazy Abstraction". In Proc. POPL'02, pages 58--70, 2002.

Digital Library

[10]

R. Jhala and K. McMillan. "Array Abstractions from Proofs". In Proc. CAV'07, volume 4590 of LNCS. Springer, 2007.

Digital Library

[11]

K. Kratkiewicz and R. Lippmann. "Using a Diagnostic Corpus of C Programs to Evaluate Buffer Overflow Detection by Static Analysis Tools". In Proc. BUGS'05, 2005.

[12]

D. Kroening, A. Groce, and E. Clarke. "Counterexample Guided Abstraction Refinement via Program Execution". In Proc. Int. Conf. on Formal Eng. Methods (ICFEM'04), volume 3308 of LNCS, pages 224--238, 2004.

[13]

D. Kroening and G. Weissenbacher. "Counterexamples with Loops for Predicate Abstraction". In Proc. CAV'06, volume 4144 of LNCS, pages 152--165, 2006.

Digital Library

[14]

W. Visser, K. Havelund, G. Brat, S. Park, and F. Lerda. "Model Checking Programs". Journal of Automated Software Engineering, 10(2), April 2003.

Digital Library

[15]

D. Wagner, J. S. Foster, E. A. Brewer, and A. Aiken. "A First Step towards Automated Detection of Buffer Overrun Vulnerabilities". In Proc. NDSS'00, pages 3--17, 2000.

[16]

J. Wilander and M. Kamkar. "A Comparison of Publicly Available Tools for Static Intrusion Prevention". In Proc. 7th Nordic Workshop on Secure IT Systems, pages 68--84, 2002.

[17]

Y. Xie, A. Chou, and D. R. Engler. "ARCHER: Using Symbolic, Path-Sensitive Analysis to Detect Memory Access Errors". In Proc. ESEC/FSE-11, pages 327--336, 2003.

Digital Library

[18]

M. Zitser, R. Lippmann, and T. Leek. "Testing Static Analysis Tools Using Exploitable Buffer Overflows from Open Source Code". In Proc. SIGSOFT'04/FSE-12, pages 97--106, 2004.

Digital Library

Cited By

Al-Bataineh OMoonen LVidziunas L(2024)Extending the range of bugs that automated program repair can handleJournal of Systems and Software10.1016/j.jss.2023.111918209(111918)Online publication date: Mar-2024
https://doi.org/10.1016/j.jss.2023.111918
Berthier NDe Oliveira SKosmatov NLonguet DSoulat RHong JLanperne MPark JCerny TShahriar H(2023)An Efficient Black-Box Support of Advanced Coverage Criteria for KleeProceedings of the 38th ACM/SIGAPP Symposium on Applied Computing10.1145/3555776.3577713(1706-1715)Online publication date: 7-Jun-2023
https://doi.org/10.1145/3555776.3577713
Wu XZheng WXia XLo D(2022)Data Quality Matters: A Case Study on Data Label Correctness for Security Bug Report PredictionIEEE Transactions on Software Engineering10.1109/TSE.2021.306372748:7(2541-2556)Online publication date: 1-Jul-2022
https://doi.org/10.1109/TSE.2021.3063727
Show More Cited By

Index Terms

A buffer overflow benchmark for software model checkers
1. Software and its engineering
  1. Software organization and properties
    1. Software functional properties
      1. Formal methods
        Model checking
2. Theory of computation
  1. Logic
    1. Verification by model checking

Recommendations

Realization of Buffer Overflow
IFITA '10: Proceedings of the 2010 International Forum on Information Technology and Applications - Volume 01

In recent decades, the buffer overflow has been a source of many serious security issues. In recent years, by the CERT/CC (Computer Emergency Response Term/Coodination Center) issued advice on the buffer overflow vulnerability for more than accounted ...
Buffer overflow and format string overflow vulnerabilities
Special issue: Security software

Buffer overflow vulnerabilities are among the most widespread of security problems. Numerous incidents of buffer overflow attacks have been reported and many solutions have been proposed, but a solution that is both complete and highly practical is yet ...
The software model checker Blast: Applications to software engineering

Blast is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal safety property, Blast either statically proves that the program satisfies the safety property, or provides an execution path ...

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences

ASE '07: Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering

November 2007

590 pages

ISBN:9781595938824

DOI:10.1145/1321631

General Chair:
Kurt Stirewalt
Michigan State University, USA
,
Program Chairs:
Alexander Egyed
Teknowledge Corporation, USA
,
Bernd Fischer
University of Southampton, UK

Copyright © 2007 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: 05 November 2007

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Poster

Conference

ASE07

Sponsor:

ASE07: International Conference on Automated Software Engineering 2007

November 5 - 9, 2007

Georgia, Atlanta, USA

Acceptance Rates

Overall Acceptance Rate 82 of 337 submissions, 24%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

66
Total Citations
View Citations
798
Total Downloads

Downloads (Last 12 months)19
Downloads (Last 6 weeks)2

Reflects downloads up to 07 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Al-Bataineh OMoonen LVidziunas L(2024)Extending the range of bugs that automated program repair can handleJournal of Systems and Software10.1016/j.jss.2023.111918209(111918)Online publication date: Mar-2024
https://doi.org/10.1016/j.jss.2023.111918
Berthier NDe Oliveira SKosmatov NLonguet DSoulat RHong JLanperne MPark JCerny TShahriar H(2023)An Efficient Black-Box Support of Advanced Coverage Criteria for KleeProceedings of the 38th ACM/SIGAPP Symposium on Applied Computing10.1145/3555776.3577713(1706-1715)Online publication date: 7-Jun-2023
https://doi.org/10.1145/3555776.3577713
Wu XZheng WXia XLo D(2022)Data Quality Matters: A Case Study on Data Label Correctness for Security Bug Report PredictionIEEE Transactions on Software Engineering10.1109/TSE.2021.306372748:7(2541-2556)Online publication date: 1-Jul-2022
https://doi.org/10.1109/TSE.2021.3063727
Al-Bataineh OMoonen L(2022)Towards Extending the Range of Bugs That Automated Program Repair Can Handle2022 IEEE 22nd International Conference on Software Quality, Reliability and Security (QRS)10.1109/QRS57517.2022.00031(209-220)Online publication date: Dec-2022
https://doi.org/10.1109/QRS57517.2022.00031
Khoury R(2022)A Taxonomy of Software Flaws Leading to Buffer Overflows2022 IEEE 22nd International Conference on Software Quality, Reliability and Security (QRS)10.1109/QRS57517.2022.00011(1-8)Online publication date: Dec-2022
https://doi.org/10.1109/QRS57517.2022.00011
Al-Bataineh OGrishina AMoonen L(2021)Towards More Reliable Automated Program Repair by Integrating Static Analysis Techniques2021 IEEE 21st International Conference on Software Quality, Reliability and Security (QRS)10.1109/QRS54544.2021.00075(654-663)Online publication date: Dec-2021
https://doi.org/10.1109/QRS54544.2021.00075
Iqbal YSindhu MArif MJaved M(2021)Enhancement in Buffer Overflow (BOF) Detection Capability of Cppcheck Static Analysis Tool2021 International Conference on Cyber Warfare and Security (ICCWS)10.1109/ICCWS53234.2021.9703043(112-117)Online publication date: 23-Nov-2021
https://doi.org/10.1109/ICCWS53234.2021.9703043
Jakobs MPauck FPlatzner MWehrheim HWiersema T(2021)Software/Hardware Co-Verification for Custom Instruction Set ProcessorsIEEE Access10.1109/ACCESS.2021.31312139(160559-160579)Online publication date: 2021
https://doi.org/10.1109/ACCESS.2021.3131213
Goel ASakallah K(2020)AVR: Abstractly Verifying ReachabilityTools and Algorithms for the Construction and Analysis of Systems10.1007/978-3-030-45190-5_23(413-422)Online publication date: 25-Apr-2020
https://dl.acm.org/doi/10.1007/978-3-030-45190-5_23
Karna AChen YYu HZhong HZhao J(2018)The role of model checking in software engineeringFrontiers of Computer Science: Selected Publications from Chinese Universities10.1007/s11704-016-6192-012:4(642-668)Online publication date: 1-Aug-2018
https://dl.acm.org/doi/10.1007/s11704-016-6192-0
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.

Figures

Tables

Media

View Table of Conten