< Terug naar vorige pagina

Project

Aantoonbaar behouden van veiligheidseigenschappen in aanwezigheid van aanvallers op een lager abstractieniveau

Onze moderne samenleving boogt in toenemende mate op computerapparaten voor haar goede werking. Met hun verhoogde aanwezigheid neemt ook het aantal interacties tussen verschillende softwarecomponenten toe. Om deze interacties te beveiligen en de impact van bug-exploits (zowel kwaadaardig als accidenteel van aard) te beperken, is een soort beveiligingsprimitief vereist om de interface tussen verschillende componenten te handhaven.

In dit proefschrift bestuderen we hardware capabilities als mogelijke oplossing voor dit probleem. Capabilities zijn pointers die inherent permissies bevatten, waarvan de grenzen door de hardware afgedwongen worden. Ze zijn een hardwareprimitief op assembleertaalniveau dat voorziet in een fijnkorrelige spatiale bescherming binnen componenten, en een efficiënte compartimentering tussen componenten. Ze worden al sinds de jaren 60 onderzocht, maar verkregen recent hernieuwde belangstelling dankzij het CHERI project aan de Universiteit van Cambridge.

Gezien hun weinig abstracte maar toch flexibele karakter is het moeilijk om correcte en veilige programma's te schrijven die capabilities manipuleren. Om dit probleem te verhelpen bestudeert dit proefschrift methoden om formeel te redeneren over de beveiliging die geboden wordt door capabilities. We leggen deze garanties vast in een vorm van algemeen veiligheidscontract voor een capability machine dat we een universeel contract noemen. Dit universele contract beschrijft hoe capabilities de macht van willekeurige, onvertrouwde code inperken. Het stelt ons bijgevolg in staat om te verifiëren of de concrete code van een applicatie aan bepaalde interessante eigenschappen voldoet, zelfs in de aanwezigheid van willekeurige onvertrouwde code.

De eerste bijdragen van dit proefschrift illustreren deze benadering in verscheidene situaties. We introduceren formele, gemechaniseerde modellen van verschillende capability machines die gebruik maken van universele contracten voor één taal om te redeneren over concrete assembleertaalcode.

Het eerste model, Cerise, illustreert hoe men kan redeneren over de spatiale bescherming en compartimentering die een doorsnee capability machine biedt. Om het model te illustreren verifiëren we een teller die afhankelijk is van de encapsulatie van zijn private state, en een calling conventie op de heap die gebruik maakt van dynamische geheugenallocatie. We verifiëren ook een voorbeeld van dynamisch sealen, wat illustreert dat hardware capabilities voldoende krachtig zijn om ontwerppatronen uit de literatuur over object capabilities op assembleertaalniveau te implementeren.

Vervolgens wordt ondersteuning voor effecten in de vorm van Memory-Mapped I/O (MMIO) toegevoegd aan het Cerise-model. De compartimentering die capabilities bieden wordt gebruikt om efficiënte, nestbare beveiligingswrappers rond I/O-apparaten te construeren. De wrappers maken het mogelijk om verschillende lagen van safety-eigenschappen voor het volledige systeem af te dwingen over de MMIO-traces van de capability machine. Interessant genoeg kunnen verschillende, gelaagde wrappers worden geverifieerd onder verschillende modellen van aanvallers, en de resultaten die worden verkregen door het verifiëren van lagen die zich dichter bij de hardware bevinden, kunnen worden hergebruikt bij het verifiëren van hogergelegen lagen. Deze nesting en de daaruit voortvloeiende mogelijkheden voor verificatie zijn moeilijk efficiënt te realiseren op hedendaagse standaardhardware. Om het model te illustreren verifiëren we twee voorbeelden in een systeem van wrappers bestaande uit drie lagen, waarbij elke laag de resultaten van de vorige hergebruikt en een verfijnder model beschouwt voor de aanvaller.

De laatste instantiatie van universele contracten waar we ons op richten, is het efficiënt ondersteunen van een vorm van enclaved executie bovenop capability hardware; een combinatie die nog niet eerder gerealiseerd was. Enclaved executie is een populair mechanisme voor het dynamisch creëren van Trusted Execution Environments (TEEs), ook wel enclaves genoemd. Enclaves zijn geïsoleerde uitvoeringscontexten die de integriteit en vertrouwelijkheid van software binnen de enclave beschermen (zelfs tegen gecompromitteerde systeemsoftware) en die ondersteuning bieden voor attestatie. We demonstreren een nieuw, bottom-up ontwerp voor flexibele enclaves bovenop een capability machine en presenteren drie verschillende implementaties van dit ontwerp, vergezeld van eenvoudige prestatiebenchmarks. Het bepalen van de juiste formele behandeling van enclaved executie als een universeel contract is lopend werk.

Redeneren over code op assembleertaalniveau is moeilijk en leidt dikwijls tot fouten. De laatste contributie van de thesis verlegt daarom de focus van redeneren op assembleertaalniveau (i.e., binnenin één taal) naar redeneren over veilige compilatie naar capability architecturen. Het standaardcriterium van full abstraction wordt gebruikt om veilige compilatie te instantiëren, en een compiler van C-achtige code die in separation logic geverifieerd is, naar C-achtige code met ondersteuning voor zogenaamde lineaire capabilities (een niet-dupliceerbaar type capabilities), wordt fully abstract bewezen. De intuïtie achter de compiler is dat de lineaire separation logic resources kunnen worden gereïficeerd en gerepresenteerd door lineaire capabilities in de targettaal. Het full abstractionbewijs impliceert ruwweg dat aanvallen die mogelijk zijn op targettaalniveau in de capability architectuur al mogelijk moeten zijn geweest op het geverifieerde brontaalniveau, i.e. de compiler creëerde geen extra veiligheidsproblemen die niet ook al aanwezig waren op het brontaalniveau. Op de lange termijn is de hoop om een vorm van graduele verificatie te ondersteunen, waarbij delen van codebases in C die kritiek zijn voor de veiligheid kunnen worden geverifieerd en gecompileerd met deze compiler, zodanig dat veiligheidsgaranties kunnen worden afgedwongen in aanwezigheid van buggy of onvertrouwde code.

Datum:20 sep 2017 →  15 jul 2022
Trefwoorden:Linear Capbilities
Disciplines:Toegepaste wiskunde, Computerarchitectuur en -netwerken, Distributed computing, Informatiewetenschappen, Informatiesystemen, Programmeertalen, Scientific computing, Theoretische informatica, Visual computing, Andere informatie- en computerwetenschappen
Project type:PhD project