Composec: Hvordan bevarer man IT-sikkerhed når IT-applikationer kombineres?
Hver dag bruger vi internetprotokoller som NemID og ”https” (TLS). Selvom disse protokoller efterhånden er blevet undersøgt ganske detaljeret, er det stadigt uklart, om de er sikre, når de kombineres. Ligesom harmløse kemikalier kan reagere og blive giftige, kan kombinationen af sikre komponenter give et usikkert system. I Composec projektet undersøger vi under hvilke betingelser, vi kan give et matematisk bevis for, at det samlede system er sikkert. Vi udvikler også et program, der automatisk kan afgøre, om en given kombination overholder betingelserne, så softwareudviklere hurtigt kan finde svaghederne i deres systemer, og når de er afhjulpet, garantere IT-sikkerheden af det samlede system.
IT-sikkerhed er et uhyre spændende og udfordrende område, hvor man kan skifte mellem at tænke som angriber (hvordan ødelægger vi systemet?) og forsvarer (hvordan kan vi proaktivt undgå angreb?). Jeg er især blevet fascineret af, hvordan man automatisk dels kan finde svagheder, dels kan vise, at der ingen er. Den videnskabelige ambition er at bygge systemer, der er sikre ikke bare mod den form for angreb, som vi kender i dag, men også mod nye former for angreb, der måtte opstå i fremtiden. Det er en stor tilfredsstillelse at se, at både virksomheder og samfund drager nytte af vores forskning: Sammen med kolleger har jeg været i stand til af at finde og rette adskillige fejl i internetprotokoller.
Den væsentlige udfordring ligger i at finde de rigtige betingelser til at garantere IT-sikkerheden i et samlet system: På den ene side skal de være stærke nok til, at vi kan lave et matematisk bevis, på den anden side skal de være tilstrækkeligt anvendelige til at kunne håndtere typiske internetapplikationer. Det ville være let nok at bevise korrektheden af meget restriktive betingelser, men det svarer lidt til at sige “hvis internettet havde været lavet anderledes, ville det have været sikkert.” Vores mål er at finde betingelser, der kan bruges i praksis. Målet er at lave et bibliotek med komponenter, som bevisligt kan kombineres, uden at sætte IT-sikkerheden over styr. Det skal være muligt for alle at tilføje komponenter til dette bibliotek, hvis de accepteres af vore automatiske analyser. En internetudvikler, der kun bruger komponenter fra biblioteket, kan derfor være fuldstændigt sikker på, at IT-sikkerheden bevares.
Jeg kan sagtens arbejde alene, men jeg kan endnu bedre lide at arbejde sammen med andre forskere. Jeg synes specielt, at det er spændende at arbejde med fremragende studerende, som selv kan tænke, og som gerne vil være forskere og få en ph.d.-grad. Sapere Aude-bevillingen giver mig mulighed for at få to ph.d.-studerende, og vi kan arbejde sammen med stor forskningsmæssig frihed. Bevillingen giver mig også mulighed for at arbejde sammen med andre forskere og at prøve resultaterne af sammen med relevante virksomheder. Det er en uvurderlig hjælp til at bygge en lille forskningsgruppe og udbygge forbindelserne til andre. Og så er det selvfølgelig en stor ære at modtage en Sapere Aude-bevilling.
Jeg er opvokset i Freiburg i Tyskland, hvor jeg gik i sprogligt gymnasium og derefter på universitetet. Jeg tog en ph.d. ved ETH Zürich med speciale i datalogi og IT-sikkerhed, og jeg var postdoc ved IBM forskningslaboratoriet i Zürich, indtil jeg fik en adjunktstilling på Danmarks Tekniske Universitet.
I min fritid spiller jeg klaver, ser film eller går i teatret. Jeg kan godt lide gamle ting og sager: Bøger, grafik, slotte og fly (jeg har dog ikke så mange af de sidste to).
Danmarks Tekniske Universitet, DTU Compute - Institut for Matematik og Computer Science
Datalogi, matematisk logik, IT-sikkerhed
Lyngby
Det humanistiske Friedrich-Gymnasium Freiburg