{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:41:18Z","timestamp":1780994478362,"version":"3.54.1"},"publisher-location":"Cham","reference-count":49,"publisher":"Springer International Publishing","isbn-type":[{"value":"9783319897219","type":"print"},{"value":"9783319897226","type":"electronic"}],"license":[{"start":{"date-parts":[[2018,1,1]],"date-time":"2018-01-01T00:00:00Z","timestamp":1514764800000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/creativecommons.org\/licenses\/by\/4.0"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2018]]},"DOI":"10.1007\/978-3-319-89722-6_4","type":"book-chapter","created":{"date-parts":[[2018,4,13]],"date-time":"2018-04-13T10:53:50Z","timestamp":1523616830000},"page":"79-105","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":13,"title":["The Meaning of Memory Safety"],"prefix":"10.1007","author":[{"given":"Arthur","family":"Azevedo de Amorim","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"C\u0103t\u0103lin","family":"Hri\u0163cu","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Benjamin C.","family":"Pierce","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"297","published-online":{"date-parts":[[2018,4,14]]},"reference":[{"key":"4_CR1","unstructured":"Caja. Attack vectors for privilege escalation (2012). http:\/\/code.google.com\/p\/google-caja\/wiki\/AttackVectors"},{"key":"4_CR2","unstructured":"Agten, P., Jacobs, B., Piessens, F.: Sound modular verification of C code executing in an unverified context. In: POPL (2015). https:\/\/lirias.kuleuven.be\/bitstream\/123456789\/471365\/3\/sound-verification.pdf"},{"issue":"4","key":"4_CR3","first-page":"397","volume":"77","author":"A Ahmed","year":"2007","unstructured":"Ahmed, A., Fluet, M., Morrisett, G.: $${\\rm L}^3$$: a linear language with locations. Fundam. Inform. 77(4), 397\u2013449 (2007). http:\/\/content.iospress.com\/articles\/fundamenta-informaticae\/fi77-4-06","journal-title":"Fundam. Inform."},{"key":"4_CR4","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1007\/978-3-540-88313-5_22","volume-title":"Computer Security - ESORICS 2008","author":"Aslan Askarov","year":"2008","unstructured":"Askarov, A., Hunt, S., Sabelfeld, A., Sands, D.: Termination-insensitive noninterference leaks more than just a bit. In: ESORICS (2008). http:\/\/www.cse.chalmers.se\/~andrei\/esorics08.pdf"},{"key":"4_CR5","unstructured":"Azevedo de Amorim, A., D\u00e9n\u00e8s, M., Giannarakis, N., Hri\u0163cu, C., Pierce, B.C., Spector-Zabusky, A., Tolmach, A.: Micro-policies: formally verified, tag-based security monitors. In: S&P, Oakland (2015). http:\/\/prosecco.gforge.inria.fr\/personal\/hritcu\/publications\/micro-policies.pdf"},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"Backes, M., K\u00f6pf, B., Rybalchenko, A.: Automatic discovery and quantification of information leaks. In: S&P, Oakland (2009). https:\/\/doi.org\/10.1109\/SP.2009.18","DOI":"10.1109\/SP.2009.18"},{"key":"4_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"253","DOI":"10.1007\/978-3-319-07151-0_16","volume-title":"Functional and Logic Programming","author":"T Balabonski","year":"2014","unstructured":"Balabonski, T., Pottier, F., Protzenko, J.: Type soundness and race freedom for Mezzo. In: Codish, M., Sumii, E. (eds.) FLOPS 2014. LNCS, vol. 8475, pp. 253\u2013269. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-07151-0_16"},{"key":"4_CR8","unstructured":"Benton, N., Tabareau, N.: Compiling functional types to relational specifications for low level imperative code. In: Kennedy, A., Ahmed, A. (eds.) TLDI (2009). http:\/\/dblp.uni-trier.de\/db\/conf\/tldi\/tldi2009.html#BentonT09"},{"key":"4_CR9","doi-asserted-by":"crossref","unstructured":"Bhargavan, K., Delignat-Lavaud, A., Maffeis, S.: Defensive JavaScript - building and verifying secure web components. In: FOSAD (2013). http:\/\/dx.doi.org\/10.1007\/978-3-319-10082-1_4","DOI":"10.1007\/978-3-319-10082-1_4"},{"issue":"4","key":"4_CR10","doi-asserted-by":"publisher","first-page":"117","DOI":"10.1145\/2775054.2694367","volume":"50","author":"David Chisnall","year":"2015","unstructured":"Chisnall, D., Rothwell, C., Watson, R.N.M., Woodruff, J., Vadera, M., Moore, S.W., Roe, M., Davis, B., Neumann, P.G.: Beyond the PDP-11: architectural support for a memory-safe C abstract machine. In: ASPLOS (2015). https:\/\/www.cl.cam.ac.uk\/~dc552\/papers\/asplos15-memory-safe-c.pdf","journal-title":"ACM SIGPLAN Notices"},{"key":"4_CR11","unstructured":"Clause, J.A., Doudalis, I., Orso, A., Prvulovic, M.: Effective memory protection using dynamic tainting. In: ASE (2007). http:\/\/www.cc.gatech.edu\/~orso\/papers\/clause.doudalis.orso.prvulovic.pdf"},{"issue":"6","key":"4_CR12","doi-asserted-by":"publisher","first-page":"689","DOI":"10.3233\/JCS-15784","volume":"24","author":"AA Amorim de","year":"2016","unstructured":"de Amorim, A.A., Collins, N., DeHon, A., Demange, D., Hritcu, C., Pichardie, D., Pierce, B.C., Pollack, R., Tolmach, A.: A verified information-flow architecture. J. Comput. Secur. 24(6), 689\u2013734 (2016). https:\/\/doi.org\/10.3233\/JCS-15784","journal-title":"J. Comput. Secur."},{"key":"4_CR13","unstructured":"Devietti, J., Blundell, C., Martin, M.M.K., Zdancewic, S.: HardBound: architectural support for spatial safety of the C programming language. In: ASPLOS (2008). http:\/\/acg.cis.upenn.edu\/papers\/asplos08_hardbound.pdf"},{"key":"4_CR14","unstructured":"Devriese, D., Piessens, F., Birkedal, L.: Reasoning about object capabilities with logical relations and effect parametricity. In: EuroS&P (2016). http:\/\/cs.au.dk\/~birke\/papers\/object-capabilities-tr.pdf"},{"key":"4_CR15","unstructured":"Dhawan, U., Hri\u0163cu, C., Rubin, R., Vasilakis, N., Chiricescu, S., Smith, J.M., Knight Jr., T.F., Pierce, B.C., DeHon, A.: Architectural support for software-defined metadata processing. In: ASPLOS (2015). http:\/\/ic.ese.upenn.edu\/abstracts\/sdmp_asplos2015.html"},{"key":"4_CR16","unstructured":"Durumeric, Z., Kasten, J., Adrian, D., Halderman, J.A., Bailey, M., Li, F., Weaver, N., Amann, J., Beekman, J., Payer, M., Paxson, V.: The matter of Heartbleed. In: IMC (2014). http:\/\/doi.acm.org\/10.1145\/2663716.2663755"},{"key":"4_CR17","unstructured":"Elliott, T., Pike, L., Winwood, S., Hickey, P.C., Bielman, J., Sharp, J., Seidel, E.L., Launchbury, J.: Guilt free Ivory. In: Haskell (2015). https:\/\/www.cs.indiana.edu\/~lepike\/pubs\/ivory.pdf"},{"key":"4_CR18","unstructured":"Fournet, C., Swamy, N., Chen, J., Dagand, P.-\u00c9., Strub, P.-Y., Livshits, B.: Fully abstract compilation to JavaScript. In: POPL (2013). https:\/\/research.microsoft.com\/pubs\/176601\/js-star.pdf"},{"key":"4_CR19","unstructured":"Goguen, J.A., Meseguer, J.: Security policies and security models. In: S&P (1982). http:\/\/spy.sci.univr.it\/papers\/Isa-orig\/Sicurezza\/NonInterferenza\/noninter.pdf"},{"key":"4_CR20","unstructured":"Hicks, M.: What is memory safety? (2014). http:\/\/www.pl-enthusiast.net\/2014\/07\/21\/memory-safety\/"},{"key":"4_CR21","unstructured":"ISO. ISO C standard 1999. Technical report. ISO\/IEC 9899:1999 draft. ISO (1999). http:\/\/www.open-std.org\/jtc1\/sc22\/wg14\/www\/docs\/n1124.pdf"},{"key":"4_CR22","doi-asserted-by":"crossref","unstructured":"Jana, S., Shmatikov, V.: Memento: learning secrets from process footprints. In: S&P, Oakland (2012). https:\/\/doi.org\/10.1109\/SP.2012.19","DOI":"10.1109\/SP.2012.19"},{"key":"4_CR23","unstructured":"Kang, J., Hur, C., Mansky, W., Garbuzov, D., Zdancewic, S., Vafeiadis, V.: A formal C memory model supporting integer-pointer casts. In: PLDI (2015). https:\/\/www.seas.upenn.edu\/~wmansky\/mcast.pdf"},{"key":"4_CR24","unstructured":"Krebbers, R.: The C standard formalized in Coq. Ph.D. thesis, Radboud University Nijmegen (2015). http:\/\/robbertkrebbers.nl\/research\/thesis.pdf"},{"key":"4_CR25","unstructured":"Kwon, A., Dhawan, U., Smith, J.M., Knight Jr., T.F., DeHon, A.: Low-fat pointers: compact encoding and efficient gate-level implementation of fat pointers for spatial safety and capability-based security. In: CCS (2013). http:\/\/www.crash-safe.org\/node\/27"},{"issue":"1","key":"4_CR26","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/s10817-008-9099-0","volume":"41","author":"Xavier Leroy","year":"2008","unstructured":"Leroy, X., Blazy, S.: Formal verification of a C-like memory model and its uses for verifying program transformations. JAR 41(1), 1\u201331 (2008). http:\/\/pauillac.inria.fr\/~xleroy\/publi\/memory-model-journal.pdf","journal-title":"Journal of Automated Reasoning"},{"key":"4_CR27","unstructured":"Maffeis, S., Mitchell, J.C., Taly, A.: Object capabilities and isolation of untrusted web applications. In: S&P, Oakland (2010). https:\/\/www.doc.ic.ac.uk\/~maffeis\/papers\/oakland10.pdf"},{"key":"4_CR28","unstructured":"Memarian, K., Matthiesen, J., Lingard, J., Nienhuis, K., Chisnall, D., Watson, R.N.M., Sewell, P.: Into the depths of C: elaborating the de facto standards. In: PLDI (2016). http:\/\/doi.acm.org\/10.1145\/2908080.2908081"},{"key":"4_CR29","doi-asserted-by":"crossref","unstructured":"Meyerovich, L.A., Livshits, V.B.: Conscript: specifying and enforcing fine-grained security policies for JavaScript in the browser. In: S&P, Oakland (2010). http:\/\/dx.doi.org\/10.1109\/SP.2010.36","DOI":"10.1109\/SP.2010.36"},{"key":"4_CR30","unstructured":"Morrisett, G., Felleisen, M., Harper, R.: Abstract models of memory management. In: FPCA (1995). http:\/\/doi.acm.org\/10.1145\/224164.224182"},{"key":"4_CR31","unstructured":"Nagarakatte, S., Zhao, J., Martin, M.M.K., Zdancewic, S.: SoftBound: highly compatible and complete spatial memory safety for C. In: PLDI (2009). http:\/\/repository.upenn.edu\/cgi\/viewcontent.cgi?article=1941&context=cis_reports"},{"key":"4_CR32","unstructured":"Nagarakatte, S., Zhao, J., Martin, M.M.K., Zdancewic, S.: CETS: compiler enforced temporal safety for C. In: ISMM (2010). http:\/\/acg.cis.upenn.edu\/papers\/ismm10_cets.pdf"},{"issue":"3","key":"4_CR33","doi-asserted-by":"publisher","first-page":"477","DOI":"10.1145\/1065887.1065892","volume":"27","author":"GC Necula","year":"2005","unstructured":"Necula, G.C., Condit, J., Harren, M., McPeak, S., Weimer, W.: CCured: type-safe retrofitting of legacy software. TOPLAS 27(3), 477\u2013526 (2005). https:\/\/doi.org\/10.1145\/1065887.1065892","journal-title":"TOPLAS"},{"key":"4_CR34","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139084673","volume-title":"Nominal Sets: Names and Symmetry in Computer Science","author":"AM Pitts","year":"2013","unstructured":"Pitts, A.M.: Nominal Sets: Names and Symmetry in Computer Science. Cambridge University Press, New York (2013)"},{"key":"4_CR35","doi-asserted-by":"crossref","unstructured":"Pottier, F., Protzenko, J.: Programming with permissions in Mezzo. In: ICFP (2013)","DOI":"10.1145\/2500365.2500598"},{"key":"4_CR36","unstructured":"Reynolds, J.C.: Separation logic: a logic for shared mutable data structures. In: LICS (2002). http:\/\/dl.acm.org\/citation.cfm?id=645683.664578"},{"key":"4_CR37","unstructured":"The Rust programming language (2017). http:\/\/www.rust-lang.org"},{"issue":"5","key":"4_CR38","doi-asserted-by":"publisher","first-page":"699","DOI":"10.3233\/JCS-140502","volume":"22","author":"C Schlesinger","year":"2014","unstructured":"Schlesinger, C., Pattabiraman, K., Swamy, N., Walker, D., Zorn, B.G.: Modular protections against non-control data attacks. JCS 22(5), 699\u2013742 (2014). https:\/\/doi.org\/10.3233\/JCS-140502","journal-title":"JCS"},{"key":"4_CR39","doi-asserted-by":"crossref","unstructured":"Smith, G.: On the foundations of quantitative information flow. In: FoSSaCS 2009. http:\/\/doi.org\/10.1007\/978-3-642-00596-1_21","DOI":"10.1007\/978-3-642-00596-1_21"},{"key":"4_CR40","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"718","DOI":"10.1007\/978-3-642-40203-6_40","volume-title":"Computer Security \u2013 ESORICS 2013","author":"D Stefan","year":"2013","unstructured":"Stefan, D., Buiras, P., Yang, E.Z., Levy, A., Terei, D., Russo, A., Mazi\u00e8res, D.: Eliminating cache-based timing attacks with instruction-based scheduling. In: Crampton, J., Jajodia, S., Mayes, K. (eds.) ESORICS 2013. LNCS, vol. 8134, pp. 718\u2013735. Springer, Heidelberg (2013). https:\/\/doi.org\/10.1007\/978-3-642-40203-6_40"},{"key":"4_CR41","doi-asserted-by":"crossref","unstructured":"Swamy, N., Hicks, M.W., Morrisett, G., Grossman, D., Jim, T.: Safe manual memory management in Cyclone. SCP 62(2), 122\u2013144 (2006). http:\/\/www.cs.umd.edu\/~mwh\/papers\/cyc-mm-scp.pdf","DOI":"10.1016\/j.scico.2006.02.003"},{"key":"4_CR42","doi-asserted-by":"crossref","unstructured":"Swasey, D., Garg, D., Dreyer, D.: Robust and compositional verification of object capability patterns. In: OOPSLA (2017, to appear). https:\/\/people.mpi-sws.org\/~swasey\/papers\/ocpl","DOI":"10.1145\/3133913"},{"key":"4_CR43","unstructured":"Szekeres, L., Payer, M., Wei, T., Song, D.: SoK: eternal war in memory. In: IEEE S&P (2013). http:\/\/lenx.100871.net\/papers\/War-oakland-CR.pdf"},{"key":"4_CR44","doi-asserted-by":"crossref","unstructured":"Taly, A., Erlingsson, \u00da., Mitchell, J.C., Miller, M.S., Nagra, J.: Automated analysis of security-critical JavaScript APIs. In: S&P, Oakland (2011). http:\/\/dx.doi.org\/10.1109\/SP.2011.39","DOI":"10.1109\/SP.2011.39"},{"key":"4_CR45","unstructured":"Turon, A.: Rust: from POPL to practice (keynote). In: POPL (2017). http:\/\/dl.acm.org\/citation.cfm?id=3011999"},{"key":"4_CR46","unstructured":"Williams, C.: Oracle\u2019s Larry Ellison claims his Sparc M7 chip is hacker-proof \u2013 errr... The Register (2015). http:\/\/www.theregister.co.uk\/2015\/10\/28\/oracle_sparc_m7\/"},{"key":"4_CR47","unstructured":"Yang, E.Z., Mazi\u00e8res, D.: Dynamic space limits for Haskell. In: PLDI (2014). http:\/\/doi.acm.org\/10.1145\/2594291.2594341"},{"key":"4_CR48","first-page":"402","volume-title":"Lecture Notes in Computer Science","author":"Hongseok Yang","year":"2002","unstructured":"Yang, H., O\u2019Hearn, P.W.: A semantic basis for local reasoning. In: FoSSaCS (2002). http:\/\/dl.acm.org\/citation.cfm?id=646794.704850"},{"key":"4_CR49","unstructured":"Zhang, D., Askarov, A., Myers, A.C.: Language-based control and mitigation of timing channels. In: PLDI (2012). http:\/\/doi.acm.org\/10.1145\/2254064.2254078"}],"container-title":["Lecture Notes in Computer Science","Principles of Security and Trust"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-89722-6_4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,15]],"date-time":"2019-10-15T15:20:15Z","timestamp":1571152815000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-89722-6_4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018]]},"ISBN":["9783319897219","9783319897226"],"references-count":49,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-89722-6_4","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2018]]}}}