Anthropic esitteli kokeiden tuloksia, joissa tekoälymalleja käytettiin olemassa olevien projektien luotettavuuden ja turvallisuuden muodolliseen varmentamiseen. Kokeen aikana tekoälymalleja käytettiin matemaattisten todisteiden luomiseen muistivirheiden puuttumisesta 123 avoimen lähdekoodin kirjastolle, joita testattiin OSS Fuzz -infrastruktuurissa.
Todistus suoritettiin käännetyn assembly-koodin tasolla RISC-V-arkkitehtuurille. Rocq Prover -todennusjärjestelmälle luotujen todistusten kokonaismäärä oli noin 180 miljoonaa riviä koodia (noin 600 000 riviä binääritiedostoa kohden ja 18 000 RISC-V-käskyä). Todisteet luotiin muuntamalla olemassa olevat fuzz-testit automaattisesti muodollisiksi spesifikaatioiksi, minkä jälkeen Clauden tekoälymalli osoitti ohjelman olevan virheetön mille tahansa syöttödatalle aina 64 Mt:iin asti.
Todisteiden rakentamisprosessin aikana tekoälymalli pystyi tunnistamaan ja korjaamaan satoja bugeja, joita fuzz-testaus ei aiemmin havainnut. Näihin kuuluivat muun muassa puskurin ylivuotohaavoittuvuudet tiettyjen syöttötietojen käsittelyssä (esim. CVE-2026-56132 libexpatissa) sekä loogiset virheet. Lisäksi tekoälymallia käytettiin osoittamaan ytimen zlib-algoritmin toteutuksen vaatimustenmukaisuus. Linux RFC 1950 -spesifikaatiot.
Rustissa luotiin myös tulkki osalle Pythonin kieltä, jolle laadittiin muodollinen todistus CPython-semantiikkaa koskevasta yhteensopivuudesta Verus-työkalupakin avulla. Käyttäytymisen vertailemiseksi CPythonin kanssa suoritettiin yli 1.7 miljoonaa satunnaisesti luotua Python-ohjelmaa. 99.95 %:ssa tapauksista näiden ohjelmien suorittamisen tulokset uudessa toteutuksessa ja CPythonissa täsmäsivät, ja kaikki havaitut eroavaisuudet olivat tunnettuja reunatapauksia.
Muodollinen todentaminen takaa spesifikaatioiden noudattamisen, mutta se ei täysin poista tietoturvaongelmia, koska monisäikeisyyden, dynaamisen linkityksen ja todellisen laitteiston poikkeavan käyttäytymisen aiheuttamat riskit pysyvät formaalisoimattomina. Ehdotetun lähestymistavan keskeinen etu on, että se toimii suoraan binääritiedostojen kanssa, mikä poistaa tarpeen kirjoittaa olemassa olevaa koodia uudelleen formaalisesti todennettavissa olevilla kielillä.
Lähde: opennet.ru
