اثبات صوری ۱۲۳ کتابخانه متن‌باز با Claude؛ وارد شدن وریفیکیشن به دنیای واقعی

چه کاری انجام شد؟

اثبات صوری یعنی به‌جای آزمایش چند ورودی، با استدلال ریاضی نشان دهیم برنامه برای همهٔ ورودی‌ها یک ویژگی مشخص را دارد. مشکل همیشگی این روش هزینه است. نمونهٔ معروف آن seL4 است که ساختنش حدود ۲ نفر-سال و راستی‌آزمایی‌اش حدود ۲۰ نفر-سال طول کشید. به همین دلیل وریفیکیشن بیشتر در کدهای حیاتی مانند الکترونیک هوانوردی استفاده شده است.

این تیم دشوارترین بخش، یعنی نوشتن مشخصات (spec)، را از تست‌های fuzz موجود گرفت. ویژگی مورد اثبات این بود که برنامه هرگز کرش نکند: هیچ خطای ایمنی حافظه یا شکست assertion رخ ندهد و خروج عادی باشد. این ویژگی برای همهٔ ورودی‌های کمتر از ۶۴ مگابایت و همهٔ پاسخ‌های مدل‌شدهٔ سیستم‌عامل و چیدمان‌های حافظه ثابت شد.

روند کار چنین بود: کتابخانه و تست fuzz آن به RISC-V کامپایل می‌شوند. با معناشناسی صوری RISC-V و فرایندهای لینوکس که Theorem ساخته، spec به‌صورت مکانیکی تولید می‌شود. Claude اثبات را می‌نویسد و کرنل Rocq آن را بررسی می‌کند. اگر Claude باگی پیدا کند، کد را اصلاح می‌کند، spec دوباره تولید می‌شود و اثبات تازه‌ای نوشته می‌شود.

باگ‌هایی که fuzzer پیدا نمی‌کرد

به گفتهٔ گزارش، بسیاری از باگ‌ها را fuzzerها که معمولاً ورودی‌های کوچک (حدود ۱ مگابایت) را جهش می‌دهند، به‌سختی پیدا می‌کنند. یک نمونه underflow شمارنده در یک کتابخانهٔ فشرده‌سازی است که به نوشتن خارج از محدوده می‌رسد و ورودی حدود ۲۰ مگابایتی با چیدمان نادر لازم دارد. نمونهٔ دیگر خواندن خارج از محدوده در یک دیکدر تصویر است که ورودی ۶۴ مگابایتی و بیش از ۲ گیگابایت حافظه می‌خواهد. همچنین CVE-2026-56132 در libexpat دوباره کشف شد و یک باگ منطقی بدون کرش پیدا شد که در آن محدودیت بارگذاری فایل همیشه اعمال نمی‌شد.

نکتهٔ جالب این است که چون بسیاری از تست‌های fuzz خودشان ویژگی‌هایی مثل رفت‌وبرگشت (roundtrip) یا برابری با پیاده‌سازی مرجع را بررسی می‌کنند، اثبات «کرش نمی‌کند» گاهی خودِ آن ویژگی سطح بالا را هم ثابت می‌کند.

هزینه و محدودیت‌ها

هزینهٔ اصلی توکن است و اثبات‌ها می‌توانند صدها میلیون توکن بخواهند. در آزمایش‌های خود Anthropic، وقتی عامل‌ها می‌توانستند اثبات‌های هم را در یک فضای مشترک کپی کنند، حدود ۱۷٪ توکن کمتر مصرف شد. دلیلش این است که بخش بزرگی از اثبات‌ها دربارهٔ کد مشترک مانند runtime زبان C و راه‌اندازی ASan است.

نویسندگان خودشان تأکید می‌کنند «اثبات‌شده» یعنی «بدون باگ» نیست. چکر فقط تطابق اثبات با spec را تأیید می‌کند، نه تطابق spec یا مدل ماشین با واقعیت. اثبات‌ها برای باینری‌های تک‌نخی و استاتیک روی RISC-V با musl هستند، در حالی که بیشتر استقرارها x86 یا ARM و با glibc‌اند. ASan هم همهٔ باگ‌های حافظه را نمی‌گیرد، و خطر reward hacking در حلقهٔ اصلاح کد (بازنویسی برنامه تا ظاهراً کرش نکند) کاهش یافته اما حذف نشده است.

چرا برای برنامه‌نویس‌ها مهم است؟

اگر ادعای گزارش دربارهٔ مقیاس‌پذیری درست باشد، وریفیکیشن می‌تواند مثل fuzzing به ابزاری روزمره برای کتابخانه‌های پرکاربرد تبدیل شود. Theorem بخشی از اثبات‌ها و مدل‌های معناشناسی را منتشر کرده و پیشنهاد داده این فرایند را برای پروژه‌های متن‌باز دیگر هم اجرا کند. برنامهٔ آن‌ها شامل کتابخانه‌های مشترکی مثل glibc، OpenSSL و cURL است.

برای کاربران ایرانی، چون این ابزارها و اثبات‌ها متن‌باز و قابل دانلودند، بخش بزرگی از نتایج مستقل از تحریم‌ها قابل مطالعه است. اما اجرای خود Claude برای تولید اثبات تابع دسترسی به سرویس‌های خارجی است.