Hoppa till huvudinnehållet
Till KTH:s startsida

FDD3463 Programvarusäkerhet 7,5 hp

Programvarusäkerhet handlar om att säkerställa att programvaran i ett säkerhetskritisk system beter sig på ett korrekt och tillförlitligt sätt. Detta kan betyda att programvaran inte låter obehöriga få tillgång till data de inte har behörighet till, eller att programvaran är fri från programfel som deadlocks eller buffer overflows. De huvudsakliga teknikerna som används för programvarusäkerhet är statisk analys, övervakning, och testning. I kursen behandlas flera grundläggande tekniker för programvarusäkerhet.

Information per kursomgång

Termin

Information för HT 2024 Start 2024-10-28 programstuderande

Studielokalisering

KTH Campus

Varaktighet
2024-10-28 - 2025-01-13
Perioder
P2 (7,5 hp)
Studietakt

50%

Anmälningskod

51467

Undervisningsform

Normal Dagtid

Undervisningsspråk

Engelska

Kurs-PM
Kurs-PM är inte publicerat
Antal platser

Ingen platsbegränsning

Målgrupp
Ingen information tillagd
Planerade schemamoduler
[object Object]
Del av program
Ingen information tillagd

Kontakt

Examinator
Ingen information tillagd
Kursansvarig
Ingen information tillagd
Lärare
Ingen information tillagd

Kursplan som PDF

Notera: all information från kursplanen visas i tillgängligt format på denna sida.

Kursplan FDD3463 (VT 2022–)
Rubriker med innehåll från kursplan FDD3463 (VT 2022–) är markerade med en asterisk ( )

Innehåll och lärandemål

Kursupplägg

Denna kurs ges samtidigt med kursen på masternivå DD2460 (Software Safety and Security). Ph.D. kursen skiljer sig på följande sätt:

1. Rapporten och slutpresentationen, samt övningslabben som är utformade för att lära sig de olika verktygen, är individuella uppgifter.

2. Istället för att lösa fördefinierade guidade uppgifter i verifiering kommer studenterna att utveckla en formell modell och en modell på mjukvarunivå av en algoritm, arkitektur eller protokoll som de arbetar med som en del av sin forskning. Högnivåmodellen kommer att utvecklas i Event-B, NuSMV, eller ett liknande verktyg som är lämpligt för formell verifiering; lågnivåmodellen (som kan inkludera endast en del av högnivåmodellen) kommer att skrivas i ett programmeringsspråk som Java och verifieras med ett verktyg som JPF eller PAT.

Kursinnehåll

    Del I. Introduktion till programvarusäkerhet.
    Del II. Temporallogik, modellering, modelltestning, formell specifikation. Verktyg: NuSMV.
    Del III. Systemmodellering med Event-B. Verktyg: Rodin.
    Del IV. Parallellism, nätprogrammering. Verktyg: Java Pathfinder.
    Del V. Minnessäkerhet, fuzzning. Verktyg: minneskontrollverktyg, fuzz-testare.

Lärandemål

Efter godkänd kurs ska studenten kunna:
    förklara säkerhetsaspekter för system,
    konstruera modeller av system,
    specificera och analysera säkerhetsegenskaper,
    tillämpa analysverktyg på programvarusystem,
    utvärdera och jämföra olika tillvägagångssätt för verifiering och validering av programvarusystem,
i syfte att
    som samhällsmedborgare och expert kunna diskutera programvarusäkerhet,
    i arbetslivet och/eller forskningsprojekt kunna uttrycka säkerhetsegenskaper formellt,
    kunna använda och anpassa olika verktyg och tekniker för att verifiera sådana egenskaper.

Kurslitteratur och förberedelser

Särskild behörighet

Genomgången kurs i datasäkerhet motsvarande DD2395.
För Ph.D. kandidaten behöver naturligtvis åtminstone en design av en forskningsidé för att kunna formalisera den i en modell.

Rekommenderade förkunskaper

Goda kunskaper och färdigheter inom programmering, programspråk och programsemantik. Kunskap om första ordningens logik och ändliga automater.

Utrustning

 Programvaruinstallationer tillhandahålls på KTH:s labbdatorer eller tillgängliga via länkar på Canvas.

Kurslitteratur

 Forskningsartiklar, bokutdrag, verktygsdokumentation och webbsidor; tillhandahålls på Canvas.

Examination och slutförande

När kurs inte längre ges har student möjlighet att examineras under ytterligare två läsår.

Betygsskala

P, F

Examination

  • EXA1 - Examination, 7,5 hp, betygsskala: P, F

Examinator beslutar, baserat på rekommendation från KTH:s handläggare av stöd till studenter med funktionsnedsättning, om eventuell anpassad examination för studenter med dokumenterad, varaktig funktionsnedsättning.

Examinator får medge annan examinationsform vid omexamination av enstaka studenter.

Möjlighet till komplettering

Ingen information tillagd

Möjlighet till plussning

Ingen information tillagd

Examinator

Etiskt förhållningssätt

  • Vid grupparbete har alla i gruppen ansvar för gruppens arbete.
  • Vid examination ska varje student ärligt redovisa hjälp som erhållits och källor som använts.
  • Vid muntlig examination ska varje student kunna redogöra för hela uppgiften och hela lösningen.

Ytterligare information

Kursrum i Canvas

Registrerade studenter hittar information för genomförande av kursen i kursrummet i Canvas. En länk till kursrummet finns under fliken Studier i Personliga menyn vid kursstart.

Ges av

Huvudområde

Denna kurs tillhör inget huvudområde.

Utbildningsnivå

Forskarnivå

Påbyggnad

Ingen information tillagd

Forskarkurs

Forskarkurser på EECS/Teoretisk datalogi