"Institutsionaalne uurimistoetus" projekt IUT2-1
IUT2-1 "Tõestatavalt turvalised ja korrektsed arvutisüsteemid (1.01.2013−31.12.2018)", Dominique Peer Ghislain Dr Unruh, Tartu Ülikool, Loodus- ja täppisteaduste valdkond, arvutiteaduse instituut.
IUT2-1
Tõestatavalt turvalised ja korrektsed arvutisüsteemid
Provably secure and verifiable systems
1.01.2013
31.12.2018
Teadus- ja arendusprojekt
Institutsionaalne uurimistoetus
ETIS klassifikaatorAlamvaldkondCERCS klassifikaatorFrascati Manual’i klassifikaatorProtsent
4. Loodusteadused ja tehnika4.6. ArvutiteadusedP170 Arvutiteadus, arvutusmeetodid, süsteemid, juhtimine (automaatjuhtimisteooria)1.1. Matemaatika ja arvutiteadus (matemaatika ja teised sellega seotud teadused: arvutiteadus ja sellega seotud teadused (ainult tarkvaraarendus, riistvara arendus kuulub tehnikavaldkonda)100,0
PerioodSumma
01.01.2013−31.12.2013173 000,00 EUR
01.01.2014−31.12.2014173 000,00 EUR
01.01.2015−31.12.2015173 000,00 EUR
01.01.2016−31.12.2016173 000,00 EUR
01.01.2017−31.12.2017173 000,00 EUR
01.01.2018−31.12.2018173 000,00 EUR
1 038 000,00 EUR

Tundlikke ja kriitilisi isikuandmeid töödeldakse tänapäeval paljude erinevate seadmete poolt. Selle info terviklikust ja konfidentsiaalsust ähvardavad nii tarkvaravead kui pahatahtlikud rünnakud. Turvaliste ja verifitseeritavate süsteemide disainimine on aga olemuslikult keeruline: krüptograafiliste algoritmide kasutamiseks on vaja ekspertteadmisi, ning infosüsteemide keerukus välistab nende käsitsi analüüsimise, sest väiksedki implementeerimisvead võivad täielikult hävitada igasugused turvalisuse ja õigsuse garantiid. Saavutamaks kõrget usaldusväärsust, peab süsteem olema õigesti kavandatud (kasutades vajadusel krüptograafia "viimast sõna") ning selle nõuetekohast toimimist (st nii turvalisust kui korrektset toimimist) peab olema võimalik tõestada (ideaalis automaatselt arvuti abil). Selles projektis uurime meetodeid krüptograafilistel primitiividel ja protokollidel põhinevate turvaliste süsteemide kavandamiseks ning nende turvalisuse ja korrektsuse automaatseks verifitseerimiseks.
Sensitive and critical personal and business information is stored and managed by a multitude of electronic devices. Integrity and confidentiality of that data is threatened by software errors and malicious attacks. Yet, designing secure and verifiable systems is inherently difficult: The correct use of cryptography requires expert knowledge, the sheer complexity of the systems defies manual analysis; minor mistakes in implementation and analysis can completely destroy all security and correctness guarantees. For a high level of trust in a system, this system needs to be designed properly (using state-of-the-art cryptographic schemes where needed), and its proper operation (both security and correct behavior) needs to be proven (ideally with the help of a computer as humans are likely to make mistakes). In this project, we will study methods for designing secure systems (based on cryptographic primitives and protocols), and methods for computer-aided verification of their security and correctness.
Projekti peaeesmärgiks on turvalisus ja töökindlus. Selle saavutamiseks tegime teadusuuringuid järgnevates alamvaldkondades: Krüptograafia: Selleks, et luua turvalisi süsteeme, on vaja baasprimitiive. Töötasime välja uusi krüptosüsteeme, signatuuriskeeme, kuid ka keerukaid krüptograafilisi protokolle: nullteadmustõestusi, segamisvõrke anonüümsuse säilitamiseks, asukoha verifitseerimisprotokolle, privaatsust säilitavaid andmekaeve algoritme ning uusi rakendusi turvalisest sidekanalitest e-valimislahendusteni. Meie erilise tähelepanu all oli kvantkrüptograafia kaks peamist haru: turvalisus kvantrünnete vastu (töötasime välja kvantturvalisi krüpto- ja signatuuriskeeme) ning kvantmehaanikal põhinevatel algoritmide kasutamine klassikaliselt lahendumatute krüptograafiliste ülesannete lahendamiseks (nagu tingimusteta turvalisus, tühistatav krüptosüsteem, asukoha verifitseeritavus). Formaalne verifitseerimine: Tarkvaralahendused sisaldavad pea alati vigu. Kõrgete turvanõuele korral (nagu lennundus) tekitavad vead vastuvõetamatuid riske. Staatiline ianalüüs võimaldab formaalselt tõestada vigade puudumist tarkvaras. Koostöös TU Munich ülikooliga arendasime staatilist koodianalüsaatorit Goblint ja saime mitmeid olulisi teoreetilisi tulemusi. Vead krüptograafilistes turvatõestustes on samamoodi vastuvõetamatud. Töötasime välja mitmeid meetodeid klassikaliste ja kvantkrüptograafiliste protokollide formaalseks verifitseerimiseks ning realiseerisime vastava tarkvara ning selle käigus lõime uue tööstusstandardi krüptoskeemide jaoks. Kodeerimisteooria: Süsteemide töökindlust ei vähenda ainult ründed vaid ka vead andmete salvestamisel ja edastamisel. Töötasime välja mitmeid uusi koode (meetodeid tagamaks andmete säilimist vigade korral) ja neile vastavaid dekodeerimisalgoritme, mida saab kasutada nii raadiosides kui ka andmete salvestamiseks (välkmälus jm). Meie teadustöö jätkub nii rahvusvahelistes projektides (ERC grant CerQuS jt) kui ka koostöös tööstuspartneritega (Cybernetica jt).