Protecting Functional Programs From Low-Level Attackers

Software systems are growing ever larger. Early software systems were singular units developed by small teams of programmers writing in the same programming language. Modern software systems, on the other hand, consist of numerous interoperating components written by different teams and in different programming languages. While this more modular and diversified approach to software development has enabled us to build ever larger and more complex software systems, it has, however, made it harder to ensure the reliability and security of software systems. In this thesis we study and remedy the security flaws that arise when attempting to resolve the difference in abstractions between components written in high-level functional programming languages and components written in imperative low-level programming languages. High-level functional programming languages, treat computation as the evaluation of mathematical functions. Low-level imperative programming languages, on the contrary, provide programmers with features that enable them to directly interact with the underlying hardware. While these features help programmers write more efficient software, they also make it easy to write malware through techniques such as buffer overflows and return oriented programming. Concretely, we develop new run-time approaches for protecting components written in functional programming languages from malicious components written in low-level programming languages by making using of an emerging memory isolation mechanism.This memory isolation mechanism is called the Protected Module Architecture (PMA). Informally, PMA isolates the code and data that reside within a certain area of memory by restricting access to that area based on the location of the program counter. We develop these run-time protection techniques that make use of PMA for three important areas where components written in functional programming languages are threatened by malicious low-level components: foreign function interfaces, abstract machines and compilation. In everyone of these three areas, we formally prove that our run-time protection techniques are indeed secure. In addtion to that we also provide implementations of our ideas through a fully functional compiler and a well-performing abstract machine