Skip to main content
SpringerLink
Log in

Witnessing Secure Compilation

  • Conference paper
  • First Online:
Verification, Model Checking, and Abstract Interpretation (VMCAI 2020)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11990))

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 69.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 89.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

References

  1. 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_2

    Chapter  Google Scholar 

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

  3. 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

  4. 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

  5. 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-9

    Article  MathSciNet  MATH  Google Scholar 

  6. 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_15

    Chapter  Google Scholar 

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

  8. 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_9

    Chapter  Google Scholar 

  9. 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_24

    Chapter  Google Scholar 

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

    Google Scholar 

  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/BFb0058037

    Chapter  Google Scholar 

  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_17

    Chapter  Google Scholar 

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

    Google Scholar 

  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/3280984

    Article  Google Scholar 

  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)

    Article  Google Scholar 

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

    Google Scholar 

  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_24

    Chapter  Google Scholar 

  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)

    Google Scholar 

Download references

Acknowledgments

The authors were supported, in part, by NSF grant CCF-1563393 from the National Science Foundation. Any opinions, findings, and conclusions or recommendations expressed are those of the author(s) and do not necessarily reflect the views of the National Science Foundation. Kedar Namjoshi would like to acknowledge fruitful discussions during a Dagstuhl Seminar on Secure Compilation organized in May 2018.

Author information

Authors and Affiliations

  1. Nokia Bell Labs, Murray Hill, NJ, USA

    Kedar S. Namjoshi

  2. Rice University, Houston, TX, USA

    Lucas M. Tabajara

Authors
  1. Kedar S. Namjoshi
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Lucas M. Tabajara
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Kedar S. Namjoshi .

Editor information

Editors and Affiliations

  1. Ludwig-Maximilians-Universität München, Munich, Germany

    Dirk Beyer

  2. Max Planck Institute for Software Systems, Kaiserslautern, Rheinland-Pfalz, Germany

    Damien Zufferey

Rights and permissions

Reprints and permissions

Copyright information

© 2020 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Namjoshi, K.S., Tabajara, L.M. (2020). Witnessing Secure Compilation. In: Beyer, D., Zufferey, D. (eds) Verification, Model Checking, and Abstract Interpretation. VMCAI 2020. Lecture Notes in Computer Science(), vol 11990. Springer, Cham. https://doi.org/10.1007/978-3-030-39322-9_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-39322-9_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-39321-2

  • Online ISBN: 978-3-030-39322-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation