See veebileht kasutab küpsiseid kasutaja sessiooni andmete hoidmiseks. Veebilehe kasutamisega nõustute ETISe kasutustingimustega. Loe rohkem
Olen nõus
"Eesti Teadusfondi uurimistoetus" projekt ETF8124
ETF8124 "Turvaomaduste arusaadavalt tõestatav keelepõhine kehtestamine (1.01.2010−31.12.2012)", Peeter Laud, Cybernetica AS.
ETF8124
Turvaomaduste arusaadavalt tõestatav keelepõhine kehtestamine
Convincingly provable language-based enforcement of security properties
1.01.2010
31.12.2012
Teadus- ja arendusprojekt
Eesti Teadusfondi uurimistoetus
ValdkondAlamvaldkondCERCS erialaFrascati Manual’i erialaProtsent
4. Loodusteadused ja tehnika4.6. ArvutiteadusedP175 Informaatika, süsteemiteooria1.1. Matemaatika ja arvutiteadus (matemaatika ja teised sellega seotud teadused: arvutiteadus ja sellega seotud teadused (ainult tarkvaraarendus, riistvara arendus kuulub tehnikavaldkonda)100,0
AsutusRollPeriood
Cybernetica ASkoordinaator01.01.2010−31.12.2012
PerioodSumma
01.01.2010−31.12.2010234 000,00 EEK (14 955,33 EUR)
01.01.2011−31.12.201114 955,60 EUR
01.01.2012−31.12.201214 955,60 EUR
44 866,53 EUR

Süsteemide turvaomaduste kehtestamine on raske ülesanne. Raskused kerkivad üles paljudel erinevatel tasemetel: turvaomaduste spetsifitseerimisel, turvatõestuse leidmisel, selle tõestuse kontrollil. Tõestuste süstematiseerimiseks on hiljuti välja pakutud programmide ümberkirjutamise meetod: turvatõestus esitatakse teisenduste jadana esialgsest süsteemist süsteemini, mille turvalisus on ilmne. Igaüks neist teisendustest on seejuures üsna lihtne ning lubab üsna lihtsasti tõestada, et ta süsteemi väljastpoolt jälgitavat käitumist ei muuda. Sellele ideele tuginedes on välja töötatud mitmeid erinevaid krüptoprotokollide turvatõestuste andmise raamvärke. Käesoleva projekti esmaseks ülesandeks on nende raamvärkide edasiarendus. Me pöörame suurt tähelepanu soovitud teisenduste jada leidmise viisidele. Meil on kavas võimaldada protokollide väljatöötajal see teisenduste jada interaktiivselt ette anda. See toob endaga kaasa mitmeid probleeme protokolliesituste semantika vallast, kuid ka kasutajaliideste vallast, need kaks valdkonda ei ole antud ülesande juures teineteisest lahutatavad. Me uurime ka teisenduste jada leidmise vahendi integreerimist teisenduste korrektsuse kontrolli vahendiga. Projekti täiendavaks eesmärgiks on areng neis andmeturbe valdkondades, kus programmide ümberkirjutamisel on oluline roll. Meil on kavas täielikumalt integreerida tüübisüsteeme arvutuslikult turvalise infovoo jaoks turvalise programmeerimise raamvärkidesse. Samuti on meil kavas uurida meetodeid erinevate süsteemide turvaanalüüsil kasutatavate ründepuude samm-sammuliseks lihtsustamiseks. Projekti tulemused parandavad meie aruteluoskust väidetavalt turvaliste süsteemide jaoks.
Enforcing the security properties of systems is a difficult task. The difficulties manifest at many levels: specifying properties, proving the security, verifying the proof. Recently the proofs have been systematized by the method of program rewriting. A proof is a sequence of transformations from the initial protocol to an obviously secure protocol. Each of the transformations is rather simple and allows a simple proof that it does not change the observable behaviour of the system. Based on that idea, several frameworks for giving security proofs for protocols have appeared. The main goal of the project is to advance those frameworks. We stress the importance of finding a suitable sequence of transformations. We intend to give the protocol researcher means of specifying that sequence interactively. This introduces various problems related to the semantics of protocol representations, and to the user interface of such a tool. Those classes of problems cannot be tackled separately. We also investigate the integration of a transformation-sequence-finding tool with a transformation-verifying tool. An additional goal of the project is to advance the art of other security problems where program rewriting plays a significant role. We intend to integrate type systems for computationally secure information flow more deeply with frameworks for secure programming. We also intend to develop methods for step-by-step simplification of attack trees that are used in the security analysis of various systems. The results of the project improve our ability to reason about allegedly secure systems.