Formella metoder för säkerhet

Kursen kan ingå i följande program:

1. Computer Science, masterprogram (N2COS)

En kandidatexamen i datavetenskap eller ett relaterat ämnesområde.

Formella metoder är matematiska tekniker för specifikation, design och verifiering av mjukvaru- och hårdvarusystem. I säkerhetssammanhang tillhandahåller formella metoder rigorösa verktyg för att modellera och analysera system med avseende på potentiella sårbarheter samt för att säkerställa efterlevnad av säkerhetspolicys. Dessa metoder möjliggör en exakt definition av säkerhetsegenskaper och tillåter automatiserad verifiering för att upptäcka brister som kan förbises vid traditionell testning. Genom att tillämpa formella tekniker såsom modellkontroll, satsbevisning och formella specifikationsspråk kan utvecklare bygga system med bevisbara säkerhetsgarantier. Kursen består av en serie föreläsningar om olika formalism och verifieringsmetoder som har utvecklats för att resonera kring säkerhets- och sekretessegenskaper.

Efter godkänd kurs ska studenten kunna:

Kunskap och förståelse

• Förklara formella metoders roll vid specificering och verifiering av säkerhetskritiska system.

Färdigheter och förmåga

• Formellt definiera och resonera kring centrala säkerhets- och integritetsegenskaper med hjälp av formella specifikationsspråk.
• Använda automatiserade verifieringsverktyg för att verifiera efterlevnad av säkerhetspolicyer och identifiera potentiella sårbarheter

Värderingsförmåga och förhållningssätt

• Utvärdera kritiskt styrkor och begränsningar hos olika formella tekniker.

Kursen inkluderar föreläsningar och en projektkomponent. Föreläsningarna innehåller en obligatorisk del: att delta i quiz. Projektarbetet innebär att implementera och experimentera med ämnen relaterade till de koncept som introduceras i kursen. Att genomföra och presentera projektet, skriva en rapport samt delta i en kodgranskningssession är obligatoriskt.

Undervisningsspråk: engelska

För att klara kursen krävs:

1. Att klara quiz
2. Ett godtagbart individuellt bidrag till projektet, inklusive:
   • Implementering
   • Presentation
   • Kodgranskning på plats
   • Inlämning av skriftlig rapport som dokumenterar projektet"

Om en student som har underkänts två gånger på samma examinerande moment önskar byta examinator inför nästa examinationstillfälle ska en sådan begäran bifallas om det inte finns särskilda skäl däremot (6 kap. 22 § HF).

Om en student har fått besked om pedagogiskt stöd från Göteborgs universitet med rekommendation om anpassad examination och/eller anpassad examinationsform kan examinator, i det fall det är förenligt med kursens lärandemål och förutsatt att inte orimliga resurser krävs, besluta att bevilja studenten anpassad examination och/eller anpassad examinationsform.

Om en kurs har avvecklats eller genomgått en större förändring ska studenten erbjudas minst två examinationstillfällen, utöver ordinarie examinationstillfälle. Dessa tillfällen fördelas under en tid av minst ett år, dock som längst två år efter det att kursen avvecklats/förändrats. Vad gäller praktik och verksamhetsförlagd utbildning (VFU) gäller motsvarande, men med begränsning till endast ett ytterligare examinationstillfälle.

Om en student har fått besked om att denne uppfyller kraven för att vara student vid Riksidrottsuniversitetet (RIU-student) har examinator rätt att besluta om anpassning vid examination, om detta görs i enlighet med Lokala regler gällande RIU-studenter vid Göteborgs universitet.

Delkurser

1. Projekt, 6 hp
   Betygsskala: Mycket väl godkänd (5), Väl godkänd (4), Godkänd (3) och Underkänd (U)
2. Quiz, 1,5 hp
   Betygsskala: Godkänd (G) och Underkänd (U)

På kursen ges något av betygen Mycket väl godkänd (5), Väl godkänd (4), Godkänd (3) och Underkänd (U).

• Betyg 3: Godkända quiz, framgångsrikt genomfört projekt med inlämning av en fungerande artefakt, leverans av en bra rapport och presentation, samt godkänd kodgranskning.
• Betyg 4 och 5: utöver kriterierna som anges för årskurs 3 kommer dessa betyg att ges baserat på kvaliteten på genomförandet, resultaten, presentationen och rapporten.

Kursen utvärderas genom möten, både under och efter kursen, mellan lärare och studentrepresentanter. Ett anonymt skriftligt frågeformulär skickas även ut till studenterna efter kursens slut. Resultaten av utvärderingarna används för att förbättra kursinnehållet och som indikation till vilka delar som skulle kunna läggas till, tas bort, förbättras eller ändras.

Kursen är samläst med Chalmers.

För att delta i kursen rekommenderar vi att ha genomfört en av följande kurser:

• Formal Methods for Software Development
• Logic in Computer Science.