{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,27]],"date-time":"2026-02-27T02:19:16Z","timestamp":1772158756573,"version":"3.50.1"},"publisher-location":"Cham","reference-count":72,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783030171834","type":"print"},{"value":"9783030171841","type":"electronic"}],"license":[{"start":{"date-parts":[[2019,1,1]],"date-time":"2019-01-01T00:00:00Z","timestamp":1546300800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2019]]},"DOI":"10.1007\/978-3-030-17184-1_17","type":"book-chapter","created":{"date-parts":[[2019,4,6]],"date-time":"2019-04-06T21:34:04Z","timestamp":1554586444000},"page":"469-498","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":10,"title":["Robustly Safe Compilation"],"prefix":"10.1007","author":[{"given":"Marco","family":"Patrignani","sequence":"first","affiliation":[]},{"given":"Deepak","family":"Garg","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2019,4,6]]},"reference":[{"key":"17_CR1","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"611","DOI":"10.1007\/BFb0014571","volume-title":"Theoretical Aspects of Computer Software","author":"M Abadi","year":"1997","unstructured":"Abadi, M.: Secrecy by typing in security protocols. In: Abadi, M., Ito, T. (eds.) TACS 1997. LNCS, vol. 1281, pp. 611\u2013638. Springer, Heidelberg (1997). https:\/\/doi.org\/10.1007\/BFb0014571"},{"key":"17_CR2","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/3-540-48749-2_2","volume-title":"Secure Internet Programming","author":"M Abadi","year":"1999","unstructured":"Abadi, M.: Protection in programming-language translations. In: Vitek, J., Jensen, C.D. (eds.) Secure Internet Programming. LNCS, vol. 1603, pp. 19\u201334. Springer, Heidelberg (1999). https:\/\/doi.org\/10.1007\/3-540-48749-2_2"},{"issue":"1","key":"17_CR3","doi-asserted-by":"publisher","first-page":"4:1","DOI":"10.1145\/1609956.1609960","volume":"13","author":"M Abadi","year":"2009","unstructured":"Abadi, M., Budiu, M., Erlingsson, \u00da., Ligatti, J.: Control-flow integrity principles, implementations, and applications. ACM Trans. Inf. Syst. Secur. 13(1), 4:1\u20134:40 (2009)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"17_CR4","doi-asserted-by":"crossref","unstructured":"Abadi, M., Fournet, C., Gonthier, G.: Authentication primitives and their compilation. In: Proceedings of the 27th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2000, pp. 302\u2013315. ACM, New York (2000)","DOI":"10.1145\/325694.325734"},{"key":"17_CR5","doi-asserted-by":"publisher","first-page":"37","DOI":"10.1006\/inco.2002.3086","volume":"174","author":"M Abadi","year":"2002","unstructured":"Abadi, M., Fournet, C., Gonthier, G.: Secure implementation of channel abstractions. Inf. Comput. 174, 37\u201383 (2002)","journal-title":"Inf. Comput."},{"key":"17_CR6","doi-asserted-by":"publisher","first-page":"8:1","DOI":"10.1145\/2240276.2240279","volume":"15","author":"M Abadi","year":"2012","unstructured":"Abadi, M., Plotkin, G.D.: On protection by layout randomization. ACM Trans. Inf. Syst. Secur. 15, 8:1\u20138:29 (2012)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"17_CR7","doi-asserted-by":"crossref","unstructured":"Abate, C., et al.: When good components go bad: formally secure compilation despite dynamic compromise. In: CCS 2018 (2018)","DOI":"10.1145\/3243734.3243745"},{"key":"17_CR8","doi-asserted-by":"crossref","unstructured":"Abate, C., Blanco, R., Garg, D., Hri\u0163cu, C., Patrignani, M., Thibault, J.: Journey beyond full abstraction: exploring robust property preservation for secure compilation. arXiv:1807.04603 , July 2018","DOI":"10.1109\/CSF.2019.00025"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Agten, P., Strackx, R., Jacobs, B., Piessens, F.: Secure compilation to modern processors. In: 2012 IEEE 25th Computer Security Foundations Symposium, CSF 2012, pp. 171\u2013185. IEEE (2012)","DOI":"10.1109\/CSF.2012.12"},{"key":"17_CR10","doi-asserted-by":"crossref","unstructured":"Ahmed, A., Blume, M.: Typed closure conversion preserves observational equivalence. In: Proceedings of the 13th ACM SIGPLAN International Conference on Functional Programming, ICFP 2008, pp. 157\u2013168. ACM, New York (2008)","DOI":"10.1145\/1411204.1411227"},{"key":"17_CR11","doi-asserted-by":"crossref","unstructured":"Ahmed, A., Blume, M.: An equivalence-preserving CPS translation via multi-language semantics. In: Proceedings of the 16th ACM SIGPLAN International Conference on Functional Programming, ICFP 2011, pp. 431\u2013444. ACM, New York (2011)","DOI":"10.1145\/2034773.2034830"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Almeida, J.B., et al.: Jasmin: high-assurance and high-speed cryptography. In: ACM Conference on Computer and Communications Security, pp. 1807\u20131823. ACM (2017)","DOI":"10.1145\/3133956.3134078"},{"issue":"4","key":"17_CR13","doi-asserted-by":"publisher","first-page":"181","DOI":"10.1016\/0020-0190(85)90056-0","volume":"21","author":"B Alpern","year":"1985","unstructured":"Alpern, B., Schneider, F.B.: Defining liveness. Inf. Process. Lett. 21(4), 181\u2013185 (1985)","journal-title":"Inf. Process. Lett."},{"issue":"2","key":"17_CR14","doi-asserted-by":"publisher","first-page":"301","DOI":"10.3233\/JCS-130493","volume":"22","author":"M Backes","year":"2014","unstructured":"Backes, M., Hritcu, C., Maffei, M.: Union, intersection and refinement types and reasoning about type disjointness for secure protocol implementations. J. Comput. Secur. 22(2), 301\u2013353 (2014)","journal-title":"J. Comput. Secur."},{"key":"17_CR15","doi-asserted-by":"crossref","unstructured":"Barthe, G., Gr\u00e9goire, B., Laporte, V.: Secure compilation of side-channel countermeasures: the case of cryptographic \u201cconstant-time\u201d. In: CSF 2018 (2018)","DOI":"10.1109\/CSF.2018.00031"},{"key":"17_CR16","first-page":"35","volume":"33","author":"G Barthe","year":"2007","unstructured":"Barthe, G., Rezk, T., Basu, A.: Security types preserving compilation. Comput. Lang. Syst. Struct. 33, 35\u201359 (2007)","journal-title":"Comput. Lang. Syst. Struct."},{"issue":"2","key":"17_CR17","doi-asserted-by":"publisher","first-page":"8:1","DOI":"10.1145\/1890028.1890031","volume":"33","author":"J Bengtson","year":"2011","unstructured":"Bengtson, J., Bhargavan, K., Fournet, C., Gordon, A.D., Maffeis, S.: Refinement types for secure implementations. ACM Trans. Program. Lang. Syst. 33(2), 8:1\u20138:45 (2011)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"17_CR18","unstructured":"Benton, N., Hur, C.-K.: Realizability and compositional compiler correctness for a polymorphic language. Technical report, MSR (2010)"},{"issue":"1","key":"17_CR19","doi-asserted-by":"publisher","first-page":"217","DOI":"10.1016\/0304-3975(92)90185-I","volume":"96","author":"G Berry","year":"1992","unstructured":"Berry, G., Boudol, G.: The chemical abstract machine. Theor. Comput. Sci. 96(1), 217\u2013248 (1992)","journal-title":"Theor. Comput. Sci."},{"key":"17_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"20","DOI":"10.1007\/978-3-642-01465-9_2","volume-title":"Formal Aspects in Security and Trust","author":"G Boudol","year":"2009","unstructured":"Boudol, G.: Secure information flow as a safety property. In: Degano, P., Guttman, J., Martinelli, F. (eds.) FAST 2008. LNCS, vol. 5491, pp. 20\u201334. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-01465-9_2"},{"key":"17_CR21","doi-asserted-by":"crossref","unstructured":"Bowman, W.J., Ahmed, A.: Noninterference for free. In: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015. ACM, New York (2015)","DOI":"10.1145\/2784731.2784733"},{"key":"17_CR22","doi-asserted-by":"crossref","unstructured":"Bugliesi, M., Giunti, M.: Secure implementations of typed channel abstractions. In: Proceedings of the 34th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, pp. 251\u2013262. ACM, New York (2007)","DOI":"10.1145\/1190216.1190253"},{"key":"17_CR23","doi-asserted-by":"publisher","first-page":"319","DOI":"10.1145\/195470.195579","volume":"29","author":"NP Carter","year":"1994","unstructured":"Carter, N.P., Keckler, S.W., Dally, W.J.: Hardware support for fast capability-based addressing. SIGPLAN Not. 29, 319\u2013327 (1994)","journal-title":"SIGPLAN Not."},{"key":"17_CR24","unstructured":"Chong, S.: Expressive and enforceable information security policies. Ph.D. thesis, Cornell University, August 2008"},{"issue":"6","key":"17_CR25","doi-asserted-by":"publisher","first-page":"1157","DOI":"10.3233\/JCS-2009-0393","volume":"18","author":"MR Clarkson","year":"2010","unstructured":"Clarkson, M.R., Schneider, F.B.: Hyperproperties. J. Comput. Secur. 18(6), 1157\u20131210 (2010)","journal-title":"J. Comput. Secur."},{"key":"17_CR26","doi-asserted-by":"publisher","first-page":"573","DOI":"10.3233\/JCS-2008-0334","volume":"16","author":"R Corin","year":"2008","unstructured":"Corin, R., Deni\u00e9lou, P.-M., Fournet, C., Bhargavan, K., Leifer, J.: A secure compiler for session abstractions. J. Comput. Secur. 16, 573\u2013636 (2008)","journal-title":"J. Comput. Secur."},{"key":"17_CR27","doi-asserted-by":"crossref","unstructured":"Costanzo, D., Shao, Z., Gu, R.: End-to-end verification of information-flow security for C and assembly programs. In: PLDI, pp. 648\u2013664. ACM (2016)","DOI":"10.1145\/2980983.2908100"},{"key":"17_CR28","unstructured":"Devriese, D., Patrignani, M., Keuchel, S., Piessens, F.: Modular, fully-abstract compilation by approximate back-translation. Log. Methods Comput. Sci. 13(4) (2017). https:\/\/lmcs.episciences.org\/4011"},{"key":"17_CR29","doi-asserted-by":"crossref","unstructured":"Devriese, D., Patrignani, M., Piessens, F.: Secure compilation by approximate back-translation. In: POPL 2016 (2016)","DOI":"10.1145\/2837614.2837618"},{"key":"17_CR30","unstructured":"El-Korashy, A.: A formal model for capability machines - an illustrative case study towards secure compilation to CHERI. Master\u2019s thesis, Universitat des Saarlandes (2016)"},{"issue":"5","key":"17_CR31","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1145\/1275497.1275500","volume":"29","author":"C Fournet","year":"2007","unstructured":"Fournet, C., Gordon, A.D., Maffeis, S.: A type discipline for authorization policies. ACM Trans. Program. Lang. Syst. 29(5), 141\u2013156 (2007)","journal-title":"ACM Trans. Program. Lang. Syst."},{"key":"17_CR32","doi-asserted-by":"crossref","unstructured":"Fournet, C., Swamy, N., Chen, J., Dagand, P.-E., Strub, P.-Y., Livshits, B.: Fully abstract compilation to JavaScript. In: Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2013, pp. 371\u2013384. ACM, New York (2013)","DOI":"10.1145\/2480359.2429114"},{"key":"17_CR33","unstructured":"Garg, D., Hritcu, C., Patrignani, M., Stronati, M., Swasey, D.: Robust hyperproperty preservation for secure compilation (extended abstract). ArXiv e-prints, October 2017"},{"issue":"4","key":"17_CR34","doi-asserted-by":"publisher","first-page":"451","DOI":"10.3233\/JCS-2003-11402","volume":"11","author":"AD Gordon","year":"2003","unstructured":"Gordon, A.D., Jeffrey, A.: Authenticity by typing for security protocols. J. Comput. Secur. 11(4), 451\u2013519 (2003)","journal-title":"J. Comput. Secur."},{"issue":"4","key":"17_CR35","doi-asserted-by":"publisher","first-page":"639","DOI":"10.1017\/S0960129514000279","volume":"26","author":"D Gorla","year":"2016","unstructured":"Gorla, D., Nestman, U.: Full abstraction for expressiveness: history, myths and facts. Math. Struct. Comput. Sci. 26(4), 639\u2013654 (2016)","journal-title":"Math. Struct. Comput. Sci."},{"key":"17_CR36","doi-asserted-by":"publisher","first-page":"133","DOI":"10.1145\/1925844.1926402","volume":"46","author":"C-K Hur","year":"2011","unstructured":"Hur, C.-K., Dreyer, D.: A Kripke logical relation between ML and assembly. SIGPLAN Not. 46, 133\u2013146 (2011)","journal-title":"SIGPLAN Not."},{"key":"17_CR37","doi-asserted-by":"crossref","unstructured":"Jagadeesan, R., Pitcher, C., Rathke, J., Riely, J.: Local memory via layout randomization. In: Proceedings of the 2011 IEEE 24th Computer Security Foundations Symposium, CSF 2011, Washington, DC, USA, pp. 161\u2013174. IEEE Computer Society (2011)","DOI":"10.1109\/CSF.2011.18"},{"key":"17_CR38","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/978-3-540-31987-0_29","volume-title":"Programming Languages and Systems","author":"A Jeffrey","year":"2005","unstructured":"Jeffrey, A., Rathke, J.: Java JR: fully abstract trace semantics for a core Java language. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 423\u2013438. Springer, Heidelberg (2005). https:\/\/doi.org\/10.1007\/978-3-540-31987-0_29"},{"key":"17_CR39","doi-asserted-by":"crossref","unstructured":"Juglaret, Y., Hri\u0163cu, C., de Amorim, A.A., Pierce, B.C.: Beyond good and evil: formalizing the security guarantees of compartmentalizing compilation. In: 29th IEEE Symposium on Computer Security Foundations (CSF). IEEE Computer Society Press, July 2016. To appear","DOI":"10.1109\/CSF.2016.11"},{"key":"17_CR40","doi-asserted-by":"crossref","unstructured":"Kang, J., Kim, Y., Hur, C.-K., Dreyer, D., Vafeiadis, V.: Lightweight verification of separate compilation. In: POPL 2016, pp. 178\u2013190 (2016)","DOI":"10.1145\/2914770.2837642"},{"key":"17_CR41","unstructured":"Kuznetsov, V., Szekeres, L., Payer, M., Candea, G., Sekar, R., Song, D.: Code-pointer integrity. In: Proceedings of the 11th USENIX Conference on Operating Systems Design and Implementation, OSDI 2014, Berkeley, CA, USA, pp. 147\u2013163. USENIX Association (2014)"},{"key":"17_CR42","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"29","DOI":"10.1007\/978-3-319-26529-2_3","volume-title":"Programming Languages and Systems","author":"A Larmuseau","year":"2015","unstructured":"Larmuseau, A., Patrignani, M., Clarke, D.: A secure compiler for ML modules. In: Feng, X., Park, S. (eds.) APLAS 2015. LNCS, vol. 9458, pp. 29\u201348. Springer, Cham (2015). https:\/\/doi.org\/10.1007\/978-3-319-26529-2_3"},{"key":"17_CR43","doi-asserted-by":"crossref","unstructured":"Leroy, X.: Formal certification of a compiler back-end or: programming a compiler with a proof assistant. In: POPL, pp. 42\u201354 (2006)","DOI":"10.1145\/1111320.1111042"},{"issue":"4","key":"17_CR44","doi-asserted-by":"publisher","first-page":"363","DOI":"10.1007\/s10817-009-9155-4","volume":"43","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: A formally verified compiler back-end. J. Autom. Reason. 43(4), 363\u2013446 (2009)","journal-title":"J. Autom. Reason."},{"key":"17_CR45","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"563","DOI":"10.1007\/978-3-540-88313-5_36","volume-title":"Computer Security - ESORICS 2008","author":"S Maffeis","year":"2008","unstructured":"Maffeis, S., Abadi, M., Fournet, C., Gordon, A.D.: Code-carrying authorization. In: Jajodia, S., Lopez, J. (eds.) ESORICS 2008. LNCS, vol. 5283, pp. 563\u2013579. Springer, Heidelberg (2008). https:\/\/doi.org\/10.1007\/978-3-540-88313-5_36"},{"key":"17_CR46","unstructured":"McKeen, F., et al.: Innovative instructions and software model for isolated execution. In: HASP 2013, pp. 10:1\u201310:1. ACM (2013)"},{"key":"17_CR47","doi-asserted-by":"publisher","first-page":"15","DOI":"10.1145\/361932.361937","volume":"16","author":"JH Morris Jr","year":"1973","unstructured":"Morris Jr., J.H.: Protection in programming languages. Commun. ACM 16, 15\u201321 (1973)","journal-title":"Commun. ACM"},{"issue":"9","key":"17_CR48","doi-asserted-by":"publisher","first-page":"135","DOI":"10.1145\/1631687.1596572","volume":"44","author":"G Neis","year":"2009","unstructured":"Neis, G., Dreyer, D., Rossberg, A.: Non-parametric parametricity. SIGPLAN Not. 44(9), 135\u2013148 (2009)","journal-title":"SIGPLAN Not."},{"key":"17_CR49","doi-asserted-by":"crossref","unstructured":"Neis, G., Hur, C.-K., Kaiser, J.-O., McLaughlin, C., Dreyer, D., Vafeiadis, V.: Pilsner: a compositionally verified compiler for a higher-order imperative language. In: Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, pp. 166\u2013178. ACM (2015)","DOI":"10.1145\/2784731.2784764"},{"key":"17_CR50","doi-asserted-by":"crossref","unstructured":"New, M.S., Bowman, W.J., Ahmed, A.: Fully abstract compilation via universal embedding. In: Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, pp. 103\u2013116. ACM, New York (2016)","DOI":"10.1145\/2951913.2951941"},{"key":"17_CR51","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-03811-6","volume-title":"Principles of Program Analysis","author":"F Nielson","year":"1999","unstructured":"Nielson, F., Nielson, H.R., Hankin, C.: Principles of Program Analysis. Springer, New York (1999). https:\/\/doi.org\/10.1007\/978-3-662-03811-6"},{"issue":"4","key":"17_CR52","doi-asserted-by":"publisher","first-page":"655","DOI":"10.1017\/S0960129514000280","volume":"26","author":"J Parrow","year":"2014","unstructured":"Parrow, J.: General conditions for full abstraction. Math. Struct. Comput. Sci. 26(4), 655\u2013657 (2014)","journal-title":"Math. Struct. Comput. Sci."},{"key":"17_CR53","doi-asserted-by":"publisher","first-page":"6:1","DOI":"10.1145\/2699503","volume":"37","author":"M Patrignani","year":"2015","unstructured":"Patrignani, M., Agten, P., Strackx, R., Jacobs, B., Clarke, D., Piessens, F.: Secure compilation to protected module architectures. ACM Trans. Program. Lang. Syst. 37, 6:1\u20136:50 (2015)","journal-title":"ACM Trans. Program. Lang. Syst."},{"issue":"6","key":"17_CR54","doi-asserted-by":"publisher","first-page":"125:1","DOI":"10.1145\/3280984","volume":"51","author":"M Patrignani","year":"2019","unstructured":"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\u2013125:36 (2019)","journal-title":"ACM Comput. Surv."},{"key":"17_CR55","doi-asserted-by":"crossref","unstructured":"Patrignani, M., Clarke, D.: Fully abstract trace semantics of low-level isolation mechanisms. In: Proceedings of the 29th Annual ACM Symposium on Applied Computing, SAC 2014, pp. 1562\u20131569. ACM (2014)","DOI":"10.1145\/2554850.2554865"},{"issue":"0","key":"17_CR56","first-page":"22","volume":"42","author":"M Patrignani","year":"2015","unstructured":"Patrignani, M., Clarke, D.: Fully abstract trace semantics for protected module architectures. Comput. Lang. Syst. Struct. 42(0), 22\u201345 (2015)","journal-title":"Comput. Lang. Syst. Struct."},{"key":"17_CR57","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"176","DOI":"10.1007\/978-3-319-03542-0_13","volume-title":"Programming Languages and Systems","author":"M Patrignani","year":"2013","unstructured":"Patrignani, M., Clarke, D., Piessens, F.: Secure compilation of object-oriented components to protected module architectures. In: Shan, C. (ed.) APLAS 2013. LNCS, vol. 8301, pp. 176\u2013191. Springer, Cham (2013). https:\/\/doi.org\/10.1007\/978-3-319-03542-0_13"},{"key":"17_CR58","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"289","DOI":"10.1007\/978-3-642-21461-5_19","volume-title":"Formal Techniques for Distributed Systems","author":"M Patrignani","year":"2011","unstructured":"Patrignani, M., Clarke, D., Sangiorgi, D.: Ownership types for the join calculus. In: Bruni, R., Dingel, J. (eds.) FMOODS\/FORTE -2011. LNCS, vol. 6722, pp. 289\u2013303. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-21461-5_19"},{"key":"17_CR59","doi-asserted-by":"crossref","unstructured":"Patrignani, M., Devriese, D., Piessens, F.: On modular and fully abstract compilation. In: Proceedings of the 29th IEEE Computer Security Foundations Symposium, CSF 2016 (2016)","DOI":"10.1109\/CSF.2016.9"},{"key":"17_CR60","doi-asserted-by":"crossref","unstructured":"Patrignani, M., Garg, D.: Secure compilation and hyperproperties preservation. In: Proceedings of the 30th IEEE Computer Security Foundations Symposium, CSF 2017, Santa Barbara, USA (2017)","DOI":"10.1109\/CSF.2017.13"},{"key":"17_CR61","unstructured":"Patrignani, M., Garg, D.: Robustly safe compilation or, efficient, provably secure compilation. CoRR, abs\/1804.00489 (2018)"},{"issue":"5","key":"17_CR62","doi-asserted-by":"publisher","first-page":"517","DOI":"10.3233\/JCS-2009-0352","volume":"17","author":"A Sabelfeld","year":"2009","unstructured":"Sabelfeld, A., Sands, D.: Declassification: dimensions and principles. J. Comput. Secur. 17(5), 517\u2013548 (2009)","journal-title":"J. Comput. Secur."},{"issue":"1","key":"17_CR63","doi-asserted-by":"publisher","first-page":"30","DOI":"10.1145\/353323.353382","volume":"3","author":"FB Schneider","year":"2000","unstructured":"Schneider, F.B.: Enforceable security policies. ACM Trans. Inf. Syst. Secur. 3(1), 30\u201350 (2000)","journal-title":"ACM Trans. Inf. Syst. Secur."},{"key":"17_CR64","unstructured":"Stark, I.: Names and higher-order functions. Ph.D. thesis, University of Cambridge, December 1994. Also available as Technical Report 363, University of Cambridge Computer Laboratory"},{"key":"17_CR65","doi-asserted-by":"crossref","unstructured":"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, POPL 2015, pp. 275\u2013287. ACM, New York (2015)","DOI":"10.1145\/2775051.2676985"},{"key":"17_CR66","doi-asserted-by":"crossref","unstructured":"Sumii, E., Pierce, B.C.: A bisimulation for dynamic sealing. In: Principles of Programming Languages, pp. 161\u2013172 (2004)","DOI":"10.1145\/982962.964015"},{"issue":"1","key":"17_CR67","doi-asserted-by":"crossref","first-page":"425","DOI":"10.1145\/2578855.2535889","volume":"49","author":"N Swamy","year":"2014","unstructured":"Swamy, N., Fournet, C., Rastogi, A., Bhargavan, K., Chen, J., Strub, P.-Y., Bierman, G.: Gradual typing embedded securely in Javascript. SIGPLAN Not. 49(1), 425\u2013437 (2014)","journal-title":"SIGPLAN Not."},{"key":"17_CR68","unstructured":"Swasey, D., Garg, D., Dreyer, D.: Robust and compositional verification of object capability patterns. In: Proceedings of the 2017 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2017, 22\u201327 October 2017 (2017)"},{"key":"17_CR69","unstructured":"Tsampas, S., El-Korashy, A., Patrignani, M., Devriese, D., Garg, D., Piessens, F.: Towards automatic compartmentalization of C programs on capability machines. In: 2017 Workshop on Foundations of Computer Security, FCS 2017, 21 August 2017 (2017)"},{"key":"17_CR70","doi-asserted-by":"publisher","first-page":"167","DOI":"10.3233\/JCS-1996-42-304","volume":"4","author":"D Volpano","year":"1996","unstructured":"Volpano, D., Irvine, C., Smith, G.: A sound type system for secure flow analysis. J. Comput. Secur. 4, 167\u2013187 (1996)","journal-title":"J. Comput. Secur."},{"key":"17_CR71","doi-asserted-by":"crossref","unstructured":"Woodruff, J., et al.: The CHERI capability model: revisiting RISC in an age of risk. In: Proceeding of the 41st Annual International Symposium on Computer Architecuture, ISCA 2014, Piscataway, NJ, USA, pp. 457\u2013468. IEEE Press (2014)","DOI":"10.1109\/ISCA.2014.6853201"},{"key":"17_CR72","unstructured":"Zdancewic, S.A.: Programming languages for information security. Ph.D. thesis, Cornell University (2002)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-030-17184-1_17","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,5]],"date-time":"2020-12-05T17:24:52Z","timestamp":1607189092000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-030-17184-1_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019]]},"ISBN":["9783030171834","9783030171841"],"references-count":72,"URL":"https:\/\/doi.org\/10.1007\/978-3-030-17184-1_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019]]},"assertion":[{"value":"6 April 2019","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"ESOP","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"European Symposium on Programming","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Prague","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Czech Republic","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2019","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"8 April 2019","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"11 April 2019","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"28","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"esop2019","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.etaps.org\/2019\/esop","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"86","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"28","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"33% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"3,2","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"12","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information"}}]}}