آنتروپیک می‌گوید کلود ویژگی‌های امنیتی ۱۲۳ کتابخانه نرم‌افزاری را به‌طور رسمی اثبات کرده است
آنتروپیک در پژوهشی که در ۲۲ اکتبر ۲۰۲۶ منتشر کرد، گزارش داد که مدل هوش مصنوعی کلود توانسته است برای ۲۳۹ نقطه ورود در آزمون‌های فازینگِ ۱۲۳ کتابخانه متن‌باز، در سطح کد اسمبلی معماری RISC-V اثبات‌های رسمی تولید کند که درستی آن‌ها با ابزارهای ماشینی بررسی می‌شود. این پروژه با همکاری شرکت تئورم انجام شده است.
به گفته آنتروپیک، کلود ابتدا باگ‌های شناسایی‌شده را اصلاح کرد و سپس اثبات کرد که برنامه‌ها برای تمام ورودی‌های کوچک‌تر از ۶۴ مگابایت و در برابر همه پاسخ‌های مدل‌شده سیستم‌عامل لینوکس و چیدمان‌های حافظه، همواره به‌طور عادی خاتمه می‌یابند؛ بدون آنکه خطای ایمنی حافظه رخ دهد یا یکی از گزاره‌های تأییدی برنامه نقض شود. این اثبات‌ها بر این فرض استوارند که برنامه به‌صورت یک فایل اجرایی ایستا و تک‌ریسمانی، با بودجه حافظه ثابت، روی پردازنده RISC-V و تحت لینوکس اجرا می‌شود. آنتروپیک اعلام کرد که این اثبات‌ها در مجموع حدود ۱۸۰ میلیون خط کد به زبان Rocq را شامل می‌شوند و هر اثبات معمولاً حدود ۶۰۰ هزار خط دارد؛ درحالی‌که طول میانه فایل‌های اجرایی بررسی‌شده ۱۸ هزار دستور RISC-V است. این شرکت می‌گوید تا آنجا که اطلاع دارد، این نخستین تلاش گسترده برای استفاده از هوش مصنوعی به‌منظور اجرای راستی‌آزمایی رسمی روی نرم‌افزارهای عملیاتی، در سطح کد اسمبلی، است.
بخشی از اثبات‌ها، به همراه معناشناسی رسمی دستورهای RISC-V و رفتار سیستم‌عامل که مبنای آن‌ها قرار گرفته است، در گیت‌هاب منتشر می‌شود. آنتروپیک همچنین اعلام کرد اجزای مورداعتماد ساخته‌شده برای این پروژه را که پیش‌تر در دسترس عموم نبوده‌اند، اثبات‌های کامل مربوط به آزمون‌های فازی که نیازی به اصلاح کد نداشتند و مشخصات آزمون‌هایی را که اثبات آن‌ها ممکن نشد، منتشر می‌کند. بااین‌حال، اثبات‌هایی که ممکن است یک باگ اصلاح‌نشده را آشکار کنند، منتشر نخواهند شد.
تبدیل آزمون‌های فازینگ به اثبات‌های رسمی
در این روش، آزمون فازینگ موجود و قابل‌کامپایل هر کتابخانه به یک مشخصات رسمی تبدیل می‌شود که یک قاعده را بیان می‌کند: آزمون نباید با هیچ ورودی کوچک‌تر از ۶۴ مگابایت از کار بیفتد. این مشخصات بر اساس دستورهای کامپایل‌شده RISC-V تعریف می‌شوند و از معناشناسی رسمی مجموعه دستورهای RISC-V و فرایندهای لینوکس که شرکت تئورم تدوین کرده است، بهره می‌برند. سپس اثبات‌گر Rocq هر اثبات تکمیل‌شده را در برابر مشخصات مربوطه بررسی می‌کند. به گفته آنتروپیک، در این ساختار تنها سه مؤلفه باید مورداعتماد باشند: مدل‌های رسمی RISC-V و فرایندهای لینوکس، گزاره‌های دقیق قضیه‌ها و خودِ بررسی‌کننده اثبات Rocq.
آنتروپیک اعلام کرد این فرایند را روی صدها پروژه در طرح OSS-Fuzz گوگل اجرا کرده است. این طرح آزمون فازینگ مستمر را برای پروژه‌های متن‌باز واجد شرایط فراهم می‌کند و برنامه‌های نوشته‌شده به زبان‌های C و C++ را به‌طور خودکار با AddressSanitizer تجهیز می‌کند؛ ابزاری که هنگام دسترسی نامعتبر به حافظه، اجرای برنامه را متوقف می‌کند. پیوستی با تاریخ ۲۲ اکتبر ۲۰۲۶، صورت کامل قضیه اثبات‌شده را شرح می‌دهد: برای تمام ورودی‌های کوچک‌تر از ۶۴ مگابایت و همه چیدمان‌های حافظه، نه فایل اجرایی مجهز به ASan و نه نسخه عادی برنامه دچار خطای حافظه، توقف اجباری یا رفتار خارج از مدل نمی‌شوند. همچنین، هر دو نسخه ردپاهای یکسانی از عملیات خواندن و نوشتن، رفتار هنگام خروج و وضعیت نهایی فایل‌سیستم تولید می‌کنند.
بر اساس این پیوست، کلود در جریان پروژه حدود یک میلیارد خط کد Rocq تولید کرد که تقریباً ۱۸۰ میلیون خط از آن‌ها از بررسی‌کننده اثبات عبور کردند. برای نمونه، نقطه ورود تجزیه‌گر ۳۹۱ خطی کتابخانه cJSON با اثباتی شامل ۶۳۰ هزار خط پوشش داده شد؛ درحالی‌که برای کتابخانه fftw3، با ۵۱ هزار خط کد پیوندشده، اثباتی ۴۸۰ هزار خطی تولید شد. ازآنجاکه کلود اجازه داشت پیش از تکمیل اثبات، کد را اصلاح کند، آنتروپیک برای اصلاحات امتیاز منفی در نظر گرفت و برای اثبات اینکه اصلاح کد دقیقاً کدام ورودی‌ها را تغییر داده است، امتیاز اضافی اختصاص داد. همچنین، اصلاحات ثبت و ممیزی شدند تا احتمال دست‌کاری سازوکار پاداش کاهش یابد.
باگ‌هایی که در جریان تلاش برای اثبات کشف شدند
آنتروپیک گزارش داد که تلاش برای اثبات رسمی، صدها باگ را آشکار کرده است که بسیاری از آن‌ها احتمالاً با روش‌های معمول فازینگ پیدا نمی‌شدند. هنگام اثبات یکی از نقاط ورود یک کتابخانه، کلود متوجه سرریز شمارنده‌ای در یک برنامه از حالت فشرده خارج‌کننده داده شد که به نوشتن خارج از محدوده حافظه منجر می‌شد؛ اما این مشکل فقط برای ورودی‌هایی در حدود ۲۰ مگابایت و با یک چیدمان خاص و نادر رخ می‌داد. یافته‌های دیگر شامل خواندن خارج از محدوده در یک رمزگشای تصویر بود که به ورودی ۶۴ مگابایتی و بیش از ۲ گیگابایت حافظه نیاز داشت، خواندن خارج از محدوده‌ای که تنها پس از توالی مشخصی از فراخوانی‌ها روی دو شناسه مربوط به یک فایل واحد رخ می‌داد، و کشف دوباره آسیب‌پذیری CVE-2026-56132 در کتابخانه libexpat بود که به ورودی دارای تو‌در‌تویی عمیق نیاز داشت.
کلود همچنین باگ‌های منطقی‌ای را پیدا کرد که هرگز باعث از کار افتادن برنامه نمی‌شوند؛ از جمله موردی که در آن محدودیت مربوط به فایل‌هایی که یک برنامه اجازه بارگذاری آن‌ها را دارد، همیشه اعمال نمی‌شد. آنتروپیک اعلام کرد تلاش برای راستی‌آزمایی چند برنامه مهم و پرکاربرد، یک باگ منطقی ناشناخته را آشکار کرد که بیش از یک دهه پنهان مانده بود. این شرکت همچنین گفت هنگام تلاش برای اثبات درستی یک نمایشگر PDF پرکاربرد، در عرض یک هفته به همان تعداد باگ امنیتی رسید که معمولاً طی یک سال گزارش می‌شود.
آزمایش‌های تکمیلی و یافته‌های مربوط به بهره‌وری
آنتروپیک در آزمایشی فراتر از OSS-Fuzz، از کلود خواست مشخصات رسمی RFC 1950 را بنویسد؛ سند فنی‌ای که قالب فشرده‌سازی zlib را تعریف می‌کند. سپس کلود باید اثبات می‌کرد که پیاده‌سازی zlib در هسته لینوکس مطابق این مشخصات عمل می‌کند. کلود مستقیماً فایل اجرایی کامپایل‌شده برای معماری x86 را اثبات کرد و برای این کار از معناشناسی رسمی مجموعه دستورهای x86 که خودش تولید کرده بود، بهره گرفت. آنتروپیک می‌گوید همین فرایند را برای شش کتابخانه پرکاربرد دیگر نیز تکرار کرده و باگ‌های جزئی و غیرقابل‌بهره‌برداری را در حالت‌های مرزی یافته است؛ باگ‌هایی که گزارش آن‌ها برای رسیدگی به پروژه‌های اصلی ارسال می‌شود. این شرکت همچنین گزارش داد که فرایند تولید معناشناسی x86، صدها اشتباه در مستندات مرجع رسمی و تعداد کمتری باگ در خود سخت‌افزار را آشکار کرد. افزون بر این، اجرای گام‌به‌گام بر اساس این معناشناسی می‌تواند محیط کاربری اوبونتو را روی یک هسته لینوکس راه‌اندازی کند.
در آزمایشی دیگر، کلود مفسری برای بخش بزرگی از زبان پایتون را با زبان Rust ساخت و با استفاده از ابزار راستی‌آزمایی Verus اثبات کرد که این مفسر از معناشناسی CPython پیروی می‌کند؛ معناشناسی‌ای که در یک مقاله دانشگاهی تشریح شده است. طبق پیوست فنی، هر ۱۷ لایه مفسر به‌طور رسمی اثبات شدند. قضیه اثبات‌شده می‌گوید: «هرگاه مفسر نتیجه‌ای برگرداند، آن نتیجه همان چیزی است که معناشناسی رسمی تعیین می‌کند.» آنتروپیک اعلام کرد آزمون تجربی روی ۱.۷ میلیون برنامه پایتون که به‌صورت تصادفی تولید شده بودند، نشان داد رفتار مفسر در ۹۹.۹۵ درصد موارد با CPython یکسان است. همچنین، از میان هفت باگی که عمداً در برنامه گنجانده شده بودند، پنج مورد از آزمون تصادفی جان سالم به در بردند، اما هر هفت مورد باعث شکست اثبات رسمی شدند.
برای سنجش بهره‌وری، آنتروپیک ۳۶ وظیفه کوچک راستی‌آزمایی ساخت که از کوچک‌سازی نقاط ورود واقعی OSS-Fuzz به دست آمده بودند. این برنامه‌ها بین ۲۸۳ تا ۲۴۹۱ دستور داشتند، ورودی آن‌ها به ۶۴ بایت محدود شده بود و AddressSanitizer در آن‌ها با یک محیط اجرایی کوچک‌تر به نام mini-ASan جایگزین شده بود که حدود ۱۰۰ دستور داشت. آنتروپیک گزارش داد که مدل Opus 5.5 نیمی از این وظایف را با مصرف حدود ۴۰ درصد توکن کمتر از Opus 5 اثبات می‌کند. این شرکت همچنین اعلام کرد عامل‌هایی که اجازه داشتند اثبات‌های یکدیگر را در فضای کاری مشترک کپی کنند، در مقایسه با عامل‌هایی که به‌تنهایی کار می‌کردند، به ۱۷ درصد توکن کمتر نیاز داشتند. برخی از این عامل‌ها پس از شکست در تلاش انفرادی موفق شدند و عامل‌هایی که به‌تنهایی کار می‌کردند، نتوانستند دو مورد از اثبات‌ها را تکمیل کنند. به گفته آنتروپیک، همین مزیت استفاده مجدد در مقیاس بزرگ پروژه OSS-Fuzz نیز مشاهده شد؛ در این پروژه، گروه‌های عامل‌ها اثبات‌های تکمیل‌شده را کپی و متناسب با نیاز خود اصلاح می‌کردند، زیرا بخش بزرگی از هر اثبات به کد مشترک زمان اجرای C و راه‌اندازی AddressSanitizer مربوط می‌شد.
محدودیت‌های اعلام‌شده و برنامه OSS Verify
آنتروپیک تأکید کرد که این اثبات‌ها به معنای عاری بودن کتابخانه‌ها از باگ نیستند؛ زیرا ممکن است مشکلات باقی‌مانده در اجزای مورداعتماد یا خارج از محدوده اثبات‌ها قرار داشته باشند. این اثبات‌ها فایل‌های اجرایی ایستای تک‌ریسمانی RISC-V را پوشش می‌دهند که با کتابخانه musl libc پیوند داده شده‌اند؛ حال آنکه بیشتر کاربران این کتابخانه‌ها را روی معماری‌های x86 یا ARM اجرا می‌کنند و از پیونددهی پویا با glibc بهره می‌برند. افزون بر این، AddressSanitizer تمام باگ‌های مربوط به ایمنی حافظه را شناسایی نمی‌کند. این شرکت انتظار دارد با پیشرفت مدل‌ها، بتوان این محدودیت‌ها را به‌تدریج برطرف کرد.
شرکت تئورم همین فرایند راستی‌آزمایی را از طریق برنامه OSS Verify به‌صورت رایگان در اختیار پروژه‌های متن‌باز واجد شرایط قرار می‌دهد. ثبت‌نام از طریق یک درخواست ادغام انجام می‌شود که فایل‌های project.yaml، Dockerfile و build.sh را به مخزن برنامه اضافه می‌کند. تئورم می‌گوید پروژه‌ها را با معیارهایی مشابه OSS-Fuzz بررسی می‌کند و زیرساخت‌های حیاتی و پرکاربرد را در اولویت قرار می‌دهد. طبق توضیحات این شرکت، نگه‌دارندگان پروژه یک اثبات Rocq دریافت می‌کنند که هسته بررسی‌کننده Rocq آن را تأیید کرده است و نشان می‌دهد هر هدف فازینگ با هیچ ورودی تا سقف ۶۴ مگابایت از کار نمی‌افتد. باگ‌های کشف‌شده در جریان اثبات، به‌صورت خصوصی و از طریق ایمیل به نگه‌دارندگان گزارش می‌شوند و برای افشای عمومی آن‌ها مهلت مشخصی تعیین نشده است. تولید اثبات‌ها ممکن است چند روز طول بکشد. نقشه راه تئورم نیز راستی‌آزمایی کل اکوسیستم Nix، از جمله زیرساخت‌های حیاتی مانند glibc، OpenSSL و cURL را هدف قرار داده است.