Formaalit menetelmät¶

Formaalit eli muodolliset menetelmät ovat matematiikkaan ja logiikkaan perustuvia työkaluja tietojenkäsittelyjärjestelmien kehittämiseen ja niitä koskevaan päättelyyn, sekä ohjelmistojen, laitteistojen että näiden yhdistelmien tapauksessa. Formaalien menetelmien soveltaminen turvallisuuteen on noussut viime vuosikymmeninä vakiintuneeksi tutkimusalueeksi, joka keskittyy turvallisuusominaisuuksien määrittelyyn ja todistamiseen. Niiden käyttö vaatii tarkan spesifikaation

itse järjestelmälle käyttäen sopivaa abstraktiotasoa, joka voi olla idealisoitu suunnitelma, koodi tai jotain siltä väliltä,
vihamieliselle ympäristölle, jossa järjestelmä toimii, ja
ominaisuuksille, mahdollisesti muillekin kuin turvaominaisuuksille, jotka järjestelmän tulee täyttää.

Muodollinen päättely antaa mahdollisuuden todistaa, että järjestelmä täyttää määritellyt ominaisuudet vihamielisessä ympäristössä tai vaihtoehtoisesti tunnistaa haavoittuvuuksia suhteessa johonkin hyvin määriteltyyn hyökkääjien luokkaan.

Formaaleja menetelmiä voidaan soveltaa laajasti ja ne ovat tärkeitä tämän materiaalin monilla muilla, teknisillä osa-alueilla. Formalismeilla on sovelluksia koko järjestelmäpinossa (siis kovosta tietojärjestelmiin). Edellytyksenä muodollisten menetelmien opiskelulle ovat taustatiedot logiikasta, diskreetistä matematiikasta, automaattisesta päättelystä (theorem proving), formaaleista kielistä ja ohjelmoinnin semantiikasta.

Mallintaminen ja abstraktio ovat formaalien menetelmien kulmakiviä. CyBOK-tekstistä saat tietoa niiden soveltamisesta useilla kyberturvan aloilla, joita ovat pääsynvalvonta, suojattu tietovuo, kryptoprotokollat ja ohjelman oikeellisuus. Teksti kattaa erilaisia lähestymistapoja muodolliseen analyysiin ja todistamiseen, esimerkiksi sellaiset, joiden pohjalla on semantiikka, pelit, simulaatio, ekvivalenssi tai hienonnus (refinement). Näiden kautta voit tutustua sekä logiikkaan perustuviin että käyttäytymiseen liittyviin. Edellisissä vaatimukset ilmaistaan logiikan kaavoilla ja jälkimmäisissä turvallisen toiminnan mallien avulla. Esimerkkejä käytännön työkaluista näille lähestymistavoille ovat yleiskäyttöiset automaattiset todistajat, kuten Isabelle / HOL ja Coq, toteutuvuuden ratkaisijat, kuten Z3, mallintarkistimet, kuten SPIN, FDR ja PRISM.

Järjestelmäkehitys seuraa usein perinteistä koodauksen, testauksen ja korjauksen sykliä. Tietoturvakriittisissä järjestelmissä “testaus—korjaus” voi olla käytännössä “murto—paikkaus”, koska virheet voivat johtaa tietoturva-aukkoihin. Esimerkiksi ohjelmaan, josta puuttuu tarkistus muistiin kirjoitettaessa, voidaan kohdistaa puskurin ylivuotohyökkäys. Ja järjestelmä, joka ei tarkista kaikkia käyttöoikeuspyyntöjä, voi johtaa luvattomaan resurssien käyttöön. Pientenkin virheiden vaikutukset voivat olla tuhoisia käytännössä. Jotkut hyökkääjät ovat erittäin taitavia löytämään ja hyödyntämään hyvinkin mitättömän tuntuisia vikoja. Formaalit menetelmät tarjoavat mahdollisuuden parantaa järjestelmäkehityksen sykliä varmistamalla, että järjestelmät täyttävät vaatimukset tai ovat ainakin vapaita tietyntyyppisistä vioista.

Formaaleja menetelmiä voidaan käyttää järjestelmän kehittämisen ja toiminnan eri vaiheissa, ja niitä voidaan soveltaa erilaisiin järjestelmän artefakteihin.

Järjestelmäsuunnittelu: Niitä voidaan käyttää kaikenlaisten suunnitelmien määrittelyyn ja verifiointiin — tai virheiden löytämiseen niistä. Hyvä esimerkki ovat kryptoprotokollat, joissa muodolliset menetelmät ovat huomattavasti edistäneet turvallisuutta.
Kooditaso: Ohjelmissa on virheitä, jotka usein edustavat tietoturva-aukkoja. Oikeilla työkaluilla vikojen etsiminen on helppoa. Formaalit työkalut vaihtelevat yksinkertaisista staattisista analysaattoreista täysimittaiseen interaktiiviseen verifiointiin. Edelliset voivat varmistaa erittäin suurissakin koodikannoissa “matalia” ominaisuuksia, kuten tietyntyyppisten turvavikojen poissaolon. Jälkimmäisillä voi todistaa syvällisiä ominaisuuksia, mutta yleensä vain pienissä ohjelmissa.
Konfiguraatiotaso: Järjestelmien turvallisuus riippuu myös siitä, miten ne on konfiguroitu. Esimerkiksi pääsynvalvontamekanismit vaativat määrittelyn, kenellä on oikeus tehdä mitäkin.

Edellä on korostunut formalismien vaikutus turva-aukkojen karsimisessa. Käänteisesti formalismeilla voidaan saada turvallisten järjestelmien kehittämiselle vahva matemaattinen pohja. Tällainen matemaattisten menetelmien soveltaminen oikein toimivien ohjelmien tai järjestelmien kehittämiseksi (eikä vain vikojen havaitsemiseksi) oli motivaationa muodollisten menetelmien varhaisille kehittäjille. Ajatuksen ytimenä on tarkastella ohjelmia ja järjestelmiä matemaattisina objekteina, joista tehdään päätelmiä matematiikan ja logiikan avulla. Kumpikin näkökulma, vikojen haku ja viattomaksi rakentaminen, soveltuvat turvallisuuteen mutta eivät ole siitä riippuvaisia.

Kun sovellusalueena on turvallisuus, tarvitaan kaksi täydennystä: ensinnäkin ympäristö on vihamielinen ja sitä varten täytyy tehdä uhkamalli, jossa uhka on yleensä aktiivinen, hyökkääjä. Toiseksi jotkin turvaominaisuudet eroavat perinteisistä ohjelman oikeellisuuteen kuuluvista ominaisuuksista siten, että niitä ei voi päätellä yksittäisistä ohjelman suorituksista, ei vaikka kaikki mahdollisuudet käytäisiin läpi. Täytyy verrata suorituksia eri syötteillä, ja usein pareittainen vertailu riittää joskin pitää ulottaa kaikkiin pareihin. Tällaisia ominaisuuksia kutsutaan hyperominaisuuksiksi (nimitys on vuodelta 2010). Turvallisuuden alalla keskeisiä esimerkkejä ovat sivukanavien puuttuminen ja suoritusten riippumattomuus (englanniksi täsmällisemmin non-interference). Esimerkiksi Spectre- ja Meltdown-haavoittuvuuksien puuttuminen järjestelmästä ovat hyperominaisuuksia. Niitä ei löydetty formaaleilla menetelmillä, mutta löydön jälkeen ne voitiin formalisoida ja rakentaa työkaluihin mekanismit vastaavien ongelmien havaitsemiseksi. Vuonna 2021 esijulkaistun artikkelin A Survey of Practical Formal Methods for Security mukaan on edelleen niin, että “menetelmät osoittavat ongelman läsnäolon, eivät sen puutetta”. Artikkeli ilmaisee tämän formaaleille menetelmille ja tietoturvahaavoittuvuuksille, muokaten Dijkstran kuuluisaa ja edelleen pätevää toteamusta vuodelta 1969, jossa menetelmän sijasta oli testaus ja ongelmana ohjelmistobugi.

Vielä lähempänä käytäntöä on katsausartikkeli Formal verification: will the seedling ever flower? (2017), joka otsikostaan huolimatta esittää useita hyvin onnistuneita projekteja. Siinä on myös kokemusperäisiä neuvoja formaalien menetelmien ja työkalujen valinnalle. Mainitaan vielä teoreettinen mutta melko yleistajuiseksi kirjoitettu artikkeli Blueprint for a science of cybersecurity, josta löytyy mm. hyperominaisuuden selitys (artikkeli on NSA:n tulevaisuusjulkaisussa vuodelta 2012.)

Esimerkki: CSP kryptografisten protokollien mallinnuksessa

CSP (communicating sequential processes) on abstrakti kieli, jolla kuvataan rinnakkain toimivia ja viestien vaihdon avulla kommunikoivia järjestelmiä. Ne koostuvat prosesseista, jotka “elävät” tapahtumien (events) kautta. Prosessit ilmaisevat, millaisia tapahtumia voi sattua ja miten ne asettuvat toistensa perään tai rinnalle. Osa tapahtumista on sellaisia, jotka synkronoivat eri prosesseja. Tällaiset on luontevaa tulkita viestien lähettämiseksi ja vastaanottamiseksi, mutta se ei ole ainoa mahdollisuus.

Kryptografinen protokolla mallinnetaan määrittämällä osapuolet, hyökkääjä ja verkko (media) prosesseiksi, joissa tapahtumina ovat tietynmuotoiset viestit, jotka “lähetetään” kanavia pitkin. Mitään lähetyksiä ei tietenkään tapahdu ja puhe kanavista on vain havainnollistus. CSP on itse asiassa prosessien algebra, jossa prosesseista voi “laskea” uusia esim. asettamalla niitä rinnakkain tai peräkkäin tai määrittelemällä niiden välille viestikanava.

Tietoturvatavoitteet mallinnetaan asettamalla vaatimuksia sille, millaisia tapahtumaketjuja eli jälkiä (traces) tällaisessa systeemissä voi esiintyä. Siis kaikkien mahdollisten tapahtumaketjujen pitää toteuttaa joitakin ominaisuuksia. Tämä riittää luottamuksellisuuden ja autenttisuuden mallintamiseen. Jos halutaan tutkia kiistämättömyyttä tai saatavuutta, joudutaan vaatimaan myös sitä, että tietynlaiset tapahtumaketjut ovat mahdollisia, tai siis että jotkin tapahtumat tosiaan toteutuvat. Tätä varten pitää ottaa huomioon, millaisia estymiä (failures) prosesseissa voi esiintyä (esimerkkejä ovat deadlock ja sen muunnelma livelock).

Prosessin (jälki-)semantiikalla tarkoitetaan siis kaikkia mahdollisia tapahtumaketjuja, jotka se voi suorittaa. Jälkiä koskevat vaatimukset voi tarkistaa todistamalla ne muodollisesti tai käyttämällä automaattista mallintarkistajaa (model checker). CSP:lle soveliain on nimeltään FDR, joka ei oikeastaan tarkista yhtä mallia, vaan vertailee kahta prosessia P ja Q. Vertailussa selviää, onko P hienonnus (refinement) Q:sta eli sisältyykö P:n semantiikka Q:n semantiikkaan. Lähtökohta Q mainitaan usein spesifikaatioksi, jota implementaatio P hienontaa. Jälki-semantiikassa P on hienonnus Q:sta, jos jokainen P:lle mahdollinen tapahtumaketju on mahdollinen myös Q:lle — eli implementaatiossa ei tapahdu mitään sellaista mitä ei ole spesifioitu.

Nimi FDR tulee sanoista Failures Divergences Refinement. Failure tarkoittaa estymää kuten jo mainittiin ja divergence eli pillastuma tarkoittaa ikisilmukkaa; yleisessä semantiikassa pitää nekin ottaa huomioon. FDR toimii siten, että se käy läpi tietyn tila-avaruuden kaikki tilat (“jälkiä seuraten”). Näin ollen se voi käsitellä vain äärellistilaisia systeemejä (muutamaan miljoonaan tilaan asti). Siispä menetelmää voidaan käyttää vain sellaisen systeemin tutkimiseen, jossa on rajattu määrä osapuolia, käytännössä vain muutama. Protokollan sinänsä pitää toimia periaatteessa rajattoman toimijajoukon puitteissa. Oxfordin yliopistossa 1990-luvulla kehitetty FDR on nykyään kaupallinen tuote: FDR4-sivulta voi koodia ladata myös kokeiltavaksi.