شرکت آنتروپیک نتایج آزمایش‌هایی را که با استفاده از مدل‌های هوش مصنوعی برای تأیید رسمی قابلیت اطمینان و امنیت پروژه‌های موجود انجام شده بود، ارائه داد. در طول آزمایش، از مدل‌های هوش مصنوعی برای تولید اثبات‌های ریاضی عدم وجود خطاهای حافظه برای ۱۲۳ کتابخانه متن‌باز آزمایش‌شده در زیرساخت OSS Fuzz استفاده شد.
این تأیید در سطح کد اسمبلی کامپایل شده برای معماری RISC-V انجام شد. حجم کل اثبات‌های تولید شده تقریباً به ۱۸۰ میلیون خط کد برای سیستم تأیید Rocq Prover رسید (تقریباً ۶۰۰۰۰۰ خط در هر فایل باینری با ۱۸۰۰۰ دستورالعمل RISC-V). اثبات‌ها با تبدیل خودکار تست‌های فازینگ موجود به مشخصات رسمی تولید شدند، پس از آن مدل Claude AI ثابت کرد که برنامه برای هر داده ورودی تا ۶۴ مگابایت بدون نقص است.
در طول فرآیند اثبات، مدل هوش مصنوعی توانست صدها باگ را که قبلاً توسط آزمایش فاز شناسایی نشده بودند، شناسایی و رفع کند. از جمله موارد دیگر، این موارد شامل آسیب‌پذیری‌های سرریز بافر هنگام پردازش داده‌های ورودی خاص (به عنوان مثال، CVE-2026-56132 در libexpat) و همچنین خطاهای منطقی بود. علاوه بر این، از مدل هوش مصنوعی برای اثبات انطباق پیاده‌سازی الگوریتم zlib در هسته استفاده شد. Linux مشخصات RFC 1950.
یک مفسر برای زیرمجموعه‌ای از پایتون نیز در Rust ایجاد شد که برای آن یک اثبات رسمی انطباق با معناشناسی CPython با استفاده از جعبه ابزار Verus تهیه شد. برای مقایسه رفتار با CPython، بیش از ۱.۷ میلیون برنامه پایتون که به صورت تصادفی تولید شده بودند، اجرا شدند. در ۹۹.۹۵٪ موارد، نتایج اجرای این برنامه‌ها در پیاده‌سازی جدید و در CPython مطابقت داشت و هرگونه اختلافی که مشاهده شد، موارد حاشیه‌ای شناخته شده بودند.
تأیید رسمی، انطباق با مشخصات را تضمین می‌کند، اما مسائل امنیتی را به طور کامل از بین نمی‌برد، زیرا خطرات ناشی از مشکلات چندرشته‌ای، پیوند پویا و رفتار غیرعادی در سخت‌افزار واقعی، غیررسمی باقی می‌مانند. یکی از مزایای کلیدی رویکرد پیشنهادی این است که مستقیماً با فایل‌های دودویی کار می‌کند و نیاز به بازنویسی کد موجود به زبان‌های قابل تأیید رسمی را از بین می‌برد.
منبع: opennet.ru
