Porcelain: A Semantic Framework for Representing and Analyzing Memory Safety Techniques
Resumo
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.
Palavras-chave:
Memory Safety, Rust, Cyclone, Checked C
Referências
Samson Abramsky. 1993. Computational interpretations of linear logic. Theor. Comput. Sci. 111, 1–2 (April 1993), 3–57. DOI: 10.1016/0304-3975(93)90181-R
Security Research Apple. 2022. Towards the next generation of XNU memory safety: kalloc_type. Apple. Retrieved June 14, 2025 from [link]
Content Team CWE. 2023. CWE CATEGORY: Comprehensive Categorization: Memory Safety. MITRE. Retrieved June 14, 2025 from [link]
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
Graham Hutton. 2016. Programming in Haskell (2nd ed.). Cambridge University Press, USA.
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 ’02). USENIX Association, USA, 275–288.
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
Brian W. Kernighan and Dennis M. Ritchie. 1988. The C Programming Language (2nd ed.). Prentice Hall Professional Technical Reference.
Steve Klabnik and Carol Nichols. 2018. The Rust Programming Language. No Starch Press, USA.
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’24). USENIX Association, USA, Article 27, 19 pages.
Niko Matsakis. 2018. An alias-based formulation of the borrow checker. [link]
John McCarthy. 1960. Recursive functions of symbolic expressions and their computation by machine, Part I. Commun. ACM 3, 4 (April 1960), 184–195. DOI: 10.1145/367177.367199
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–526. DOI: 10.1145/1065887.1065892
Alex Rebert and Christoph Kern. 2024. Secure by Design: Google’s Perspective on Memory Safety. Google Security Engineering Technical Report. Google.
Amanda Stjerna. 2020. Modelling Rust’s Reference Ownership Analysis Declaratively in Datalog. Master’s thesis. Uppsala University, Department of Information Technology.
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–60. [link]
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–265. DOI: 10.1023/B:LISP.0000029446.78563.a4
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–84.
Philip Wadler. 1990. Linear Types can Change the World!. In Programming Concepts and Methods. [link]
NienkeWessel. 2019. The Semantics of Ownership and Borrowing in the Rust Programming Language. Bachelor’s Thesis. Radboud University.
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
Security Research Apple. 2022. Towards the next generation of XNU memory safety: kalloc_type. Apple. Retrieved June 14, 2025 from [link]
Content Team CWE. 2023. CWE CATEGORY: Comprehensive Categorization: Memory Safety. MITRE. Retrieved June 14, 2025 from [link]
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
Graham Hutton. 2016. Programming in Haskell (2nd ed.). Cambridge University Press, USA.
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 ’02). USENIX Association, USA, 275–288.
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
Brian W. Kernighan and Dennis M. Ritchie. 1988. The C Programming Language (2nd ed.). Prentice Hall Professional Technical Reference.
Steve Klabnik and Carol Nichols. 2018. The Rust Programming Language. No Starch Press, USA.
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’24). USENIX Association, USA, Article 27, 19 pages.
Niko Matsakis. 2018. An alias-based formulation of the borrow checker. [link]
John McCarthy. 1960. Recursive functions of symbolic expressions and their computation by machine, Part I. Commun. ACM 3, 4 (April 1960), 184–195. DOI: 10.1145/367177.367199
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–526. DOI: 10.1145/1065887.1065892
Alex Rebert and Christoph Kern. 2024. Secure by Design: Google’s Perspective on Memory Safety. Google Security Engineering Technical Report. Google.
Amanda Stjerna. 2020. Modelling Rust’s Reference Ownership Analysis Declaratively in Datalog. Master’s thesis. Uppsala University, Department of Information Technology.
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–60. [link]
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–265. DOI: 10.1023/B:LISP.0000029446.78563.a4
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–84.
Philip Wadler. 1990. Linear Types can Change the World!. In Programming Concepts and Methods. [link]
NienkeWessel. 2019. The Semantics of Ownership and Borrowing in the Rust Programming Language. Bachelor’s Thesis. Radboud University.
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
Publicado
22/09/2025
Como Citar
COLLE, Pedro Henrique Boniatti; MACHADO, Rodrigo.
Porcelain: A Semantic Framework for Representing and Analyzing Memory Safety Techniques. In: SIMPÓSIO BRASILEIRO DE LINGUAGENS DE PROGRAMAÇÃO (SBLP), 29. , 2025, Recife/PE.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2025
.
p. 93-96.
DOI: https://doi.org/10.5753/sblp.2025.10677.
