Mine planer

Jeg er doktorgradsstudent med prosjektet:

Formell modellering, spesifikasjon og verifikasjon av sikkerhet i Datasystemer.

Finansieringen er fra Norsk Forskninsråd/UiO, og utgår for tiden rundt juletider 1997. Etter dette vet jeg ikke hva jeg skal ta meg til. Det blir vel å søke en jobb. Bare synd det er tynt miljø på teoretisk sikkerhetsarbeid i Norge. Hvis noen er interessert i samarbeid så bare send meg beskjed og jeg vil stille opp.

Jeg har planlagt 3-4 artikler. Tittel og beskrivelse for disse følger nedenfor. Merk at tittel og innhold har vært og er under konstant revisjon.

Determination of non-interference in finite specifications.

Gitt et datasystem/spesifikasjon med et endelig antall tilstander. Og gitt et endelig alfabet med inndatasymboler. Vis at systemet er sikkert, dvs. opprettholder non-interferens.

Verification of security in algebraic specifications

Liste opp og evaluere kjente og nye teknikker for å verifisere sikkerhet generelt og non-interferens spesielt i algebraiske spesifikasjoner. Sammenligne og evt. vise hvorvidt noen er sterkere enn andre.

Refinement and non-interference

Gitt en spesifikasjon som skal har non-interferens-egenskap. Vedlikeholdes denne egenskapen ved forfining? Hva må isåfall til for at dette skjer? Kan det være noe å spare på å ikke vise dette i spesifikasjonen men vente til forfiningen, evt. til implementasjonen?

A model of information flow

I forvaltningen og ellers i samfunnet finnes det informasjon og det finnes en rett til å kunne motta denne informasjonen. Eksempler er innsynsrett i pasientjournaler og offentlighetsprinsippet i forvaltningen. Kan denne retten formaliseres, og kan man modellere dette inn som et sikkerhetsprinsipp i datasystemer? Artikkelen er ment å gi et eksempel på en slik modell.

Jon Haugsand (jonhaug@ifi.uio.no)

Sist endret: 8. oktober 1997