Tänk dig en framtid där du i ett projekt specificerar de säkerhetskritiska egenskaper som du vill att din nya mjukvara ska ha och vid leverans får du ett matematiskt bevis för att din nya mjukvara faktiskt lever upp till dina specifikationer.
Det finns en stark dragningskraft i att kunna bevisa att din mjukvara kommer fungera precis som det var tänkt.
I termer av säkerhet, både aspekterna ”safety” och ”security”, finns möjligheten att undvika oförutsedda och otestade specialfall och därmed leverera ökad trygghet och assurans.
Det kan också ge möjligheter till effektivisering och minskade kostnader för testning av mjukvaran.
Som forskningsområde är detta en gren av så kallade formella metoder och det gjordes mycket arbete redan på 70-talet för att hitta vägar till bevisbar säkerhet i en produkt. Tyvärr har det visat sig vara ett svårt att nyttja i praktiken och fallen där man lyckats med denna form av bevisning är få.
Ljus i tunneln
Nu kanske området går mot en ljusare framtid. Nyligen rapporterade nämligen den amerikanska forskningsorganisationen DARPA att ett ”Red-Team” av hackers efter sex veckors ihärdiga försök gått bet på att ta över ett styrsystem till en ”Quad-Copter”-leksak. Mjukvaran för drönaren hade byggts om av ett forskarteam på ett sätt som kunde bevisas vara säkert.
Kanske är detta ett led i vad som behövs i den allt mer besvärliga kampen att hålla våra IT- och OT-system säkra.
Läs gärna mer i den inspirerande artikeln på Quanta Magazine: https://www.quantamagazine.org/20160920-formal-verification-creates-hacker-proof-code/
