Skip to main content

2016 | OriginalPaper | Buchkapitel

Securing a Compiler Transformation

verfasst von : Chaoqiang Deng, Kedar S. Namjoshi

Erschienen in: Static Analysis

Verlag: Springer Berlin Heidelberg

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

search-config
loading …

Abstract

A compiler can be correct and yet be insecure. That is, a compiled program may have the same input-output behavior as the original, and yet leak more information. An example is the commonly applied optimization which removes dead (i.e., useless) stores. It is shown that deciding a posteriori whether a new leak has been introduced as a result of eliminating dead stores is difficult: it is PSPACE-hard for finite-state programs and undecidable in general. In contrast, deciding the correctness of dead store removal is in polynomial time. In response to the hardness result, a sound but approximate polynomial-time algorithm for secure dead store elimination is presented and proved correct. Furthermore, it is shown that for several other compiler transformations, security follows from correctness.

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!

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!

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!

Literatur
1.
Zurück zum Zitat Abadi, M.: Protection in programming-language translations. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 868–883. Springer, Heidelberg (1998)CrossRef Abadi, M.: Protection in programming-language translations. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 868–883. Springer, Heidelberg (1998)CrossRef
2.
Zurück zum Zitat de Amorim, A.A., Collins, N., DeHon, A., Demange, D., Hritcu, C., Pichardie, D., Pierce, B.C., Pollack, R., Tolmach, A.: A verified information-flow architecture. In: Jagannathan, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, San Diego, CA, USA, 20–21 January 2014, pp. 165–178. ACM (2014). http://doi.acm.org/10.1145/2535838.2535839 de Amorim, A.A., Collins, N., DeHon, A., Demange, D., Hritcu, C., Pichardie, D., Pierce, B.C., Pollack, R., Tolmach, A.: A verified information-flow architecture. In: Jagannathan, S., Sewell, P. (eds.) The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, San Diego, CA, USA, 20–21 January 2014, pp. 165–178. ACM (2014). http://​doi.​acm.​org/​10.​1145/​2535838.​2535839
3.
Zurück zum Zitat Bell, D., LaPadula, L.: Secure computer systems: Mathematical foundations, vol. 1-III. Technical report ESD-TR-73-278, The MITRE Corporation (1973) Bell, D., LaPadula, L.: Secure computer systems: Mathematical foundations, vol. 1-III. Technical report ESD-TR-73-278, The MITRE Corporation (1973)
4.
Zurück zum Zitat Ceara, D., Mounier, L., Potet, M.: Taint dependency sequences: a characterization of insecure execution paths based on input-sensitive cause sequences. In: Third International Conference on Software Testing, Verification and Validation, ICST 2010, Paris, France, 7–9 April 2010. Workshops Proceedings, pp. 371–380 (2010). http://dx.doi.org/10.1109/ICSTW.2010.28 Ceara, D., Mounier, L., Potet, M.: Taint dependency sequences: a characterization of insecure execution paths based on input-sensitive cause sequences. In: Third International Conference on Software Testing, Verification and Validation, ICST 2010, Paris, France, 7–9 April 2010. Workshops Proceedings, pp. 371–380 (2010). http://​dx.​doi.​org/​10.​1109/​ICSTW.​2010.​28
5.
Zurück zum Zitat Denning, D.E.: Secure information flow in computer systems. Ph.D. thesis, Purdue University, May 1975 Denning, D.E.: Secure information flow in computer systems. Ph.D. thesis, Purdue University, May 1975
7.
Zurück zum Zitat D’Silva, V., Payer, M., Song, D.X.: The correctness-security gap in compiler optimization. In: 2015 IEEE Symposium on Security and Privacy Workshops, SPW 2015, San Jose, CA, USA, 21–22 May 2015, pp. 73–87. IEEE Computer Society (2015). http://dx.doi.org/10.1109/SPW.2015.33 D’Silva, V., Payer, M., Song, D.X.: The correctness-security gap in compiler optimization. In: 2015 IEEE Symposium on Security and Privacy Workshops, SPW 2015, San Jose, CA, USA, 21–22 May 2015, pp. 73–87. IEEE Computer Society (2015). http://​dx.​doi.​org/​10.​1109/​SPW.​2015.​33
8.
Zurück zum Zitat Fournet, C., Swamy, N., Chen, J., Dagand, P., Strub, P., Livshits, B.: Fully abstract compilation to JavaScript. In: Giacobazzi, R., Cousot, R. (eds.) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, Rome, Italy, 23–25 January 2013, pp. 371–384. ACM (2013). http://doi.acm.org/10.1145/2429069.2429114 Fournet, C., Swamy, N., Chen, J., Dagand, P., Strub, P., Livshits, B.: Fully abstract compilation to JavaScript. In: Giacobazzi, R., Cousot, R. (eds.) The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, Rome, Italy, 23–25 January 2013, pp. 371–384. ACM (2013). http://​doi.​acm.​org/​10.​1145/​2429069.​2429114
9.
Zurück zum Zitat Gondi, K., Bisht, P., Venkatachari, P., Sistla, A.P., Venkatakrishnan, V.N.: SWIPE: eager erasure of sensitive data in large scale systems software. In: Bertino, E., Sandhu, R.S. (eds.) Second ACM Conference on Data and Application Security and Privacy, CODASPY 2012, San Antonio, TX, USA, 7–9 February 2012, pp. 295–306. ACM (2012). http://doi.acm.org/10.1145/2133601.2133638 Gondi, K., Bisht, P., Venkatachari, P., Sistla, A.P., Venkatakrishnan, V.N.: SWIPE: eager erasure of sensitive data in large scale systems software. In: Bertino, E., Sandhu, R.S. (eds.) Second ACM Conference on Data and Application Security and Privacy, CODASPY 2012, San Antonio, TX, USA, 7–9 February 2012, pp. 295–306. ACM (2012). http://​doi.​acm.​org/​10.​1145/​2133601.​2133638
11.
Zurück zum Zitat Namjoshi, K.S., Zuck, L.D.: Witnessing program transformations. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 304–323. Springer, Heidelberg (2013)CrossRef Namjoshi, K.S., Zuck, L.D.: Witnessing program transformations. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis. LNCS, vol. 7935, pp. 304–323. Springer, Heidelberg (2013)CrossRef
12.
Zurück zum Zitat Necula, G.: Translation validation of an optimizing compiler. In: Proceedings of the ACM SIGPLAN Conference on Principles of Programming Languages Design and Implementation (PLDI 2000), pp. 83–95 (2000) Necula, G.: Translation validation of an optimizing compiler. In: Proceedings of the ACM SIGPLAN Conference on Principles of Programming Languages Design and Implementation (PLDI 2000), pp. 83–95 (2000)
13.
Zurück zum Zitat Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)MATH Papadimitriou, C.H.: Computational Complexity. Addison-Wesley, Reading (1994)MATH
15.
Zurück zum Zitat Pnueli, A., Shtrichman, O., Siegel, M.: The code validation tool (CVT)- automatic verification of a compilation process. Softw. Tools Technol. Transf. 2(2), 192–201 (1998)CrossRefMATH Pnueli, A., Shtrichman, O., Siegel, M.: The code validation tool (CVT)- automatic verification of a compilation process. Softw. Tools Technol. Transf. 2(2), 192–201 (1998)CrossRefMATH
18.
Zurück zum Zitat Zuck, L.D., Pnueli, A., Goldberg, B.: VOC: a methodology for the translation validation of optimizing compilers. J. UCS 9(3), 223–247 (2003) Zuck, L.D., Pnueli, A., Goldberg, B.: VOC: a methodology for the translation validation of optimizing compilers. J. UCS 9(3), 223–247 (2003)
Metadaten
Titel
Securing a Compiler Transformation
verfasst von
Chaoqiang Deng
Kedar S. Namjoshi
Copyright-Jahr
2016
Verlag
Springer Berlin Heidelberg
DOI
https://doi.org/10.1007/978-3-662-53413-7_9

Premium Partner