Arvutiteaduse instituut
Tartu Ülikool
Neljapäeval, 11. detsembril 2003, kl 16.00 (pane tähele ebatavalist aega)
Küberneetika Maja (Akadeemia tee 21), ruum B101
Ettekande kiled: pdf
Kokkuvõte: Turvaline infovoog programmis tähendab seda, et programmi avalikud väljundid ei sõltu tema salajastest sisenditest, vähemalt mitte sel määral, et sellest ründajale mingit kasu oleks. Sageli teame me, et mingite muutujate väärtused programmi mingis punktis ei anna salajaste sisendite kohta mingit informatsiooni, kuid programmianalüüs seda fakti tuvastada ei suuda. Selle põhjuseks võivad olla programmis tehtavate operatsioonide iseärasused (midagi taandub ära), erinevad turvalisuse mõisted (muutujate väärtused annavad salajaste sisendite kohta infot mingi tugevama definitsiooni mõttes, aga mitte mingi nõrgema, praktilisema definitsiooni mõttes), ebatäpne spetsifikatsioon (me ikkagi ei taha salajaste sisendite kohta päris kõike varjata). Sellisel juhul on kombeks annoteerida programmi väidetega, et mingid muutujad salajaste sisendite kohta midagi olulist ei avalikusta; programmianalüüs kasutab neid annotatsioone.
Programmi sel viisil annoteerides tekib küsimus, mil määral on analüüsi tulemused seotud programmi semantikaga. Oma ettekandes me vaatame juhtu, kus programmi mingid muud väljundid on defineeritud salajaste sisendite kohta tundlikku informatsiooni mitte andma. Me defineerime, mida sel juhul infovoo turvalisus (suhteline salajasus) tähendab (avalikud väljundid ei tohi anda rohkem informatsiooni kui need teised väljundid) ja anname ka programmianalüüsi selle omaduse jaoks. Peale selle kirjeldame me üht meetodit eelpool kirjeldatud annotatsioonide modelleerimiseks suhtelise salajasuse kaudu.