< Terug naar vorige pagina
Project
ERC-Opvangmandaat: Laag-niveau objectmogelijkheden, formeel (FWOAL910)
Object capabilities (ocaps) zijn een techniek voor fijnmazige scheiding van privileges in programmeertalen, met toepassingen in beveiliging en software-engineering. Ocaps worden praktisch gebruikt in hoog-niveau programmeertalen, zoals JavaScript, maar recent is er ook een hernieuwde belangstelling voor capability machines: processors die ocaps toepassen op het lage niveau van assembleertalen (lowcaps). Beveiligingsmaatregelen gebaseerd op lowcaps bieden het perspectief van efficiënte maar waterdichte afweer tegen realistische aanvallers, met bescherming tegen willekeurige aanvallen, niet alleen aanvallen die we al kennen.
Zulke maatregelen beloven een einde te maken aan de aanvals-verdedigingswapenwedloop die veel bestaande maatregelen plaagt. In dit onderzoeksproject probeer ik dit potentieel te valideren en aan te tonen, evenals het wetenschappelijke begrip van ocaps in het algemeen te verdiepen.
Om dit doel te bereiken, gaat dit project ervan uit dat een lowcaps assembleertaal gewoon een speciaal soort programmeertaal is, die kan worden bestudeerd met behulp van krachtige technieken die zijn ontwikkeld voor hoog-niveau-programmeertalen, met name logische relaties en programmalogica. Met deze methodologie ben ik van plan nieuwe lowcaps beveiligingsmaatregelen voor te stellen, te bestuderen en te implementeren en hun effectiviteit rigoureus te bewijzen. Aan de andere kant ben ik ook van plan om effectparametriciteit verder te bestuderen: een algemene eigenschap die ik eerder voorgesteld heb om de essentie van ocaps formeel vast te leggen. Ik ben van plan deze eigenschap in verschillende contexten te bestuderen en toe te passen: voor modulair redeneren over ocap en lowcap-code, maar ook in de context van functionele en dependently-typed programmeertalen, voor een aantal verschillende doeleinden.
De resultaten van dit project zullen variëren van nieuwe, aantoonbaar correcte veiligheidsmaatregelen die zijn gebaseerd op low-caps, nieuwe redeneermethoden voor dergelijke maatregelen, maar ook nieuwe inzichten over de aard van ocaps, de relatie tussen objectgerichte en functionele programmeren en het gebruik van effectparametriciteit in bewijsassistenten.
Zulke maatregelen beloven een einde te maken aan de aanvals-verdedigingswapenwedloop die veel bestaande maatregelen plaagt. In dit onderzoeksproject probeer ik dit potentieel te valideren en aan te tonen, evenals het wetenschappelijke begrip van ocaps in het algemeen te verdiepen.
Om dit doel te bereiken, gaat dit project ervan uit dat een lowcaps assembleertaal gewoon een speciaal soort programmeertaal is, die kan worden bestudeerd met behulp van krachtige technieken die zijn ontwikkeld voor hoog-niveau-programmeertalen, met name logische relaties en programmalogica. Met deze methodologie ben ik van plan nieuwe lowcaps beveiligingsmaatregelen voor te stellen, te bestuderen en te implementeren en hun effectiviteit rigoureus te bewijzen. Aan de andere kant ben ik ook van plan om effectparametriciteit verder te bestuderen: een algemene eigenschap die ik eerder voorgesteld heb om de essentie van ocaps formeel vast te leggen. Ik ben van plan deze eigenschap in verschillende contexten te bestuderen en toe te passen: voor modulair redeneren over ocap en lowcap-code, maar ook in de context van functionele en dependently-typed programmeertalen, voor een aantal verschillende doeleinden.
De resultaten van dit project zullen variëren van nieuwe, aantoonbaar correcte veiligheidsmaatregelen die zijn gebaseerd op low-caps, nieuwe redeneermethoden voor dergelijke maatregelen, maar ook nieuwe inzichten over de aard van ocaps, de relatie tussen objectgerichte en functionele programmeren en het gebruik van effectparametriciteit in bewijsassistenten.
Datum:1 feb 2019 → 1 okt 2021
Trefwoorden:Software
Disciplines:Andere computer ingenieurswetenschappen, informatietechnologie en mathematische ingenieurswetenschappen niet elders geclassificeerd