| Summary: | Threat modelling of systems is an emerging field within computer security. With the introduction of the Meta Attack Language (MAL) by KTH researchers, the need for being able to test and verify the correctness of such modelling techniques has once again become apparent. This paper investigates the use of symbolic execution as well as model verification tools in order to certify the correctness of the produced models and their behavior. With the help of language developers, as well as a literature study about the targeted testing methods, it has been concluded that the current design of MAL makes it very difficult to test it effectively, and it is recommended that modifications be made to address that issue. === Hotmodellering av system är ett växande område inom datasäkerhet. Med introduktionen av Meta Attack Language (MAL) av KTH-forskare har behovet av att kunna testa och verifiera korrektheten av sådana modelleringstekniker återigen blivit uppenbart. Det här arbetet undersöker användningen av symbolisk exekvering samt verifieringsverktyg för programmodeller för att bekräfta korrektheten hos de producerade modellerna och deras beteende. Med hjälp av programspråkutvecklare, såväl som en litteraturstudie om de föreslagna test-metoderna, har man dragit slutsatsen att den nuvarande utformningen av MAL gör det svårt att testa det effektivt, och det rekommenderas att ändringar görs för att lösa problemet.
|
|---|
