Octopi är ett forskningsprojekt som genomförs av Chalmers och finansieras av SSF, vars syfte är att skapa en miljö i vilken säkra Internet of Things för industrin kan utvecklas. Behovet efter den här typen av lösningar är stort.
Internet of Things (IoT) har i dag en stor och självklar plats i våra liv: allt från smarta tv-apparater till digitala lås på dörrar, mobiler, självkörande bilar och air conditions. Med andra ord, alla de enheter och produkter som är uppkopplade mot internet på ett eller annat sätt.
– IoT kan upplevas som smart och bekvämt men tyvärr har det en akilleshäl, och det är säkerheten. Jag brukar jämföra IoT med de första datorerna som kom på 1970-talet – säkerheten är helt eftersatt och det är något som måste åtgärdas snarast, annars kommer det få förödande konsekvenser, säger Carl-Johan Seger.
Carl-Johan Seger är professor i datorvetenskap och arbetar sedan tre år tillbaka som WASP-professor (Wallenberg Artificial Intelligence, Autonomous Systems and Software Program) på Chalmers – det universitet där han också påbörjade sina studier 1981.
– I dag är jag tillbaka på Chalmers efter nästan 34 år i Kanada, USA och Storbritannien. Just nu arbetar jag tillsammans med fyra andra professorer i projektet Octopi, vars vision är att göra IoT säkrare eftersom vårt samhälle blir allt mer sårbart för attacker när fler och fler enheter kopplas samman via internet, säger Carl-Johan Seger.
Traditionellt är mjukvaran för IoT-enheter programmerad på ett lågnivåspråk – ett språk som är ökänt för att små misstag av programmerare kan öppna upp för farliga säkerhetsproblem. Fokuset i Octopi projektet är att byta till ett högnivåspråk.
– Men, det handlar inte bara om att möjliggöra en bättre och säkrare mjukvara. Tyvärr har det nyligen visat sig – till exempel efter Specter- och Meltdown-attackerna – att det finns mycket allvarliga säkerhetsproblem även i själva hårdvaran. Därför utvecklar vi också en ny typ av mikroprocesser som är skräddarsydda för IoT-enheter som använder högnivåspråk, säger Carl-Johan Seger.
Han berättar att man måste kunna garantera att själva processorn är säker i sig själv, för att arbetet ska bli meningsfullt, och att Octopis strategi är att formellt verifiera sin egen design:
– Med andra ord strävar vi efter att tillhandhålla ett matematiskt bevis på att den IoT-processor som vi utvecklar också kommer att vara korrekt, utan vare sig sidokanaler eller andra säkerhetsproblem. För att uppnå det kommer vi att använda ett formellt verifieringssystem som kallas Voss II och som nyligen hade sin första open-source-release.
Voss II är baserad på Voss-systemet, som Carl-Johan Seger skapade för nästan 30 år sedan och som låg till grund för det formella verifieringssystemet som än i dag används av Intel.
– Voss II har införlivat min 20 års erfarenhet från Intel i att utveckla och distribuera formella verifieringsverktyg. Nu skapar vi ett modernt formellt verifieringssystem som gör att resten av Octopi-projektet kan bygga på en solid grund, säger Carl-Johan Seger och avslutar:
– Vår vision är att vi ska utveckla något som industrin kan ta tillvara, man skulle kunna kalla det för en legobit, som möjliggör utvecklingen av säkra IoT-enheter som vi kan lita på och som kan minimera efterkommande problem. Jag hade en chef på Intel som brukade säga att ”only the paranoids survives” och det ligger rätt mycket i det.