Title: On the Foundations of Practical Language-Based Security
Respondent: Maximilian Algehed
Opponent: Frank Piessens
Date & Time: June 8, 10:00 – 13:00
Link to thesis and to the online disputation
Abstract
Teoretiska Grundvalar för Praktiska IT-Säkerhetsverktyg
Moderna datorprogram är de mest komplexa artefakter som människan någonsin
har skapat. För att samhället ska kunna lita på att ingenjörer och programmerare
inte utsätter oss alla för stora risker med dessa komplexa system behöver vi
tillgång till verktyg som hjälper oss att förebygga säkerhetsluckor. Den här
avhandligen handlar om hur vi kan säkerställa att sådana verktyg faktiskt
fungerar och inte ger ett falskt intryck om säkerhet där ingen finns.
Verktyg av den här typen kan i grova tag uppdelas i två kategorier. I den första
kategorin faller verktyg som programmeraren använder under utvecklingstiden
för att hitta problem innan programmet färdigställts och i den andra kategorin
finner vi verktyg som agerar huvudsakligen efter att ett program redan användsi praktiken för att hindra säkerhetshål som inte upptäcks under utvecklingsperi-
oden från att skapa problem. I den här avhandlingen finns nya resultat för bådadessa kategorier av verktyg.
I den första kategorin bidrar den här avhandlingen med en ny metod för att
bevisa att programmeringsspråk kan garantera att alla program i språket är
säkra. I den andra kategorin bidrar den här avhandlingen med en ny förenande
teori och ett bevis att det inte existerar några perfekta mekanismer för att ge
säkerhet. Sammanfattningsvis ger den här avhandlingen stöd till inställningen att
datasäkerhet är någonting som bör finnas med från början i utvecklingsprocessen
då det är förhållandevis mer tekniskt komplicerat att anpassa system för att
uppnå datasäkerhet a posteriori.
Moderna datorprogram är de mest komplexa artefakter som människan någonsin
har skapat. För att samhället ska kunna lita på att ingenjörer och programmerare
inte utsätter oss alla för stora risker med dessa komplexa system behöver vi
tillgång till verktyg som hjälper oss att förebygga säkerhetsluckor. Den här
avhandligen handlar om hur vi kan säkerställa att sådana verktyg faktiskt
fungerar och inte ger ett falskt intryck om säkerhet där ingen finns.
Verktyg av den här typen kan i grova tag uppdelas i två kategorier. I den första
kategorin faller verktyg som programmeraren använder under utvecklingstiden
för att hitta problem innan programmet färdigställts och i den andra kategorin
finner vi verktyg som agerar huvudsakligen efter att ett program redan användsi praktiken för att hindra säkerhetshål som inte upptäcks under utvecklingsperi-
oden från att skapa problem. I den här avhandlingen finns nya resultat för bådadessa kategorier av verktyg.
I den första kategorin bidrar den här avhandlingen med en ny metod för att
bevisa att programmeringsspråk kan garantera att alla program i språket är
säkra. I den andra kategorin bidrar den här avhandlingen med en ny förenande
teori och ett bevis att det inte existerar några perfekta mekanismer för att ge
säkerhet. Sammanfattningsvis ger den här avhandlingen stöd till inställningen att
datasäkerhet är någonting som bör finnas med från början i utvecklingsprocessen
då det är förhållandevis mer tekniskt komplicerat att anpassa system för att
uppnå datasäkerhet a posteriori.