Johdanto tekoälyyn ja formaaleihin menetelmiin kyberturvallisuudessa¶

Tässä luvussa käsitellään kahta aihetta, jotka ovat kovin erilaisia, mutta joilla on silti useita yhteisiä piirteitä. Sekä tekoäly että formaalit menetelmät

perustuvat formaaleihin kieliin ja monimutkaisiin teorioihin.

ovat olleet kauan toivelistalla: Sekä tekoälyn että automaattisten todistusten unelma juontavat juurensa 1900-luvun puoliväliin.

ovat kumpikin vahvasti piilossa pinnan alla: Soveltajat, käyttäjistä puhumattakaan, ovat vuorovaikutuksessa tulosten, kuten parannetun uhkien havaitsemisen tai varmennetun järjestelmän eheyden kanssa, ilman että he syventyvät taustalla oleviin prosesseihin.

ovat hyvin yleiskäyttöisiä menetelmiä.

Tekoälyä tarkastellaan sekä puolustuksen että hyökkäyksen näkökulmasta, ja sen sovellustavat näihin tarkoituksiin vaihtelevat suuresti. Sen sijaan formaaleja menetelmiä esitellään vain puolustuksen näkökulmasta. Hyökkääjät käyttäisivät niitä tyypillisesti samalla tavalla kuin puolustajat. Tekoäly teki 2020-luvulla läpimurron yleiseen tietoisuuteen, mutta formaalit menetelmät pysynevät kauan piikossa kriittisten järjestelmien turvallisen rakentamisen apuna.