CSSV: Towards a realistic tool for statically detecting all buffer overflows in C. Erroneous string manipulations are a major source of software defects in C programs yielding vulnerabilities which are exploited by software viruses. We present C String Static Verifyer (CSSV), a tool that statically uncovers all string manipulation errors. Being a conservative tool, it reports all such errors at the expense of sometimes generating false alarms. Fortunately, only a small number of false alarms are reported, thereby proving that statically reducing software vulnerability is achievable. CSSV handles large programs by analyzing each procedure separately. To this end procedure contracts are allowed which are verified by the tool.We implemented a CSSV prototype and used it to verify the absence of errors in real code from EADS Airbus. When applied to another commonly used string intensive application, CSSV uncovered real bugs with very few false alarms.

This software is also peer reviewed by journal TOMS.

References in zbMATH (referenced in 19 articles )

Showing results 1 to 19 of 19.
Sorted by year (citations)

  1. Kroening, Daniel; Sharygina, Natasha; Tonetta, Stefano; Tsitovich, Aliaksei; Wintersteiger, Christoph M.: Loop summarization using state and transition invariants (2013)
  2. Logozzo, Francesco; Fähndrich, Manuel: Pentagons: a weakly relational abstract domain for the efficient validation of array accesses (2010)
  3. McCloskey, Bill; Reps, Thomas; Sagiv, Mooly: Statically inferring complex heap, array, and numeric invariants (2010)
  4. Gulwani, Sumit; Lev-Ami, Tal; Sagiv, Mooly: A combination framework for tracking partition sizes (2009)
  5. Gulwani, Sumit; Mehra, Krishna K.; Chilimbi, Trishul: SPEED: precise and efficient static estimation of program computational complexity (2009)
  6. Yu, Fang; Bultan, Tevfik; Ibarra, Oscar H.: Symbolic string verification: Combining string analysis and size analysis (2009)
  7. Allamigeon, Xavier; Hymans, Charles: Static analysis by abstract interpretation: Application to the detection of heap overflows. (2008) ioport
  8. Hao, Dan; Zhang, Lu; Pan, Ying; Mei, Hong; Sun, Jiasu: On similarity-awareness in testing-based fault localization (2008) ioport
  9. Ivančić, Franjo; Yang, Zijiang; Ganai, Malay K.; Gupta, Aarti; Ashar, Pranav: Efficient SAT-based bounded model checking for software verification (2008)
  10. Simon, Axel: Value-range analysis of C programs. Towards proving the absence of buffer overflow vulnerabilities (2008)
  11. Sankaranarayanan, Sriram; Ivančić, Franjo; Gupta, Aarti: Program analysis using symbolic ranges (2007)
  12. Simon, Axel; King, Andy: Taming the wrapping of integer arithmetic (2007)
  13. Allamigeon, Xavier; Godard, Wenceslas; Hymans, Charles: Static analysis of string manipulations in critical embedded C programs (2006)
  14. Sankaranarayanan, Sriram; Ivančić, Franjo; Shlyakhter, Ilya; Gupta, Aarti: Static analysis in disjunctive numerical domains (2006)
  15. Sidiroglou, Stelios; Keromytis, Angelos D.: Execution transactions for defending against software failures: use and evaluation (2006) ioport
  16. Sidiroglou, Stelios; Keromytis, Angelos D.: Execution transactions for defending against software failures: use and evaluation (2006) ioport
  17. Rival, Xavier: Understanding the origin of alarms in Astrée (2005)
  18. Rival, Xavier: Abstract dependences for alarm diagnosis (2005)
  19. Balakrishnan, Gogul; Reps, Thomas: Analyzing memory accesses in x86 executables (2004)