Praktisk mjukvaruverifiering med formella metoder. Ett hjälpmedel i granskningsprocessen

Försvarsmaktens IT-system har ofta höga säkerhetskrav och det behövs därför hög tilltro till att systemen fungerar enligt specifikation. För att uppnå hög tilltro krävs ett noggrant verifieringsarbete. Verifiering av mjukvara är ett komplext problem där många olika metoder och verktyg måste samverka för att nå en hög tilltro till att mjukvaran är korrekt. Att mjukvaran är korrekt avseende både grundfunktionalitet och IT-säkerhetsfunktioner är avgörande när det kan påverka exempelvis personsäkerhet eller skyddsvärd information. För att med hög tilltro kunna uttala sig om mjukvarans kvalitet krävs i regel ett omfattande arbete där såväl specifikation som implementation måste undersökas på djupet. Denna rapport presenterar en studie som har undersökt hur verktyg som nyttjar formella metoder kan användas i praktiken vid verifiering av källkod. Arbetet har centrerats kring att verifiera några utvalda säkerhetsegenskaper, det vill säga enskilda aspekter av IT-säkerhetsfunktioner, baserat på två säkerhetsmål på hög nivå. Verifieringen har gjorts på källkod skriven i programspråket C där källkoden hör till en säkerhetskomponent vars funktion skulle kunna passa i många av Försvarsmaktens IT-system. Verktygen har en stor spännvidd i fråga om bevisförmåga, dvs. styrkan hos de resultat som produceras av verktygen. Bland de verktyg som har använts i denna studie syns även en koppling mellan utsagornas styrka och hur komplicerat det är att använda verktygen, där starkare bevis krävde större arbetsinsats. Verktygen som använts i studien nyttjar formella metoder som bedömdes lämpliga för verifieringsproblemet, är mogna och tillgängliga för användning samt är kopplade till supportfunktioner eller aktiva användarforum. Studiens slutsats är att användning av verktyg för verifiering med formella metoder på ett effektivt sätt kan ge ökad tilltro vid verifiering av säkerhetskritisk mjukvara. Det finns dock svårigheter med att använda sådana metoder enbart i granskningsfasen. Metoderna bör användas redan i utvecklingsstadiet när krav och kod kan anpassas. För att nå god effekt krävs lämplig metodik och kunnig personal. Såväl arbetsinsatsen som svårighetsgraden i användningen av verktygen anses vara hanterbara under dessa förutsättningar.