Van veilige compilatie naar veilige abstractie, sterkere fundamenten en nieuwe linken

Vaak worden programma's uitgevoerd in een omgeving waar de abstracties tijdens de compilatie verloren zijn gegaan of ze worden geïmplementeerd in functie van low-level primitieven. Bijvoorbeeld, een besturingssysteem kan programma's inladen in gescheiden of overlappende regio's van het geheugen en kan dan door gebruik van multi-tasking en CPU-ondersteunde virtuele geheugen primitieven fictieve geïsoleerde uitvoering simuleren voor elk van de individuele processen. Als we dergelijke abstractie kunnen implementeren zodat het gespecifieerde gedrag behouden blijft in het bijzijn van aanvallers, dan noemen we dit veilige abstractie. De formele studie van veilige abstracties is het onderwerp van een onderzoeksveld binnen computerwetenschappen dat veilige compilatie heet. Ondanks de naam handelt dit veld over meer dan wat men traditioneel als een compiler aanschouwt. Dit veld is eigenlijk veel breder en wordt beter beschreven als de studie van veilige abstracties. In deze thesis zullen we bijdragen aan die veralgemeende visie van veilige compilatie door nieuwe linken te exploreren en te demonstreren en nieuwe toepassing te zoeken in nieuwe omstandigheden. In het bijzonder zullen we kijken naar onderzoeksvelden zoals cryptografie, language expressiveness en gradual typing, waar dit nieuwe perspectief tot nieuwe inzichten en technieken kan leiden.