{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T12:40:37Z","timestamp":1760013637784,"version":"build-2065373602"},"reference-count":21,"publisher":"Sociedade Brasileira de Computa\u00e7\u00e3o","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"At the start of the millennium, the Cyclone language was developed as a solution to the memory safety shortcomings of the C language. Since then, many programming languages have emerged with their own memory safety strategies. But how can we validate those strategies? This paper proposes Porcelain: a semantic framework for representing and analyzing memory safety techniques. Introducing its definitions, use cases, and limitations whilst giving an overview of the current and future work.<\/jats:p>","DOI":"10.5753\/sblp.2025.10677","type":"proceedings-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T12:13:46Z","timestamp":1760012026000},"page":"93-96","source":"Crossref","is-referenced-by-count":0,"title":["Porcelain: A Semantic Framework for Representing and Analyzing Memory Safety Techniques"],"prefix":"10.5753","author":[{"given":"Pedro Henrique Boniatti","family":"Colle","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Rodrigo","family":"Machado","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"3742","published-online":{"date-parts":[[2025,9,22]]},"reference":[{"key":"1","doi-asserted-by":"crossref","unstructured":"Samson Abramsky. 1993. Computational interpretations of linear logic. Theor. Comput. Sci. 111, 1\u20132 (April 1993), 3\u201357. DOI: 10.1016\/0304-3975(93)90181-R<\/a>","DOI":"10.1016\/0304-3975(93)90181-R"},{"key":"2","unstructured":"Security Research Apple. 2022. Towards the next generation of XNU memory safety: kalloc_type. Apple. Retrieved June 14, 2025 from [link]<\/a>"},{"key":"3","unstructured":"Content Team CWE. 2023. CWE CATEGORY: Comprehensive Categorization: Memory Safety. MITRE. Retrieved June 14, 2025 from [link]<\/a>"},{"key":"4","doi-asserted-by":"crossref","unstructured":"Son Ho, Aymeric Fromherz, and Jonathan Protzenko. 2024. Sound Borrow-Checking for Rust via Symbolic Semantics. Proc. ACMProgram. Lang. 8, ICFP, Article 251 (Aug. 2024), 29 pages. DOI: 10.1145\/3674640<\/a>","DOI":"10.1145\/3674640"},{"key":"5","doi-asserted-by":"crossref","unstructured":"Graham Hutton. 2016. Programming in Haskell (2nd ed.). Cambridge University Press, USA.","DOI":"10.1017\/CBO9781316784099"},{"key":"6","unstructured":"Trevor Jim, J. Greg Morrisett, Dan Grossman, MichaelW. Hicks, James Cheney, and Yanling Wang. 2002. Cyclone: A Safe Dialect of C. In Proceedings of the General Track of the Annual Conference on USENIX Annual Technical Conference (ATEC \u201902). USENIX Association, USA, 275\u2013288."},{"key":"7","doi-asserted-by":"crossref","unstructured":"Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, and Derek Dreyer. 2017. RustBelt: securing the foundations of the Rust programming language. Proc. ACM Program. Lang. 2, POPL, Article 66 (Dec. 2017), 34 pages. DOI: 10.1145\/3158154<\/a>","DOI":"10.1145\/3158154"},{"key":"8","unstructured":"Brian W. Kernighan and Dennis M. Ritchie. 1988. The C Programming Language (2nd ed.). Prentice Hall Professional Technical Reference."},{"key":"9","unstructured":"Steve Klabnik and Carol Nichols. 2018. The Rust Programming Language. No Starch Press, USA."},{"key":"10","unstructured":"Hongyu Li, Liwei Guo, Yexuan Yang, ShangguangWang, and Mengwei Xu. 2024. An empirical study of rust-for-Linux: the success, dissatisfaction, and compromise. In Proceedings of the 2024 USENIX Conference on Usenix Annual Technical Conference (Santa Clara, CA, USA) (USENIX ATC\u201924). USENIX Association, USA, Article 27, 19 pages."},{"key":"11","unstructured":"Niko Matsakis. 2018. An alias-based formulation of the borrow checker. [link]<\/a>"},{"key":"12","doi-asserted-by":"crossref","unstructured":"John McCarthy. 1960. Recursive functions of symbolic expressions and their computation by machine, Part I. Commun. ACM 3, 4 (April 1960), 184\u2013195. DOI: 10.1145\/367177.367199<\/a>","DOI":"10.1145\/367177.367199"},{"key":"13","doi-asserted-by":"crossref","unstructured":"George C. Necula, Jeremy Condit, Matthew Harren, Scott McPeak, and Westley Weimer. 2005. CCured: type-safe retrofitting of legacy software. ACM Trans. Program. Lang. Syst. 27, 3 (May 2005), 477\u2013526. DOI: 10.1145\/1065887.1065892<\/a>","DOI":"10.1145\/1065887.1065892"},{"key":"14","unstructured":"Alex Rebert and Christoph Kern. 2024. Secure by Design: Google\u2019s Perspective on Memory Safety. Google Security Engineering Technical Report. Google."},{"key":"15","unstructured":"Amanda Stjerna. 2020. Modelling Rust\u2019s Reference Ownership Analysis Declaratively in Datalog. Master\u2019s thesis. Uppsala University, Department of Information Technology."},{"key":"16","doi-asserted-by":"crossref","unstructured":"David Tarditi, Archibald Samuel Elliott, Andrew Ruef, and Michael Hicks. 2018. Checked C: Making C Safe by Extension. In IEEE Cybersecurity Development Conference 2018 (SecDev). IEEE, 53\u201360. [link]<\/a>","DOI":"10.1109\/SecDev.2018.00015"},{"key":"17","doi-asserted-by":"crossref","unstructured":"Mads Tofte, Lars Birkedal, Martin Elsman, and Niels Hallenberg. 2004. A Retrospective on Region-Based Memory Management. Higher-Order and Symbolic Computation 17 (09 2004), 245\u2013265. DOI: 10.1023\/B:LISP.0000029446.78563.a4<\/a>","DOI":"10.1023\/B:LISP.0000029446.78563.a4"},{"key":"18","doi-asserted-by":"crossref","unstructured":"Katrina Tsipenyuk, Brian Chess, and Gary McGraw. 2005. Seven Pernicious Kingdoms: A Taxonomy of Software Security Errors. IEEE Security and Privacy 3, 6 (Nov. 2005), 81\u201384.","DOI":"10.1109\/MSP.2005.159"},{"key":"19","unstructured":"Philip Wadler. 1990. Linear Types can Change the World!. In Programming Concepts and Methods. [link]<\/a>"},{"key":"20","unstructured":"NienkeWessel. 2019. The Semantics of Ownership and Borrowing in the Rust Programming Language. Bachelor\u2019s Thesis. Radboud University."},{"key":"21","doi-asserted-by":"crossref","unstructured":"Jie Zhou, John Criswell, and Michael Hicks. 2023. Fat Pointers for Temporal Memory Safety of C. Proc. ACM Program. Lang. 7, OOPSLA1, Article 86 (April 2023), 32 pages. DOI: 10.1145\/3586038<\/a>","DOI":"10.1145\/3586038"}],"event":{"name":"Simp\u00f3sio Brasileiro de Linguagens de Programa\u00e7\u00e3o","location":"Brasil","acronym":"SBLP 2025","number":"29"},"container-title":["Anais do XXIX Simp\u00f3sio Brasileiro de Linguagens de Programa\u00e7\u00e3o (SBLP 2025)"],"original-title":[],"link":[{"URL":"https:\/\/sol.sbc.org.br\/index.php\/sblp\/article\/download\/36953\/36738","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/sol.sbc.org.br\/index.php\/sblp\/article\/download\/36953\/36738","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T12:13:53Z","timestamp":1760012033000},"score":1,"resource":{"primary":{"URL":"https:\/\/sol.sbc.org.br\/index.php\/sblp\/article\/view\/36953"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,9,22]]},"references-count":21,"URL":"https:\/\/doi.org\/10.5753\/sblp.2025.10677","relation":{},"subject":[],"published":{"date-parts":[[2025,9,22]]}}}