Skip to main content
SpringerLink
Log in

Fully Abstract and Robust Compilation

And How to Reconcile the Two, Abstractly

  • Conference paper
  • First Online:
Programming Languages and Systems (APLAS 2021)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 13008))

Included in the following conference series:

Abstract

The most prominent formal criterion for secure compilation is full abstraction, the preservation and reflection of contextual equivalence. Recent work introduced robust compilation, defined as the preservation of robust satisfaction of hyperproperties, i.e., their satisfaction against arbitrary attackers. In this paper, we initially set out to compare these two approaches to secure compilation. To that end, we provide an exact description of the hyperproperties that are robustly satisfied by programs compiled with a fully abstract compiler, and show that they can be meaningless or trivial. We then propose a novel criterion for secure compilation formulated in the framework of Mathematical Operational Semantics (MOS), guaranteeing both full abstraction and the preservation of robust satisfaction of hyperproperties in a more sensible manner.

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 64.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 84.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

Similar content being viewed by others

Notes

  1. 1.

    is a shorthand for .

  2. 2.

    \(\varSigma ^{*}\) is the free monad over \(\varSigma \) and \(B^{\infty }\) is the co-free comonad over B [22, Ch. 5].

  3. 3.

    It is possible to eliminate the hypothesis of determinacy when B is an endofunctor over categories richer that Set, e.g., Rel the category of sets and relations.

References

  1. Abadi, M.: Protection in programming-language translations. In: Secure Internet Programming, Security Issues for Mobile and Distributed Objects, pp. 19–34 (1999)

    Google Scholar 

  2. Abate, C., et al.: When good components go bad: formally secure compilation despite dynamic compromise. In: Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, pp. 1351–1368 (2018)

    Google Scholar 

  3. Abate, C., et al.: Trace-relating compiler correctness and secure compilation. In: ESOP 2020. LNCS, vol. 12075, pp. 1–28. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-44914-8_1

    Chapter  Google Scholar 

  4. Abate, C., Blanco, R., Garg, D., Hritcu, C., Patrignani, M., Thibault, J.: Journey beyond full abstraction: exploring robust property preservation for secure compilation. In: 2019 IEEE 32nd Computer Security Foundations Symposium (CSF), pp. 256–25615. IEEE (2019)

    Google Scholar 

  5. Abate, C., Busi, M., Tsampas, S.: Fully abstract and robust compilation and how to reconcile the two, abstractly (2021)

    Google Scholar 

  6. Abou-Saleh, F., Pattinson, D.: Towards effects in mathematical operational semantics. Electr. Notes Theor. Comput. Sci. 276, 81–104 (2011)

    Google Scholar 

  7. Aceto, L., Fokkink, W., Verhoef, C.: Structural operational semantics. In: Handbook of Process Algebra, pp. 197–292. Elsevier (2001)

    Google Scholar 

  8. Ahmed, A., Blume, M.: Typed closure conversion preserves observational equivalence. In: Hook, J., Thiemann, P. (eds.) Proceeding of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP 2008, Victoria, BC, Canada, 20–28 September 2008, pp. 157–168. ACM (2008)

    Google Scholar 

  9. Ahmed, A., Blume, M.: An equivalence-preserving CPS translation via multi-language semantics. In: Chakravarty, M.M.T., Hu, Z., Danvy, O. (eds.) Proceeding of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP 2011, Tokyo, Japan, 19–21 September 2011, pp. 431–444. ACM (2011). https://doi.org/10.1145/2034773.2034830

  10. Barthe, G., et al.: Formal verification of a constant-time preserving C compiler. Proc. ACM Program. Lang. 4(Popl), 1–30 (2019)

    Google Scholar 

  11. Barthe, G., Grégoire, B., Laporte, V.: Secure compilation of side-channel countermeasures: the case of cryptographic “constant-time”. In: 2018 IEEE 31st Computer Security Foundations Symposium (CSF), pp. 328–343. IEEE (2018)

    Google Scholar 

  12. Besson, F., Blazy, S., Wilke, P.: A verified compcert front-end for a memory model supporting pointer arithmetic and uninitialised data. J. Autom. Reason. 62(4), 433–480 (2019)

    Google Scholar 

  13. Bowman, W.J., Ahmed, A.: Noninterference for free. ACM SIGPLAN Not. 50(9), 101–113 (2015)

    Google Scholar 

  14. Busi, M., et al.: Provably secure isolation for interruptible enclaved execution on small microprocessors. In: 33rd IEEE Computer Security Foundations Symposium (CSF 2020) (2020)

    Google Scholar 

  15. Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157–1210 (2010)

    Article  Google Scholar 

  16. Devriese, D., Patrignani, M., Piessens, F.: Fully-abstract compilation by approximate back-translation. In: Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 164–177 (2016)

    Google Scholar 

  17. 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 (2015)

    Google Scholar 

  18. Durumeric, Z., et al.: The matter of heartbleed. In: Proceedings of the 2014 Conference on Internet Measurement Conference, pp. 475–488 (2014)

    Google Scholar 

  19. El-Korashy, A., Tsampas, S., Patrignani, M., Devriese, D., Garg, D., Piessens, F.: CapablePtrs: securely compiling partial programs using the pointers-as-capabilities principle. CoRR abs/2005.05944 (2020)

    Google Scholar 

  20. Engelfriet, J.: Determinacy - (observation equivalence = trace equivalence). Theor. Comput. Sci. 36(1), 21–25 (1985)

    Article  MathSciNet  Google Scholar 

  21. Gorla, D., Nestmann, U.: Full abstraction for expressiveness: history, myths and facts. Math. Struct. Comput. Sci. 26(4), 639–654 (2016)

    Article  MathSciNet  Google Scholar 

  22. Jacobs, B.: Introduction to Coalgebra: Towards Mathematics of States and Observation, Cambridge Tracts in Theoretical Computer Science, vol. 59. Cambridge University Press (2016). ISBN 9781316823187

    Google Scholar 

  23. Jacobs, K., Timany, A., Devriese, D.: Fully abstract from static to gradual. Proc. ACM Program. Lang. 5(Popl), 1–30 (2021)

    Google Scholar 

  24. Klin, B.: Bialgebras for structural operational semantics: an introduction. Theoret. Comput. Sci. 412(38), 5043–5069 (2011)

    Article  MathSciNet  Google Scholar 

  25. Klin, B., Sassone, V.: Structural operational semantics for stochastic process calculi. In: Amadio, R. (ed.) FoSSaCS 2008. LNCS, vol. 4962, pp. 428–442. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78499-9_30

    Chapter  Google Scholar 

  26. Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: Morrisett, J.G., Jones, S.L.P. (eds.) Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, 11–13 January 2006, pp. 42–54. ACM (2006)

    Google Scholar 

  27. Melton, A., Schmidt, D.A., Strecker, G.E.: Galois connections and computer science applications. In: Pitt, D., Abramsky, S., Poigné, A., Rydeheard, D. (eds.) Category Theory and Computer Programming. LNCS, vol. 240, pp. 299–312. Springer, Heidelberg (1986). https://doi.org/10.1007/3-540-17162-2_130

    Chapter  Google Scholar 

  28. Mitchell, J.C.: On abstraction and the expressive power of programming languages. Sci. Comput. Program. 21(2), 141–163 (1993)

    Article  MathSciNet  Google Scholar 

  29. Morris, F.L.: Advice on structuring compilers and proving them correct. In: Proceedings of the 1st Annual ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages, pp. 144–152 (1973)

    Google Scholar 

  30. Murray, T., Sison, R., Pierzchalski, E., Rizkallah, C.: Compositional verification and refinement of concurrent value-dependent noninterference. In: 2016 IEEE 29th Computer Security Foundations Symposium (CSF), pp. 417–431. IEEE (2016)

    Google Scholar 

  31. Nielson, H.R., Nielson, F.: Semantics with Applications: An Appetizer. Undergraduate Topics in Computer Science. Springer. London (2007). https://doi.org/10.1007/978-1-84628-692-6. ISBN 978-1-84628-691-9

  32. Parrow, J.: General conditions for full abstraction. Math. Struct. Comput. Sci. 26(4), 655–657 (2016)

    Article  MathSciNet  Google Scholar 

  33. Patrignani, M.: Why should anyone use colours? Or, syntax highlighting beyond code snippets. CoRR abs/2001.11334 (2020)

    Google Scholar 

  34. Patrignani, M., Agten, P., Strackx, R., Jacobs, B., Clarke, D., Piessens, F.: Secure compilation to protected module architectures. ACM Trans. Program. Lang. Syst. 37(2), 6:1–6:50 (2015)

    Google Scholar 

  35. Patrignani, M., Ahmed, A., Clarke, D.: Formal approaches to secure compilation: a survey of fully abstract compilation and related work. ACM Comput. Surv. (CSUR) 51(6), 1–36 (2019)

    Google Scholar 

  36. Patrignani, M., Clarke, D.: Fully abstract trace semantics for protected module architectures. Comput. Lang. Syst. Struct. 42, 22–45 (2015)

    MATH  Google Scholar 

  37. Patrignani, M., Garg, D.: Secure compilation and hyperproperty preservation. In: 2017 IEEE 30th Computer Security Foundations Symposium (CSF), pp. 392–404. IEEE (2017)

    Google Scholar 

  38. Patrignani, M., Martin, E.M., Devriese, D.: On the semantic expressiveness of recursive types. Proc. ACM Program. Lang. 5(Popl), 1–29 (2021)

    Google Scholar 

  39. Piessens, F.: Security across abstraction layers: old and new examples. In: 2020 IEEE European Symposium on Security and Privacy Workshops (EuroS&PW), pp. 271–279. IEEE (2020)

    Google Scholar 

  40. Plotkin, G.D.: LCF considered as a programming language. Theoret. Comput. Sci. 5(3), 223–255 (1977)

    Article  MathSciNet  Google Scholar 

  41. Plotkin, G.D.: A structural approach to operational semantics. Aarhus university (1981)

    Google Scholar 

  42. Sabry, A., Wadler, P.: A reflection on call-by-value. ACM Trans. Program. Lang. Syst. (TOPLAS) 19(6), 916–941 (1997)

    Article  Google Scholar 

  43. Skorstengaard, L., Devriese, D., Birkedal, L.: StkTokens: enforcing well-bracketed control flow and stack encapsulation using linear capabilities. Proc. ACM Program. Lang. 3(Popl), 19:1–19:28 (2019)

    Google Scholar 

  44. Stewart, G., Beringer, L., Cuellar, S., Appel, A.W.: Compositional compcert. In: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 275–287 (2015)

    Google Scholar 

  45. Strydonck, T.V., Piessens, F., Devriese, D.: Linear capabilities for fully abstract compilation of separation-logic-verified code. Proc. ACM Program. Lang. 3(ICFP), 84:1–84:29 (2019)

    Google Scholar 

  46. Tan, Y.K., Myreen, M.O., Kumar, R., Fox, A., Owens, S., Norrish, M.: The verified cakeML compiler backend. J. Func. Program. 29 (2019)

    Google Scholar 

  47. Thibault, J., Hritcu, C.: Nanopass back-translation of multiple traces for secure compilation proofs. In: 5th Workshop on Principles of Secure Compilation, PriSC 2021, Virtual Event, 17 January 2021 (2021). http://perso.eleves.ens-rennes.fr/people/Jeremy.Thibault/prisc2021.pdf

  48. Tsampas, S., Nuyts, A., Devriese, D., Piessens, F.: A categorical approach to secure compilation. In: Petrişan, D., Rot, J. (eds.) CMCS 2020. LNCS, vol. 12094, pp. 155–179. Springer, Cham (2020). https://doi.org/10.1007/978-3-030-57201-3_9

    Chapter  Google Scholar 

  49. Turi, D.: Categorical modelling of structural operational rules: case studies. In: Category Theory and Computer Science, 7th International Conference, CTCS 1997, Santa Margherita Ligure, Italy, 4–6 September 1997, Proceedings, pp. 127–146 (1997)

    Google Scholar 

  50. Turi, D., Plotkin, G.: Towards a mathematical operational semantics. In: Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, pp. 280–291. IEEE (1997)

    Google Scholar 

  51. Watanabe, H.: Well-behaved translations between structural operational semantics. Electr. Notes Theoret. Comput. Sci. 65(1), 337–357 (2002)

    Article  Google Scholar 

  52. Winskel, G., Nielsen, M.: Models for concurrency. DAIMI Rep. Ser. 22(463) (1993)

    Google Scholar 

Download references

Acknowledgements

We are grateful to Pierpaolo Degano, Letterio Galletta, Catalin Hritcu, Marco Patrignani, Frank Piessens, and Jeremy Thibault for their feedback on early versions of this paper. We would also like to thank the anonymous reviewers for their insightful comments and suggestions that helped to improve our presentation.

Carmine Abate is supported by the European Research Council https://erc.europa.eu/ under ERC Starting Grant SECOMP (715753). Matteo Busi is partially supported by the research grant on Formal Methods and Techniques for Secure Compilation from the Department of Computer Science of the University of Pisa.

Author information

Authors and Affiliations

  1. MPI-SP Bochum, Bochum, Germany

    Carmine Abate

  2. Università di Pisa, Pisa, Italy

    Matteo Busi

  3. KU Leuven, Leuven, Belgium

    Stelios Tsampas

Authors
  1. Carmine Abate
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Matteo Busi
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Stelios Tsampas
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Stelios Tsampas .

Editor information

Editors and Affiliations

  1. Korea University, Seoul, Korea (Republic of)

    Hakjoo Oh

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Abate, C., Busi, M., Tsampas, S. (2021). Fully Abstract and Robust Compilation. In: Oh, H. (eds) Programming Languages and Systems. APLAS 2021. Lecture Notes in Computer Science(), vol 13008. Springer, Cham. https://doi.org/10.1007/978-3-030-89051-3_6

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-89051-3_6

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-89050-6

  • Online ISBN: 978-3-030-89051-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation