Análisis de propiedades de seguridad y consumo acotado de memoria en un lenguaje funcional sin recolección de basura

Laburpena

La mayoría de lenguajes funcionales abstraen al programador del manejo de la memoria. Suelen disponer de un recolector de basura encargado de determinar, en tiempo de ejecución, qué partes de memoria ya no se necesitan y pueden ser liberadas. La principal ventaja de este enfoque es que los programadores no tienen que molestarse con asuntos relativos a la memoria. Sin embargo, este enfoque puramente implícito dificulta la tarea de predecir en tiempo de compilación los tiempos de vida en ejecución de las estructuras de datos. Por el contrario, otros lenguajes delegan completamente el manejo de la memoria en el programador. De este modo, se conoce en tiempo de compilación cuándo se liberan las estructuras de datos. No obstante, este enfoque es proclive a errores, ya que el programador puede, por error, tratar de acceder a zonas de memoria que han sido liberadas (punteros descolgados), debido a comparticiones inesperadas entre las estructuras de datos. Safe es un lenguaje funcional de primer orden que proporciona un enfoque semiexplícito al manejo de la memoria mediante dos mecanismos: regiones (inferidas por el compilador) y ajuste de patrones destructivo (controlado por el programador). De este modo se pretende prescindir de un recolector de basura para liberar las estructuras de datos que ya no se utilizan y, con ello, aumentar la predictibilidad en el uso de memoria por parte de los programas. Esto permitirá diseñar un análisis estático para inferir cotas superiores a la cantidad de memoria que un programa necesita para su ejecución. La incorporación de mecanismos explícitos de destrucción de memoria en un programa implica el riesgo de acceder a memoria ya liberada. El primer objetivo de la tesis es el desarrollo de un análisis para garantizar la seguridad de un programa con respecto a los accesos a memoria (en particular, la ausencia de punteros descolgados). Una vez que el compilador comprueba esta propiedad de seguridad para un programa concreto, el segundo objetivo es la formalización de dicha propiedad en forma de certificado, de modo que pueda ser comprobada automáticamente por el consumidor de dicho programa. Finalmente, se desarrollará un análisis basado en técnicas de interpretación abstracta para inferir cotas superiores al consumo de memoria de programas. Puesto que la meta final del proyecto Safe es la certificación de las propiedades de seguridad y consumo acotado de memoria, en esta tesis se ha puesto especial énfasis en la corrección formal de cada uno de los análisis expuestos. [ABSTRACT]In most functional languages, memory management is delegated to the runtime system. There usually exists a garbage collector in charge of determining, at runtime, which parts of the memory are no longer needed and can be disposed of. The main advantage of this approach is that programmers are not bothered about memory management issues. However, this purely implicit approach makes it difficult to predict, at compile time, the lifetimes of the data structures at runtime. Other languages delegate the task of memory management to the programmer. In this way, the lifetimes of data structures are known at compile time. However, this is an error-prone approach, since the programmer might try to access to memory areas which have been disposed of previously (dangling pointers), mainly due to unexpected sharing between data structures. Safe is a first-order functional language that provides a semiexplicit approach to memory management by means of two mechanisms: regions (inferred by the compiler), and destructive pattern matching (controlled by the programmer). In this way, we can do without a garbage collector to destroy the data structures that are no longer used. As a consequence, the behaviour of programs (regarding memory usage) becomes more predictable, and eases the task of developing a static analysis to infer upper bounds on the memory needs of a program. The incorporation of explicit mechanisms for memory destruction implies the risk of accessing dangling pointers. The first goal of this thesis is to develop a static analysis for guaranteeing the safety of a program with regard to its memory accesses (specifically, the absence of dangling pointers). Once the compiler has checked the presence of this property for a given program, our next goal is to formalize this property as a certificate, so the latter can be automatically checked by the code receiver. Finally, we will develop an abstract interpretation-based analysis for inferring upper bounds to the memory needs of a program. Since the final aim of the Safe project is the certification of pointer-safety properties and bounded memory execution, we have put emphasis on the formal correctness of each analysis.