Utvecklar säkra javaprogram med matematiska metoder

Mostowski har specificerat programmets önskade egenskaper i ett formellt, matematiskt språk och sedan utfört ett rigoröst korrekthetsbevis.

– Tekniken vi utvecklar knyter an till Java och är viktig för att öka säkerhet och skydd av personlig integritet i datornät, främst för smartkort. Men tekniken är inte begränsad till dessa, berättar Wojciech Mostowski.

Med formella metoder går det att visa att en konstruktion alltid uppfyller specifikationen. Detta görs genom att matematiskt bevisa att en serie villkor alltid är uppfyllda – och genom att bevisa att vissa andra villkor aldrig kommer att uppfyllas.

Tanken är att programtillverkarna själva ska verifiera datorernas mjukvara med verktyg som bygger på matematiska metoder. Det handlar om att skapa program med extra höga krav på säkerhet. Java Card är en teknologi som tillhandahåller verktyg för att programmera smartkort med en delmängd av programspråket Java. Java-program på smartkort kallas applets.

– Den verifikationsplattform som vi har använt i vår forskning är KeY-systemet* som är utvecklat inom KeY-projektet.

Ett av de viktigaste målen i Mostowskis forskning är att ta reda på hur långt det går nå inom formell verifering av storskaliga Java-program, i termer av användbarhet, automatisering och hur komplicerade egenskaper man kan bevisa.

Wojciech Mostowski har också undersökt praktiska och teoretiska brister i de verifierings- och utvecklingsmetoder som finns för Java Card-applets. Som en följd av detta har en programlogik anpassats för Java Card för att kunna uttrycka intressanta och viktiga skydds- och säkerhetsegenskaper. Mostowski har även föreslagit design-riktlinjer för att stödja och förenkla formell verifiering.

– Vi har även utfört omfattande praktiska experiment med KeY-systemet för att utvärdera vårt arbete.

Avhandlingen ”Formal Development of Safe and Secure Java Card Applets” försvarades vid en offentlig disputation under våren 2005 på Chalmers tekniska högskola, Göteborg

KeY-projektet:
KeY-projektet startade i november 1998 vid universitetet i Karlsruhe. Idag är det ett samarbete mellan universitetet i Karlsruhe, Chalmers och universitetet i Koblenz. Ett antal forskargrupper är knutna till projektet som finansieras av DFG, Deutsche Forschungsgemeinschaft, och Vinnova.

Syftet med projektet är att integrera den formella specificeringen och verifikationen av mjukvara i själva systemutvecklingsprocessen vid design av industriell mjukvara. Utgångspunkten är ett kommersiellt CASE-verktyg som är utökad med funktionaliteter för formell specificering och verifikation. Det slutgiltiga målet är att göra verifikationsprocessen transparent för användaren med avseende på den informella objektorienterade modellen.

Kontaktinformation
Mer information:
Wojciech Mostowskis epost: woj@cs.chalmers.se
tel. 031 772 1072, hemsida: www.cs.chalmers.se/~woj