Formal Reasoning about Capability Machines

Lau Skorstengaard

Publikation: Bog/antologi/afhandling/rapportPh.d.-afhandling

215 Downloads (Pure)

Abstract

Næsten alle programmer er skrevet i højniveausprogrammeringssprog med abstraktioner, der gør, at programmører ikke behøver at bekymre sig om hardwaredetaljer. Computere kan dog ikke køre sådanne programmer, hvilket vi løser ved at oversætte dem til et lavniveausprogrammeringssprog, som computeren forstår. Umiddelbart lyder dette uskyldigt, men hvad sker der egentlig med højniveausabstraktionerne efter oversættelsen? Er de bibeholdt og hvis ikke betyder det noget for sikkerheden? Svaret er, groft sagt, at abstraktionerne ikke er bibeholdt, hvilket giver anledning til sikkerhedsbrister.
Eksempelvis er buffer overflow angreb og return oriented-programming angreb baseret på, at forventede højniveauabstraktioner ikke bibeholdes efter oversættelse.

Sikker oversættelse (i forskningsverdenen kendt som secure compilation) omhandler oversættelser, der bevarer sikkerhed efter oversættelse. Der er mange former for sikkerhed og ligeså mange former for sikker oversættelse. Full abstraction er en form for sikker oversættelse, der beviseligt bevarer abstraktioner - selv hvis programmet interagerer med ukendte ondsindede programmer. Dette er en meget stærk egenskab, som kun er opfyldt, hvis et oversat program håndhæve abstraktionerne. Der eksisterer i dag ikke nogen rigtig oversætter, som er fully abstract (der eksisterer oversættelser mellem legetøjsprogrammeringsprog, der beviseligt opfylder egenskaben).

Et problem, i forhold til at lave en sikker oversættelse, er, at vores computere ikke har tilstrækkelige sikkerhedsprimitiver til at håndhæve højniveausabstraktionerne. Hvis vi ønsker at have sikre computere, så bliver vi nødt til at gå væk fra den traditionelle computer over til en computer med flere sikkerhedsprimitiver, men hvilken? Et bud kunne være capability machines, hvilket er computere, der udskifter pointers med capabilities.
En capability er essentielt set en polet, der ikke kan blive forfalsket og som giver adgang til noget, eksempelvis at læse fra en del af hukommelsen.

I denne afhandling tager vi et stort skridt mod at lave en rigtig sikker oversætter ved at vise, hvordan capability machines kan udgøre grundlaget for sikker oversættelse. Vi viser, hvordan en håndfuld højniveausabstraktioner kan håndhæves på capability machines ved at bruge de ekstra sikkerhedsprimitiver. Vi giver tilmed matematiske beviser for, at abstraktionerne er håndhævet.
OriginalsprogEngelsk
ForlagAarhus University
Antal sider195
StatusUdgivet - nov. 2019

Fingeraftryk

Dyk ned i forskningsemnerne om 'Formal Reasoning about Capability Machines'. Sammen danner de et unikt fingeraftryk.

Citationsformater