DD2460 Programvarusäkerhet 7,5 hp

• 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.

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.

Kunskaper i datasäkerhet, 6 hp, motsvarande slutförd kurs DD2395/DD2391.

Aktivt deltagande i kursomgång vars slutexamination ännu inte är Ladokrapporterad jämställs med slutförd kurs.
Den som är registrerad anses vara aktivt deltagande.
Med slutexamination avses både ordinarie examination och det första omexaminationstillfället.

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

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

• LAB2 - Laboration, 5,0 hp, betygsskala: A, B, C, D, E, FX, F
• TEN2 - Tentamen, 1,0 hp, betygsskala: A, B, C, D, E, FX, F
• ÖVN2 - Gruppresentation och rapport, 1,5 hp, betygsskala: A, B, C, D, E, FX, 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.

Cyrille Artho

• 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.

Den tidigare modulen EXA2 ersätts av TEN2.

I denna kurs tillämpas EECS hederskodex, se:
http://www.kth.se/eecs/utbildning/hederskodex

Denna kurs innehåller grupprojekt och laborationer. Kursregistrering efter den officiella registreringsperioden är inte möjligt, eftersom vi behöver skapa grupperna i början av kursen.