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 för forskarstuderande om när kursen ges
P4
Kursomgångar saknas för aktuella eller kommande terminer.
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.
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.
