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:
Reasoning about Separation Using Abstraction and Reification Kapitel lesen Erstes Kapitel lesen

2015 | OriginalPaper | Buchkapitel

Speed Up Configurable Certificate Validation by Certificate Reduction and Partitioning

verfasst von : Marie-Christine Jakobs

Erschienen in: Software Engineering and Formal Methods

Verlag: Springer International Publishing

Einloggen

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

search-config
loading …

Abstract

Before execution, users should formally validate the correctness of software received from untrusted providers. To accelerate this validation, in the proof carrying code (PCC) paradigm the provider delivers the software together with a certificate, a formal proof of the software’s correctness. Thus, the user only checks if the attached certificate shows correctness of the delivered software.
Recently, we introduced configurable program certification, a generic, PCC based framework supporting various software analyses and safety properties. Evaluation of our framework revealed that validation suffers from certificate reading. In this paper, we present two orthogonal approaches which improve certificate validation, both reducing the impact of certificate reading. The first approach reduces the certificate size, storing information only if it cannot easily be recomputed. The second approach partitions the certificate into independently checkable parts. The trick is to read parts of the certificate while already checking read parts. Our experiments show that validation highly benefits from our improvements.

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 On the Testability of Properties Patterns
Nächstes Kapitel Formal Analysis of Proactive, Distributed Routing
Fußnoten
1
Note, that the consumer adopts the CPA’s definition of abstract domain and coverage check but uses its own, trusted or even verified implementation.
 
2
Our implementation in CPAchecker [8] supports programs written in C.
 
3
More formally, we have one transfer function per program, i.e., a function \(\rightsquigarrow _P\). Following [7] we omit P here, and assume it to be clear from the context, both as parameter to \(\rightsquigarrow \) and as input to the algorithms.
 
5
Ubuntu was executed in the virtual machine Virtual Box version 4.3.8 r92456 running on a 64 bit Windows 7 Professional machine with 6 GB RAM.
 
Literatur
1.
Albert, E., Arenas, P., Puebla, G., Hermenegildo, M.V.: Reduced certificates for abstraction-carrying code. In: Etalle, S., Truszczyński, M. (eds.) ICLP 2006. LNCS, vol. 4079, pp. 163–178. Springer, Heidelberg (2006) CrossRef
2.
Amme, W., Möller, M.A., Adler, P.: Data flow analysis as a general concept for the transport of verifiable program annotations. Theor. Comput. Sci. 176(3), 97–108 (2007). COCV 2006
3.
Andreev, K., Räcke, H.: Balanced graph partitioning. In: SPAA 2004, pp. 120–124. ACM (2004)
4.
Besson, F., Jensen, T., Pichardie, D.: Proof-carrying code from certified abstract interpretation and fixpoint compression. Theor. Comput. Sci. 364(3), 273–291 (2006). applied SemanticsCrossRefMATHMathSciNet
5.
Besson, F., Jensen, T., Turpin, T.: Small witnesses for abstract interpretation-based proofs. In: De Nicola, R. (ed.) ESOP 2007 (ETAPS). LNCS, vol. 4421, pp. 268–283. Springer, Heidelberg (2007) CrossRef
6.
Beyer, D.: Status report on software verification. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014 (ETAPS). LNCS, vol. 8413, pp. 373–388. Springer, Heidelberg (2014) CrossRef
7.
Beyer, D., Henzinger, T.A., Théoduloz, G.: Configurable software verification: concretizing the convergence of model checking and program analysis. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 504–518. Springer, Heidelberg (2007) CrossRef
8.
Beyer, D., Keremoglu, M.E.: CPAchecker: A tool for configurable software verification. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 184–190. Springer, Heidelberg (2011) CrossRef
9.
Beyer, D., Löwe, S., Novikov, E., Stahlbauer, A., Wendler, P.: Precision reuse for efficient regression verification. In: ESEC/FSE 2013, pp. 389–399. ACM (2013)
10.
Brückner, I., Dräger, K., Finkbeiner, B., Wehrheim, H.: Slicing abstractions. In: Arbab, F., Sirjani, M. (eds.) FSEN 2007. LNCS, vol. 4767, pp. 17–32. Springer, Heidelberg (2007) CrossRef
11.
Dräger, K., Kupriyanov, A., Finkbeiner, B., Wehrheim, H.: SLAB: a certifying model checker for infinite-state concurrent systems. In: Esparza, J., Majumdar, R. (eds.) TACAS 2010 (ETAPS). LNCS, vol. 6015, pp. 271–274. Springer, Heidelberg (2010) CrossRef
12.
Jakobs, M.C., Wehrheim, H.: Certification for configurable program analysis. In: SPIN 2014, pp. 30–39. ACM (2014)
13.
Necula, G., Lee, P.: Efficient representation and validation of proofs. In: LICS 1998, June 1998, pp. 93–104 (1998)
14.
Necula, G.C.: Proof-carrying code. In: POPL 1997, pp. 106–119. ACM (1997)
15.
Necula, G.C., Rahul, S.P.: Oracle-based checking of untrusted software. In: POPL 2001, pp. 142–154. ACM (2001)
16.
Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, Heidelberg (2004)
17.
Rose, E.: Lightweight bytecode verification. J. Autom. Reasoning 31(3–4), 303–334 (2003)CrossRefMATH
18.
Seo, S., Yang, H., Yi, K., Han, T.: Goal-directed weakening of abstract interpretation results. TOPLAS 29(6), 1–39 (2007)CrossRef
19.
Taleghani, A., Atlee, J.M.: Search-carrying code. In: ASE 2010, pp. 367–376. ACM (2010)
Metadaten
Titel
Speed Up Configurable Certificate Validation by Certificate Reduction and Partitioning
verfasst von
Marie-Christine Jakobs
Copyright-Jahr
2015
Buch
Software Engineering and Formal Methods

Print ISBN: 978-3-319-22968-3

Electronic ISBN: 978-3-319-22969-0

Copyright-Jahr: 2015

DOI
https://doi.org/10.1007/978-3-319-22969-0_12

Premium Partner

    Bildnachweise