Van veilige compilatie tot veilige abstractie: Sterkere fundamenten en nieuwe verbindingen.

Projectdetails

!!Description

Software engineering vergemakkelijkt de ontwikkeling, het onderhoud en de evolutie van complexe softwaresystemen door fundamenteel te vertrouwen op abstracties.
Dergelijke abstracties omvatten services van het besturingssysteem, hoog-niveauprogrammeertalen, herbruikbare bibliotheekcode enz.
Veel beveiligingsaanvallen maken echter essentieel gebruik van discrepanties tussen abstracte semantiek en semantiek op laag niveau van programma's.
Dit omvat bijvoorbeeld geheugenveiligheidsaanvallen (bijv. stack smashing), side channel-aanvallen (bijv.Spectre / Meltdown), fysieke aanvallen (bijv.Rowhammer) en vele andere (bijv. Symlink-races).

Tegelijkertijd worden sommige abstracties zo geïmplementeerd dat (een deel van) hun garanties blijven gelden in de low-level uitvoering.
Bedenk bijvoorbeeld hoe besturingssystemen virtueel geheugen gebruiken om procesisolatie te behouden bij het toepassen van preëmptieve multitasking.
Dergelijke veilige abstracties kunnen door programmeurs niet alleen worden gebruikt om te redeneren over correctheid van software, maar ook over beveiliging.
Ze werden voor het eerst bestudeerd in 1998 door Abadi en gekarakteriseerd door een eigenschap die volledige abstractie wordt genoemd.
Sindsdien is de eigenschap in veel contexten toegepast (beveiligde compilers, beveiligde linkers, veilige oproepconventies, veilige CPU-implementaties, afdwingen van contracten enz.) en verschillende generalisaties van de eigenschap zijn voorgesteld.

De doelstellingen van dit project zijn (1) het versterken van de fundamenten van veilige compilatie, en (2) het leggen en bestuderen van nieuwe verbindingen met verschillende vakgebieden.
Om (1) te bereiken, zullen we een nieuwe familie van karakterisaties van veilige compilatie voorstellen en bestuderen die (a) niet afhankelijk zijn van I/O-event traces, (b) belangrijke eigenschappen uit de literatuur generaliseren en (c) voldoende algemeen zijn voor de nieuwe toepassingen die we in dit project gaan ontwikkelen.
Voor (2) zullen we nieuwe verbanden leggen tussen veilige compilatie en (a) karakteriseringen van relatieve taalexpressiviteit, (b) handhaving van statische types in gradueel getypeerde talen en (c) cryptografie.
Korte titelSecure Abstractions
AcroniemAIIFUND63
StatusActief
Effectieve start/einddatum15/11/2014/11/25

Flemish discipline codes

  • Software engineering

Keywords

  • software engineering