Anthropic нь одоо байгаа төслүүдийн найдвартай байдал, аюулгүй байдлыг албан ёсоор баталгаажуулахын тулд хиймэл оюун ухааны загваруудыг ашиглан хийсэн туршилтын үр дүнг танилцуулсан. Туршилтын үеэр OSS Fuzz дэд бүтцэд туршсан 123 нээлттэй эхийн номын сангийн санах ойн алдаа байхгүй гэсэн математикийн баталгааг гаргахын тулд хиймэл оюун ухааны загваруудыг ашигласан.
Баталгаажуулалтыг RISC-V архитектурын эмхэтгэсэн угсралтын кодын түвшинд гүйцэтгэсэн. Үүсгэсэн нотолгооны нийт хэмжээ нь Rocq Prover баталгаажуулалтын системийн хувьд ойролцоогоор 180 сая мөр код байв (600 RISC-V зааварчилгаатай хоёртын файл тутамд ойролцоогоор 18 мөр). Нотолгоонуудыг одоо байгаа фуззинг тестүүдийг албан ёсны үзүүлэлт болгон автоматаар хөрвүүлэх замаар үүсгэсэн бөгөөд үүний дараа Клод AI загвар нь уг програм нь 64 MB хүртэлх оролтын өгөгдөлд алдаагүй болохыг баталсан.
Баталгаажуулалтын процессын явцад хиймэл оюун ухааны загвар нь өмнө нь fuzz тестээр илрүүлээгүй байсан олон зуун алдааг тодорхойлж, засварлахад бэлтгэх боломжтой байсан. Бусад зүйлсийн дотор эдгээрт тодорхой оролтын өгөгдлийг боловсруулах үед буферийн халих эмзэг байдал (жишээ нь, libexpat дахь CVE-2026-56132), мөн логик алдаанууд багтсан болно. Цаашилбал, хиймэл оюун ухааны загварыг zlib алгоритмын цөмийн хэрэгжилтийн тохирлыг нотлоход ашигласан. Linux RFC 1950 техникийн үзүүлэлтүүд.
Python хэлний дэд олонлогийн тайлбарлагчийг Rust дээр мөн үүсгэсэн бөгөөд үүний тулд Verus хэрэгслийн хэрэгслийг ашиглан CPython семантикт нийцэж байгаагийн албан ёсны нотолгоо бэлтгэсэн. CPython-той зан төлөвийг харьцуулахын тулд санамсаргүй байдлаар үүсгэгдсэн 1.7 сая гаруй Python програмыг гүйцэтгэсэн. Тохиолдлын 99.95%-д эдгээр програмуудыг шинэ хэрэгжилт болон CPython дээр ажиллуулах үр дүн давхцаж, илэрсэн аливаа зөрүү нь мэдэгдэж буй захын тохиолдлууд байв.
Албан ёсны баталгаажуулалт нь техникийн тодорхойлолтын нийцлийг баталгаажуулдаг боловч олон урсгалт холболтын асуудал, динамик холболт, бодит техник хангамж дээрх хэвийн бус зан үйлээс үүдэлтэй эрсдэлүүд албан бус хэвээр байгаа тул аюулгүй байдлын асуудлыг бүрэн арилгадаггүй. Санал болгож буй аргын гол давуу тал нь хоёртын файлуудтай шууд ажилладаг тул одоо байгаа кодыг албан ёсоор баталгаажуулж болох хэл дээр дахин бичих шаардлагагүй болгодог.
Эх сурвалж: opennet.ru
