Anthropic: Claude todisti 123 kirjaston tietoturvan

Anthropicin mukaan sen Claude-malli kirjoitti koneellisesti tarkistettuja matemaattisia todistuksia, jotka osoittavat, että 123 avoimen lähdekoodin kirjaston käännetty koodi ei voi kaatua määritellyissä olosuhteissa. Malli löysi matkan varrella myös virheitä, jotka olivat jääneet huomaamatta vuosien ajan huolimatta biljoonista testiajoista. Tutkimus julkaistiin 22. lokakuuta yhtiön Frontier Red Teamin toimesta, joka työskenteli projektissa muodollisten menetelmien yritys Theoremin kanssa.anthropic.com

Yhtiö kutsuu tätä uskoakseen "ensimmäiseksi laajamittaiseksi ponnistukseksi käyttää tekoälyä muodollisen verifioinnin soveltamiseen tuotanto-ohjelmistoihin konekielitasolla". Anthropicin mukaan tekoäly voi nyt löytää ja hyödyntää virheitä helposti, joten pelkkä testaus ei enää riitä ohjelmistojen suojaamiseen.anthropic.com

Fuzz-testeistä todistuksiin

Tiimi aloitti Googlen OSS-Fuzz-ohjelman fuzz-testeillä ja muutti jokaisen niistä muodolliseksi määrittelyksi. Sääntönä oli, että testi ei saa koskaan kaatua millään alle 64 megatavun syötteellä, kun se käännetään RISC-V-konekielelle. Muutamassa viikossa Claude todisti tämän 239 sisääntulopisteelle 123 kirjastossa. Todistukset muodostavat yhteensä noin 180 miljoonaa riviä koodia Rocq-todistuskielellä, ja tyypillinen todistus on noin 600 000 riviä pitkä, Anthropic kertoo. Rocq-todistusten tarkistaja vahvistaa, että jokainen todistus vastaa määrittelyään, joten kehittäjien ei tarvitse tarkistaa luotua koodia rivi riviltä, Interesting Engineering raportoi.interestingengineering.com+1

Anthropic kertoi, että osa todistuksista julkaistaan yhdessä niiden taustalla olevan RISC-V- ja Linux-semantiikan kanssa. Theorem tarjoaa saman prosessin ilmaiseksi kelpuutetuille avoimen lähdekoodin projekteille OSS Verify -ohjelmansa kautta, Unite.AI raportoi. Theorem on myös julkaissut Claude-taidon auttaakseen ylläpitäjiä rekisteröitymään.unite.ai+1

Fuzzerien ohittamat virheet

Todistusten kirjoittaminen paljasti satoja virheitä, jotka Claude korjasi ennen korjatun koodin todistamista. Dekompressorista se löysi laskurin alivuodon, joka johti puskurin ylitykseen, mutta vain noin 20 megatavun syötteillä tietyllä harvinaisella rakenteella. Toinen puskurin ylitys kuvien dekooderissa vaati 64 megatavun syötteen ja yli 2 gigatavua muistia. Claude löysi myös uudelleen tunnetun haavoittuvuuden libexpat-kirjastosta ja logiikkavirheen, jossa sovelluksen tiedostojen lataamista rajoittava ominaisuus ei aina toiminut, tutkimus kertoo.anthropic.com

Takuun rajat

Anthropic varoitti, etteivät todistukset tarkoita kirjastojen olevan täysin virheettömiä. Ne olettavat käytettävän yksisäikeistä staattista binääriä kiinteällä muistibudjetilla RISC-V-suorittimella Linuxin alla. Mahdolliset jäljellä olevat virheet ovat joko todistusten soveltamisalan ulkopuolella tai luotetuissa komponenteissa, eli laitteisto- ja käyttöjärjestelmämalleissa, teoreemamäärittelyissä tai itse Rocq-tarkistajassa, yhtiö kirjoitti. Useimmat käytössä olevat järjestelmät käyttävät muita suoritinarkkitehtuureja tai kokoonpanoja, Interesting Engineering huomautti.interestingengineering.com+1

Anthropic uskoo silti taloudellisten tekijöiden muuttuvan. "Kannustamme kaikkia kehittäjiä tutkimaan muodollista verifiointia kielimallien avulla, erityisesti niitä, jotka ovat aiemmin kokeilleet sitä vähemmän kyvykkäillä malleilla ja todenneet sen toimimattomaksi", tiimi kirjoitti.anthropic.com