nach oben

Erschienen in:

2020 | OriginalPaper | Buchkapitel

Witnessing Secure Compilation

verfasst von : Kedar S. Namjoshi, Lucas M. Tabajara

Erschienen in: Verification, Model Checking, and Abstract Interpretation

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

Compiler optimizations may break or weaken the security properties of a source program. This work develops a translation validation methodology for secure compilation. A security property is expressed as an automaton operating over a bundle of program traces. A refinement proof scheme derived from a property automaton guarantees that the associated security property is preserved by a program transformation. This generalizes known refinement methods that apply only to specific security properties. In practice, the refinement relations (“security witnesses”) are generated during compilation and validated independently with a refinement checker. This process is illustrated for common optimizations. Crucially, it is not necessary to formally verify the compiler implementation, which is infeasible for production compilers.

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

Nächstes Kapitel : Backward Context-Sensitive Flow Reconstruction of Taint Analysis Results

Abadi, M.: Protection in programming-language translations. In: Vitek, J., Jensen, C.D. (eds.) Secure Internet Programming. LNCS, vol. 1603, pp. 19–34. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48749-2_2CrossRef

Abadi, M., Lamport, L.: The existence of refinement mappings. In: LICS 1988, pp. 165–175 (1988). https://doi.org/10.1109/LICS.1988.5115

de Amorim, A.A., et al.: A verified information-flow architecture. In: POPL 2014, pp. 165–178 (2014). https://doi.org/10.1145/2535838.2535839

Barthe, G., Grégoire, B., Laporte, V.: Secure compilation of side-channel countermeasures: the case of cryptographic “constant-time”. In: CSF 2018, pp. 328–343 (2018). https://doi.org/10.1109/CSF.2018.00031

Browne, M.C., Clarke, E.M., Grumberg, O.: Characterizing finite Kripke structures in propositional temporal logic. Theor. Comput. Sci. 59, 115–131 (1988). https://doi.org/10.1016/0304-3975(88)90098-9MathSciNetCrossRefMATH

Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., Sánchez, C.: Temporal logics for hyperproperties. In: Abadi, M., Kremer, S. (eds.) POST 2014. LNCS, vol. 8414, pp. 265–284. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-642-54792-8_15CrossRef

Clarkson, M.R., Schneider, F.B.: Hyperproperties. In: CSF 2008, pp. 51–65 (2008). https://doi.org/10.1109/CSF.2008.7

Deng, C., Namjoshi, K.S.: Securing a compiler transformation. In: Rival, X. (ed.) SAS 2016. LNCS, vol. 9837, pp. 170–188. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-53413-7_9CrossRef

Devriese, D., Patrignani, M., Piessens, F.: Fully-abstract compilation by approximate back-translation. In: POPL 2016, pp. 164–177 (2016). https://doi.org/10.1145/2837614.2837618

10.

D’Silva, V., Payer, M., Song, D.X.: The correctness-security gap in compiler optimization. In: SPW 2015, pp. 73–87 (2015). https://doi.org/10.1109/SPW.2015.33

11.

Fournet, C., Guernic, G.L., Rezk, T.: A security-preserving compiler for distributed programs: from information-flow policies to cryptographic mechanisms. In: CCS 2009, pp. 432–441 (2009). https://doi.org/10.1145/1653662.1653715

12.

Howard, M.: When scrubbing secrets in memory doesn’t work (2002). http://archive.cert.uni-stuttgart.de/bugtraq/2002/11/msg00046.html. Also https://cwe.mitre.org/data/definitions/14.html

13.

Le, V., Afshari, M., Su, Z.: Compiler validation via equivalence modulo inputs. In: PLDI 2014, pp. 216–226 (2014). https://doi.org/10.1145/2594291.2594334

14.

Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: POPL 2006, pp. 42–54 (2006). https://doi.org/10.1145/1111037.1111042

15.

Manna, Z., Pnueli, A.: Specification and verification of concurrent programs by \({\forall }\)-automata. In: Banieqbal, B., Barringer, H., Pnueli, A. (eds.) Temporal Logic in Specification. LNCS, vol. 398, pp. 124–164. Springer, Heidelberg (1989). https://doi.org/10.1007/3-540-51803-7_24CrossRef

16.

Marinov, D.: Credible compilation. Ph.D. thesis, Massachusetts Institute of Technology (2000)

17.

Murray, T.C., Sison, R., Engelhardt, K.: COVERN: a logic for compositional verification of information flow control. In: EuroS&P 2018, pp. 16–30 (2018). https://doi.org/10.1109/EuroSP.2018.00010

18.

Namjoshi, K.S.: A simple characterization of stuttering bisimulation. In: Ramesh, S., Sivakumar, G. (eds.) FSTTCS 1997. LNCS, vol. 1346, pp. 284–296. Springer, Heidelberg (1997). https://doi.org/10.1007/BFb0058037CrossRef

19.

Namjoshi, K.S.: Witnessing an SSA transformation. In: VeriSure Workshop, CAV (2014). https://kedar-namjoshi.github.io/papers/Namjoshi-VeriSure-CAV-2014.pdf

20.

Namjoshi, K.S., Tabajara, L.M.: Witnessing Secure Compilation (2019). https://arxiv.org/abs/1911.05866

21.

Namjoshi, K.S., Zuck, L.D.: Witnessing program transformations. In: Logozzo, F., Fähndrich, M. (eds.) SAS 2013. LNCS, vol. 7935, pp. 304–323. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-38856-9_17CrossRef

22.

Necula, G.: Translation validation of an optimizing compiler. In: (PLDI) 2000, pp. 83–95 (2000)

23.

Patrignani, M., Ahmed, A., Clarke, D.: Formal approaches to secure compilation: a survey of fully abstract compilation and related work. ACM Comput. Surv. 51(6), 125:1–125:36 (2019). https://doi.org/10.1145/3280984CrossRef

24.

Patrignani, M., Garg, D.: Secure compilation and hyperproperty preservation. In: CSF 2017, pp. 392–404 (2017). https://doi.org/10.1109/CSF.2017.13

25.

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)CrossRef

26.

Rinard, M.: Credible compilation. Technical report. In: Proceedings of CC 2001: International Conference on Compiler Construction (1999)

27.

Terauchi, T., Aiken, A.: Secure information flow as a safety problem. In: Hankin, C., Siveroni, I. (eds.) SAS 2005. LNCS, vol. 3672, pp. 352–367. Springer, Heidelberg (2005). https://doi.org/10.1007/11547662_24CrossRef

28.

Yang, X., Chen, Y., Eide, E., Regehr, J.: Finding and understanding bugs in C compilers. In: PLDI 2011, pp. 283–294 (2011). https://doi.org/10.1145/1993498.1993532

29.

Yang, Z., Johannesmeyer, B., Olesen, A.T., Lerner, S., Levchenko, K.: Dead store elimination (still) considered harmful. In: USENIX Security 2017, pp. 1025–1040 (2017). https://www.usenix.org/conference/usenixsecurity17/technical-sessions/presentation/yang

30.

Zhao, J., Nagarakatte, S., Martin, M.M.K., Zdancewic, S.: Formal verification of SSA-based optimizations for LLVM. In: PLDI 2013, pp. 175–186 (2013). https://doi.org/10.1145/2491956.2462164

31.

Zuck, L.D., Pnueli, A., Goldberg, B.: VOC: a methodology for the translation validation of optimizing compilers. J. UCS 9(3), 223–247 (2003)

Titel: Witnessing Secure Compilation
verfasst von: Kedar S. Namjoshi
Lucas M. Tabajara
Verlag: Springer International Publishing
Buch: Verification, Model Checking, and Abstract Interpretation
Print ISBN: 978-3-030-39321-2

Electronic ISBN: 978-3-030-39322-9

Copyright-Jahr: 2020
DOI: https://doi.org/10.1007/978-3-030-39322-9_1

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

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

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"