Static and dynamic countermeasures for implementation-level vulnerabilities.

Moderne programmeertalen zoals C++, C# en Java bieden diverse beschermingsfaciliteiten aan, zoals abstracte gegevenstypes, toegangsbeperkingen voor instantievelden en modulesystemen. Dergelijke abstracties zijn ontworpen om softwareontwerpprincipes te ondersteunen, zoals het afschermen van private informatie en de inkapseling van implementatieaspecten achter een publieke interface. Ze kunnen echter ook gebruikt worden voor het realiseren van beveiligingseigenschappen van computerprogramma's. Helaas gaan zulke eigenschappen typisch verloren bij het vertalen van de broncode van een programma naar machinetaal. Op broncodeniveau wordt bijvoorbeeld de toegang tot private instantievelden beperkt door het typesysteem van de programmeertaal, maar een dergelijke beperking bestaat niet op het niveau van de machinetaal. Dit kan ertoe leiden dat een vertaalde softwaremodule kwetsbaar is voor aanvallen op het niveau van de machinetaal, zoals code-injectieaanvallen en malware die zich in het besturingssysteem manifesteert.

In het eerste deel van dit proefschrift stellen we een vertalingsschema voor dat volledig abstract is, wat ruwweg betekent dat de vertaling de beveiligingseigenschappen die op broncodeniveau gelden behoudt tijdens het vertalingsproces. De definitie van volledige abstractie is gebaseerd op het behoud van contextuele equivalenties: twee softwaremodules mogen op machinetaalniveau enkel en alleen van elkaar te onderscheiden zijn door een derde module die met hen kan interageren, wanneer hun oorspronkelijke bronmodules ook van elkaar te onderscheiden zijn door een module op broncodeniveau. Een volledig abstracte vertaler zorgt ervoor dat elke mogelijke interactie op het niveau van de machinetaal uit te leggen is op het niveau van de brontaal. Deze eigenschap verzekert dat een aanvaller die zijn aanval mag schrijven in machinetaal niet krachtiger is dan een aanvaller die zijn code moet schrijven in een veilige hoog-niveau brontaal. Om deze sterke beveiligingseigenschap te verkrijgen, rekent ons vertalingsschema op de aanwezigheid van een beveiligingsprimitief in de doeltaal dat de toegang tot bepaalde geheugengebieden van een proces afschermt op basis van de waarde van de programmateller. De contributies van dit deel van het proefschrift bestaan uit het formuleren en formaliseren van het vertalingsschema, het bewijzen van de volledige abstractie van de vertaling, en het aantonen door middel van een prototype-implementatie dat het vereiste beveiligingsprimitief efficiënt realiseerbaar is op hedendaagse, alom beschikbare hardware.

In het tweede deel van dit proefschrift bespreken we hoe imperatieve programma's correct modulair geverifieerd kunnen worden, zelfs wanneer ze worden uitgevoerd in een ongeverifieerde omgeving. We richten ons op verificatiemethodes die gebaseerd zijn op Hoarelogica, dewelke ontwikkelaars toelaten om de correctheid van imperatieve programma's te bewijzen op basis van de programmabroncode. Helaas zijn de uitvoeringsgaranties van dergelijke methodes beperkt wanneer de geverifieerde code deel uitmaakt van een programma dat ook ongeverifieerde code bevat. Het is namelijk mogelijk dat de ongeverifieerde code zich niet gedraagt zoals aangenomen tijdens het verificatieproces, wat kan leiden tot het falen van eender welke assertie die gebaseerd is op die aannames. Dit is vooral problematisch bij geheugenonveilige programmeertalen zoals C, waarbij een geheugenfout in ongeverifieerde code de uitvoeringstoestand van geverifieerde code ongeldig kan maken.

Om dit probleem op te lossen, hebben we een reeks controles ontwikkeld die op de grens tussen de geverifieerde en ongeverifieerde code kunnen worden ingevoegd. Deze controles worden uitgevoerd bij elke functieoproep tussen geverifieerde en ongeverificeerde code en verzekeren dat de ongeverifieerde code zich gedraagt zoals aangenomen tijdens de verificatie. Een belangrijk probleem dat hierbij moet worden opgelost, is hoe de controles kunnen verzekeren dat geheugenfouten in het ongeverifieerde deel van het programma de uitvoeringstoestand van het geverifieerde deel niet kunnen beïnvloeden. We lossen dit probleem in twee stappen op. In de eerste stap zorgen we ervoor dat de ingevoegde controles de integriteit controleren van het heapgeheugen dat toegankelijk is voor de geverifieerde code. Hierdoor zullen ongeldige geheugenoperaties uitgevoerd door ongeverifieerde code gedetecteerd worden wanneer de geverifieerde code (terug) wordt binnengetreden. In de tweede stap gebruiken we de volledig abstracte vertaling die ontwikkeld werd in het eerste deel van dit proefschrift, om de lokale variabelen en besturingsstroominformatie van de geverifieerde code op de uitvoerstapel te beschermen. De combinatie van deze twee beschermingsmaatregelen resulteert in een zeer sterke modulaire correctheidsgarantie: geen enkele geverifieerde assertie in de geverifieerde code kan falen tijdens de uitvoering van het programma. De bijdragen van het tweede deel van het proefschrift bestaan uit het formuleren en formaliseren van de voorgestelde controles, het bewijzen dat deze controles correct en precies zijn, en het aantonen door middel van snelheidstesten dat de performantiekost van de controles voldoende laag is voor praktische toepasbaarheid.