Audit az AI korában
A Trail of Bits egy Miden zkVM auditon mutatja be, hogyan változtatja meg az AI a biztonsági kódvizsgálatot. A lényeg nem az, hogy egy AI-agent keresse meg a hibákat, hanem hogy az auditorok AI-val olyan elemzőeszközöket építhetnek, amelyek korábban idő- és költségigényük miatt nem készültek volna el. A Miden saját assembly nyelvéhez hat hónap alatt LSP-szervert, decompilert, statikus elemzőmotort és a Lean bizonyítási rendszerhez formális VM-modellt készítettek.
A statikus elemzés több mint 400 olyan helyet talált, ahol a típusellenőrzés javítható, valamint egy súlyos sérülékenységet. Egy nem megfelelően ellenőrzött, prover által megadott érték miatt rossz moduláris eredmény volt előállítható, ami lehetővé tehette Falcon-aláírások hamisítását és az ilyen kulccsal védett Miden-számlák pénzeszközeinek eltulajdonítását. Emellett az AI-val támogatott Lean-modellezés 95 géppel ellenőrzött helyességi bizonyítást készített, és két olyan finom implementációs hibát is feltárt, amelyet a meglévő unit tesztek nem észleltek.
Az írás azért fontos, mert más irányból közelíti meg az AI szerepét a kiberbiztonsági auditokban. Nem az emberi auditor kiváltását mutatja be, hanem azt, hogy az AI drasztikusan csökkentheti a speciális decompilerek, linterszabályok, statikus analizátorok és formális modellek elkészítésének költségét. A formális bizonyításnál ráadásul az AI által generált bizonyítást a Lean kernel matematikailag ellenőrzi, miközben az ember feladata annak vizsgálata marad, hogy maga a bizonyítandó állítás helyesen fogalmazza-e meg a kívánt biztonsági tulajdonságot. Ez egy fontosabb változás lehet, mint pusztán több AI-generált hibajelentés, az auditor egy adott rendszerhez célzottan építhet új ellenőrzési infrastruktúrát, amely a későbbi verziók vizsgálatánál is újra felhasználható.
