Modeling and analyzing the interaction of C and C++ strings

Gogul Balakrishnan, Naoto Maeda, Sriram Sankaranarayanan, Franjo Ivančić, Aarti Gupta, Rakesh Pothengil

Research output: Chapter in Book/Report/Conference proceedingConference contribution

1 Scopus citations

Abstract

Strings are commonly used in a large variety of software. And yet, they are a common source of bugs involving invalid memory accesses arising due to the misuse of the string manipulation API. Such bugs are often remotely exploitable, leading to severe consequences. Therefore, static detection of invalid memory accesses due to string operations has received much attention, especially for C programs that use the standard C library functions. More recently, software is increasingly being developed in object-oriented languages such as C++ and Java. However, the need to interact with legacy C code and C-based system-level APIs often necessitates the use of a mixed programming paradigm that combines features of high-level object-oriented constructs with calls to standard C library functions. While such programs are commonplace, there has been little research on static analysis of such programs. In this paper, we present memory models for C++ programs that are heap-aware, with an emphasis on modeling dynamically allocated memory, use of null-terminated string buffers, C++ Standard Template Library (STL) classes, and the interactions among these features. We use standard verification techinques such as abstract interpretation and model checking to verify properties over these models to find potential bugs. Our tool can find several previously unknown bugs in open-source projects. These bugs are primarily due to the subtle interactions of the intricate C++ programming model with legacy C string API.

Original languageEnglish (US)
Title of host publicationFormal Verification of Object-Oriented Software - International Conference, FoVeOOS 2011, Revised Selected Papers
Pages67-85
Number of pages19
DOIs
StatePublished - Aug 15 2012
Externally publishedYes
EventInternational Conference on Formal Verification of Object-Oriented Software, FoVeOOS 2011 - Turin, Italy
Duration: Oct 5 2011Oct 7 2011

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume7421 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Other

OtherInternational Conference on Formal Verification of Object-Oriented Software, FoVeOOS 2011
CountryItaly
CityTurin
Period10/5/1110/7/11

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • Computer Science(all)

Fingerprint Dive into the research topics of 'Modeling and analyzing the interaction of C and C++ strings'. Together they form a unique fingerprint.

  • Cite this

    Balakrishnan, G., Maeda, N., Sankaranarayanan, S., Ivančić, F., Gupta, A., & Pothengil, R. (2012). Modeling and analyzing the interaction of C and C++ strings. In Formal Verification of Object-Oriented Software - International Conference, FoVeOOS 2011, Revised Selected Papers (pp. 67-85). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 7421 LNCS). https://doi.org/10.1007/978-3-642-31762-0_6