Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Bücher
Zeitschriften
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
ATZ-Fachkongress

Chassis.tech plus 2024


4 Kongresse in einer Veranstaltung

Treffen Sie in München die Fachleute von Chassis, Lenkung, Bremsen sowie Reifen/Räder.
Erweiterte Suche
Anmelden
nach oben
Erschienen in:
Probabilistic Horn Clause Verification Kapitel lesen Erstes Kapitel lesen

2017 | OriginalPaper | Buchkapitel

A Context-Sensitive Memory Model for Verification of C/C++ Programs

verfasst von : Arie Gurfinkel, Jorge A. Navas

Erschienen in: Static Analysis

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config
loading …

Abstract

Verification of low-level C/C++ requires a precise memory model that supports type unions, pointer arithmetic, and casts. We present a new memory model that splits memory into a finite set of disjoint regions based on a pointer analysis. The main contribution is a field-, array- and context-sensitive pointer analysis tailored to verification. We have implemented our memory model for the LLVM bitcode and used it on a C++ case study and on SV-COMP benchmarks. Our results suggests that our model can reduce verification time by producing a finer-grained partitioning in presence of function calls.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Jetzt informieren
Vorheriges Kapitel Loop Invariants from Counterexamples
Nächstes Kapitel Effect Summaries for Thread-Modular Analysis
Fußnoten
1
Logic-based verifiers require to generate verification conditions in a side-effect free form so that they can be solved by SMT solvers. In this paper, we focus on how to provide precise points-to information to produce a sound translation to such a form. The syntax and semantics of the language and construction of VCs are beyond the scope of this paper. We refer readers to e.g., [11, 18] and their references for details.
 
3
For simplicity, we choose not to modify the definition of a concrete object to include its size.
 
4
For simplicity, we assume in Fig. 8 all cells have zero offsets.
 
5
In fact, we only need to consider cells that can be modified. Our implementation considers this optimization.
 
6
The pointer analysis is available from https://​github.​com/​seahorn/​sea-dsa.
 
7
Accessed https://​github.​com/​sosy-lab/​sv-benchmarks with sha 879e141f11348e49591738d3e11793b36546a2d5.
 
8
CASS is owned NASA and is not publicly available. It is 13,460 LOC (excluding blanks/comments).
 
9
How to instrument effectively a program for proving memory safety is beyond the scope of this paper. SeaHorn provides several LLVM bitcode transformations that insert assertions such that the transformed bitcode is free of buffer overflows if all assertions hold. For our experiments, we used one that stores non-deterministically the offset and size of a pointer. This instrumentation is simple and relies on the solver to resolve the non-determinism to make sure all pointers are properly checked.
 
11
Frama-C provides another plugin called VC for C programs, complementary to Jessie, with three different memory models: Hoare (unsound with pointers), Typed based on Burstall’s model that does not support casts, and Byte which is a byte-level memory model.
 
Literatur
1.
2.
3.
Andersen, L.O.: Program analysis and specialization for the C Programming language. Technical report (1994)
4.
5.
Burstall, R.M.: Some techniques for proving correctness of programs which alter data structures. In: Machine Intelligence (1972)
6.
Chatterjee, S., Lahiri, S.K., Qadeer, S., Rakamarić, Z.: A reachability predicate for analyzing low-level software. In: Grumberg, O., Huth, M. (eds.) TACAS 2007. LNCS, vol. 4424, pp. 19–33. Springer, Heidelberg (2007). doi:10.​1007/​978-3-540-71209-1_​4 CrossRef
7.
8.
Cohen, E., Moskal, M., Tobies, S., Schulte, W.: A precise yet efficient memory model for C. Electr. Notes Theor. Comput. Sci. 254, 85–103 (2009)CrossRef
9.
Condit, J., Hackett, B., Lahiri, S.K., Qadeer, S.: Unifying type checking and property checking for low-level code. In: POPL, pp. 302–314 (2009)
10.
Cordeiro, L., Fischer, B., Marques-Silva, J.: SMT-based bounded model checking for embedded ANSI-C software. IEEE Trans. Softw. Eng. 38(4), 957–974 (2012)CrossRef
11.
Gurfinkel, A., Kahsai, T., Komuravelli, A., Navas, J.A.: The SeaHorn verification framework. In: Kroening, D., Păsăreanu, C.S. (eds.) CAV 2015. LNCS, vol. 9206, pp. 343–361. Springer, Cham (2015). doi:10.​1007/​978-3-319-21690-4_​20 CrossRef
12.
Hubert, T., Marche, C.: Separation analysis for deductive verification. In: HAV (2007)
13.
Komuravelli, A., Gurfinkel, A., Chaki, S., Clarke, E.M.: Automatic abstraction in SMT-based unbounded software model checking. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 846–862. Springer, Heidelberg (2013). doi:10.​1007/​978-3-642-39799-8_​59 CrossRef
14.
Lattner, C., Adve, V.S.: LLVM: a compilation framework for lifelong program analysis & transformation. In: CGO, pp. 75–88 (2004)
15.
Lattner, C., Adve, V.S.: Automatic pool allocation: improving performance by controlling data structure layout in the heap. In: PLDI, pp. 129–142 (2005)
16.
Miné, A.: Field-sensitive value analysis of embedded C programs with union types and pointer arithmetics. In: LCTES, pp. 54–63 (2006)
17.
Moy, Y.: Automatic modular static safety checking for C Programs. Ph.D. thesis, Université Paris-Sud (2009)
18.
Rakamarić, Z., Emmi, M.: SMACK: decoupling source language details from verifier implementations. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 106–113. Springer, Cham (2014). doi:10.​1007/​978-3-319-08867-9_​7
19.
20.
21.
22.
Metadaten
Titel
A Context-Sensitive Memory Model for Verification of C/C++ Programs
verfasst von
Arie Gurfinkel
Jorge A. Navas
Copyright-Jahr
2017
Buch
Static Analysis

Print ISBN: 978-3-319-66705-8

Electronic ISBN: 978-3-319-66706-5

Copyright-Jahr: 2017

DOI
https://doi.org/10.1007/978-3-319-66706-5_8

Premium Partner

    Bildnachweise