Top

Published in:

2020 | OriginalPaper | Chapter

Witnessing Secure Compilation

Authors : Kedar S. Namjoshi, Lucas M. Tabajara

Published in: Verification, Model Checking, and Abstract Interpretation

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

inform now

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!

inform now

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!

inform now

next chapter : 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)

Title: Witnessing Secure Compilation
Authors: Kedar S. Namjoshi
Lucas M. Tabajara
Publisher: Springer International Publishing
Book: Verification, Model Checking, and Abstract Interpretation
Print ISBN: 978-3-030-39321-2

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

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

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner