Dina studier

Kursplan för Formella metoder för säkerhet

Kursplanen innehåller ändringar
Se ändringar

Kursplan fastställd 2026-02-16 av programansvarig (eller motsvarande).

Kursöversikt

  • Engelskt namnFormal methods for security
  • KurskodDAT705
  • Omfattning7,5 Högskolepoäng
  • ÄgareMPALG
  • UtbildningsnivåAvancerad nivå
  • HuvudområdeDatateknik
  • InstitutionDATA- OCH INFORMATIONSTEKNIK
  • BetygsskalaTH - Mycket väl godkänd (5), Väl godkänd (4), Godkänd (3), Underkänd

Kurstillfälle 1

  • Undervisningsspråk

    Engelska

  • Anmälningskod

    02143

  • Sökbar för utbytesstudenter

    Ja

Poängfördelning

Modul
LP1
LP2
LP3
LP4
Sommar
Ej LP
Tentamensdatum
0126 Projekt 6 hp
Betygsskala: TH		 6 hp
0226 Övning 1,5 hp
Betygsskala: UG		 1,5 hp

    Examinator

    Behörighet

    Information saknas

    Kursspecifika förkunskaper

    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.

    Syfte

    Syftet med kursen är att ge studenterna en förståelse för hur formella metoder kan användas för att specificera, analysera och verifiera säkerhets- och integritetskritiska system, samt att ge praktisk erfarenhet av formella specifikationsspråk och automatiserade verifieringsverktyg.

    Lärandemål (efter fullgjord kurs ska studenten kunna)

    Kunskap och förståelse:
    • förklara formella metoders roll vid specificering och verifiering av säkerhetskritiska system
    Färdighet 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:
    • kritiskt bedöma styrkor och begränsningar hos olika formella tekniker

    Innehåll

    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 formalismismer och verifieringsmetoder som har utvecklats för att resonera kring säkerhets- och sekretessegenskaper. 

    Organisation

    Kursen består av föreläsningar och en projektkomponent. Föreläsningarna innehåller en obligatorisk del i form av deltagande i quiz. Projektarbetet innebär att implementera och experimentera med metoder och begrepp som introduceras i kursen. Att genomföra och presentera projektet, skriva en rapport samt delta i en kodgranskningssession är obligatoriskt.

    Litteratur

    Kursen baseras på öppet tillgängligt material såsom forskningsartiklar, samt föreläsningsanteckningar och annat kursmaterial som tillhandahålls under kursens gång.

    Examination inklusive obligatoriska moment

    För att bli godkänd på kursen krävs att studenten klarar quizmomenten samt gör ett tillfredsställande individuellt bidrag till projektet, vilket inkluderar implementering, presentation, deltagande i kodgranskning på plats samt inlämning av en skriftlig rapport som dokumenterar projektet.

    Betygsskalan omfattar Underkänd (U), 3, 4 och 5. För betyget 3 ska studenten ha klarat quizmomenten och framgångsrikt genomfört projektet med fungerande implementation, rapport, presentation och kodgranskning. Betygen 4 och 5 ges utifrån kvaliteten på implementation, resultat, rapport och presentation, utöver att kraven för betyget 3 är uppfyllda.

    Kursens examinator får examinera enstaka studenter på annat sätt än vad som anges ovan om särskilda skäl föreligger, till exempel om en student har ett beslut från Chalmers om riktat pedagogiskt stöd på grund av funktionsnedsättning.

    Kursplanen innehåller ändringar

    • Ändring gjord på kurstillfälle:
      • 2026-05-06: Examinator Examinator ändrat från Andrei Sabelfeld (andrei) till Alejandro Russo (russo) av Viceprefekt
        [Kurstillfälle 1]
      • 2026-04-24: Examinator Examinator Andrei Sabelfeld (andrei) tillagt av Viceprefekt
        [Kurstillfälle 1]