Fully abstract and robust compilation. And how to reconcile the two, abstractly. (English) Zbl 1520.68025
Oh, Hakjoo (ed.), Programming languages and systems. 19th Asian symposium, APLAS 2021, Chicago, IL, USA, October 17–18, 2021. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 13008, 83-101 (2021).
Summary: 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.
For the entire collection see [Zbl 1507.68042].
For the entire collection see [Zbl 1507.68042].
MSC:
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
| 68N20 | Theory of compilers and interpreters |
| 68Q55 | Semantics in the theory of computing |
Keywords:
secure compilation; fully abstract compilation; robust hyperproperty preservation; language-based security; mathematical operational semanticsSoftware:
CompCertReferences:
| [1] | Abadi, M.: Protection in programming-language translations. In: Secure Internet Programming, Security Issues for Mobile and Distributed Objects, pp. 19-34 (1999) |
| [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) |
| [3] | Abate, C., Trace-relating compiler correctness and secure compilation, Programming Languages and Systems, 1-28 (2020), Cham: Springer, Cham · Zbl 1508.68046 · doi:10.1007/978-3-030-44914-8_1 |
| [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) |
| [5] | Abate, C., Busi, M., Tsampas, S.: Fully abstract and robust compilation and how to reconcile the two, abstractly (2021) |
| [6] | Abou-Saleh, F., Pattinson, D.: Towards effects in mathematical operational semantics. Electr. Notes Theor. Comput. Sci. 276, 81-104 (2011) · Zbl 1342.68064 |
| [7] | Aceto, L., Fokkink, W., Verhoef, C.: Structural operational semantics. In: Handbook of Process Algebra, pp. 197-292. Elsevier (2001) · Zbl 1062.68074 |
| [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) · Zbl 1323.68350 |
| [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). doi:10.1145/2034773.2034830 · Zbl 1323.68088 |
| [10] | Barthe, G., et al.: Formal verification of a constant-time preserving C compiler. Proc. ACM Program. Lang. 4(Popl), 1-30 (2019) |
| [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) |
| [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) · Zbl 1465.68041 |
| [13] | Bowman, W.J., Ahmed, A.: Noninterference for free. ACM SIGPLAN Not. 50(9), 101-113 (2015) · Zbl 1360.68315 |
| [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) |
| [15] | Clarkson, MR; Schneider, FB, Hyperproperties, J. Comput. Secur., 18, 6, 1157-1210 (2010) · doi:10.3233/JCS-2009-0393 |
| [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) · Zbl 1347.68064 |
| [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) |
| [18] | Durumeric, Z., et al.: The matter of heartbleed. In: Proceedings of the 2014 Conference on Internet Measurement Conference, pp. 475-488 (2014) |
| [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) |
| [20] | Engelfriet, J., Determinacy - (observation equivalence = trace equivalence), Theor. Comput. Sci., 36, 1, 21-25 (1985) · Zbl 0571.68018 · doi:10.1016/0304-3975(85)90028-3 |
| [21] | Gorla, D.; Nestmann, U., Full abstraction for expressiveness: history, myths and facts, Math. Struct. Comput. Sci., 26, 4, 639-654 (2016) · Zbl 1361.68028 · doi:10.1017/S0960129514000279 |
| [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 |
| [23] | Jacobs, K., Timany, A., Devriese, D.: Fully abstract from static to gradual. Proc. ACM Program. Lang. 5(Popl), 1-30 (2021) |
| [24] | Klin, B., Bialgebras for structural operational semantics: an introduction, Theoret. Comput. Sci., 412, 38, 5043-5069 (2011) · Zbl 1246.68150 · doi:10.1016/j.tcs.2011.03.023 |
| [25] | Klin, B.; Sassone, V.; Amadio, R., Structural operational semantics for stochastic process calculi, Foundations of Software Science and Computational Structures, 428-442 (2008), Heidelberg: Springer, Heidelberg · Zbl 1138.68468 · doi:10.1007/978-3-540-78499-9_30 |
| [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) · Zbl 1369.68124 |
| [27] | Melton, A.; Schmidt, DA; Strecker, GE; Pitt, D.; Abramsky, S.; Poigné, A.; Rydeheard, D., Galois connections and computer science applications, Category Theory and Computer Programming, 299-312 (1986), Heidelberg: Springer, Heidelberg · Zbl 0622.06004 · doi:10.1007/3-540-17162-2_130 |
| [28] | Mitchell, JC, On abstraction and the expressive power of programming languages, Sci. Comput. Program., 21, 2, 141-163 (1993) · Zbl 0809.68049 · doi:10.1016/0167-6423(93)90004-9 |
| [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) · Zbl 0309.68026 |
| [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) |
| [31] | Nielson, H.R., Nielson, F.: Semantics with Applications: An Appetizer. Undergraduate Topics in Computer Science. Springer. London (2007). doi:10.1007/978-1-84628-692-6. ISBN 978-1-84628-691-9 · Zbl 1126.68052 |
| [32] | Parrow, J., General conditions for full abstraction, Math. Struct. Comput. Sci., 26, 4, 655-657 (2016) · Zbl 1361.68085 · doi:10.1017/S0960129514000280 |
| [33] | Patrignani, M.: Why should anyone use colours? Or, syntax highlighting beyond code snippets. CoRR abs/2001.11334 (2020) |
| [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) |
| [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) |
| [36] | Patrignani, M.; Clarke, D., Fully abstract trace semantics for protected module architectures, Comput. Lang. Syst. Struct., 42, 22-45 (2015) · Zbl 1387.68054 |
| [37] | Patrignani, M., Garg, D.: Secure compilation and hyperproperty preservation. In: 2017 IEEE 30th Computer Security Foundations Symposium (CSF), pp. 392-404. IEEE (2017) |
| [38] | Patrignani, M., Martin, E.M., Devriese, D.: On the semantic expressiveness of recursive types. Proc. ACM Program. Lang. 5(Popl), 1-29 (2021) |
| [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) |
| [40] | Plotkin, GD, LCF considered as a programming language, Theoret. Comput. Sci., 5, 3, 223-255 (1977) · Zbl 0369.68006 · doi:10.1016/0304-3975(77)90044-5 |
| [41] | Plotkin, G.D.: A structural approach to operational semantics. Aarhus university (1981) |
| [42] | Sabry, A.; Wadler, P., A reflection on call-by-value, ACM Trans. Program. Lang. Syst. (TOPLAS), 19, 6, 916-941 (1997) · doi:10.1145/267959.269968 |
| [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) |
| [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) · Zbl 1346.68056 |
| [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) |
| [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) · Zbl 1493.68091 |
| [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.; Petrişan, D.; Rot, J., A categorical approach to secure compilation, Coalgebraic Methods in Computer Science, 155-179 (2020), Cham: Springer, Cham · Zbl 07314153 · doi:10.1007/978-3-030-57201-3_9 |
| [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) · Zbl 0881.18004 |
| [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) |
| [51] | Watanabe, H., Well-behaved translations between structural operational semantics, Electr. Notes Theoret. Comput. Sci., 65, 1, 337-357 (2002) · Zbl 1270.68159 · doi:10.1016/S1571-0661(04)80372-4 |
| [52] | Winskel, G., Nielsen, M.: Models for concurrency. DAIMI Rep. Ser. 22(463) (1993) |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
