Porcelain : um framework semântico para representar e analisar técnicas de segurança de memória

Abstract

A linguagem de programação C é a fundação de programação de sistemas. No começo do milênio, Cyclone iniciou o movimento de linguagens de baixo nível com segurança no acesso à memória, com o fim de gerar sistemas sem as comuns vulnerabilidades de memória de C. Nos anos seguintes, mais e mais linguagens foram surgindo, cada uma com uma nova estratégia de gerência de memória. É importante validar a corretude de cada uma dessas estratégias, porém a prova delas fica normalmente restringida ao domínio da linguagem, dificultando a análise do panorama. Dessa forma, este trabalho introduz Porcelain: um framework semântico para representar e analisar técnicas de segurança de memória. Ele é composto de duas partes: uma linguagem back-end definida, modelada para detectar e classificar falhas de memória; e uma linguagem de front-end com alguma técnica que se deseja provar via compilação para a linguagem base de back-end. A técnica de segurança de memória escolhida para se implementar neste trabalho é um Borrow Checker, inspirado em Rust e no sistema de alias de Cyclone. As definições apresentadas neste trabalho permitem a especificação e o estudo formal da correção dos mecanismos de segurança de memória implementados em PCLfront.

The Cprogramming language is the foundation of systems programming. At the beginning of the millennium, Cyclone initiated the movement of low-level languages with memory safety, aiming to build systems free from the common memory vulnerabilities of C. In the following years, more and more languages emerged, each with its own memory management strategy. It is important to validate the correctness of each of these strategies; however, their proofs are usually restricted to the domain of the language itself, hindering a broader analysis. Therefore, this work introduces Porcelain: a semantic framework for representing and analyzing memory safety techniques. It consists of two parts: a defined back-end language, designed to detect and classify memory faults; and a front-end language implementing a technique to be verified via compilation to the base back-end language. The memory safety technique chosen for implementation in this work is a borrow checker, inspired by Rust and Cyclone’s alias system. The definitions presented in this work allow the specification and formal study of the correctness of the memory safety mechanisms implemented in PCLfront.