Semi-automatische verificatie voor het verbeteren van softwareveiligheid

Verificatie van software heeft de potentie om de veiligheid van software drastisch te verbeteren. Om dit werkelijkheid te laten worden, moet het mogelijk zijn om belangrijke beveiligingseigenschappen van softwaresystemen te verifiëren tegen redelijke kosten en met hoge zekerheid. In deze thesis zullen we technieken onderzoeken om dergelijke verificatie haalbaar te maken: we zullen specifiek kijken naar het toepassen van (semi-)automatisering, hardware-ondersteunde compartimentering en veilige compilatie. Semi-automatische verificatie maakt het mogelijk om voor boilerplate en oninteressante delen van de verificatie automatisch een bewijs te leveren. Hardware-ondersteunde compartimentering maakt gebruik van de ondersteunde beveiligingsprimitieven aanwezig in de CPU (en andere hardware) om de hoeveelheid te verifiëren code te verminderen. Tenslotte maakt veilige compilatie het mogelijk betrouwbare software te bouwen in abstractere programmeertalen van een hoger niveau, met behoud van de veiligheidsgaranties in de meer concrete omgeving waarin ze wordt uitgevoerd.