Popular Science Summary
The growing adoption of software in every aspect of modern society, while enhancing productivity, has also opened up a lucrative attack surface for malicious actors to cause widescale societal damage. This stems from the fundamental design of our software stacks, which are constructed as a trusted tower of abstractions involving complex low-level software such as hypervisors, operating systems, firmware, drivers, etc. Attackers exploit a programmer’s trust in these bloated low-level software stacks to execute sophisticated attacks, compromising the safety and security of software running on the cloud and in embedded environments.
This dissertation addresses the fundamental issue of trust in software through a domain-specific functional programming language. The language employs a combination of specialised hardware isolation technologies and cryptographic techniques to eliminate the tower of low-level software abstractions from the programmer’s trusted code base, enabling software construction tailored for malicious cloud environments. Furthermore, in the realm of embedded systems, we introduce a high-level functional programming language and runtime, elevating the abstraction level at which these systems are programmed and significantly reducing common memory, type, and temporal- unsafety vulnerabilities. We hope that the contributions made through our dissertation will pave the way for further research avenues, where the robust security guarantees provided by our proposed functional languages can be integrated with emerging hardware and software-based security techniques to enable the construction of safer and more secure digital systems.