SMILE: Een beveiligingsgerichte, formeel onderbouwde modelleertaal voor mensen

Het ontwikkelen van veilige software is een uitdaging die vereist dat je veiligheid aanpakt in elke fase van de ontwikkeling. De vroege ontwerpfases zijn cruciaal voor het bereiken van niet-functionele vereisten zoals veiligheid. Desondanks krijgt de beveiliging van een softwaresysteem in praktijk slechts beperkte aandacht tijdens deze ontwerpfases. Een cruciaal element voor softwareonterwerpers om te redeneren over de beveiliging van hun ontwerpen is dat ze beschikken over een geschikte modelleertaal.

Een modelleertaal is geschikt om te redeneren over de beveiliging van software indien deze tegemoet komt aan de noden van alle betrokken belanghebbende. In de context van deze thesis concentreren we ons op drie
noden die cruciaal zijn voor het ontwerpen van veilige software. Ten eerste, softwareontwerpers vereisen een expressieve taal in welke ze een breed gamma aan beveiligingsoplossingen kunnen voorstellen en kunnen nagaan hoe deze interageren. Ten tweede, analysten vereisen een precieze taal die toelaat een grondige, bij voorkeur (deels) geautomatiseerde, analyse uit te voeren van de toegepaste beveiligingsoplossingen. Als resultaat van een dergelijke analyse moeten alle aannames waarop de oplossingen steunen expliciet zijn geworden. Ten laatste, moet een dergelijke taal begrijpbaar zijn door alle betrokken belanghebbende, welke niet allemaal beveiligingsexperten of softwareontwerpers zijn.

Deze thesis stelt een taal voor het ontwerpen van veilige software voor. Deze taal bestaat uit voorgedefiniëerde, herbruikbare bouwblokken, elk met precies omlijnde functionaliteit. We hebben onze taal ook volledig formeel gespecifiëerd en voorzien ook een raamwerk waarin kan bewezen worden dat een softwareontwerp aan de benodigde beveiligingsvereisten voldoet. On na te gaan of onze taal voldoende expressief is, hebben we deze gebruikt om een realistisch authenticatiemechanisme te modelleren. Verder hebben we een empirische studie uitgevoerd ter evaluatie of beginnelingen met betrekking tot software beveiliging de bouwblokken van onze taal begrijpen mits minimale training.