آنتروپیک با کمک کلود، امنیت ۱۲۳ کتابخانه نرم‌افزاری را بررسی کرد
شرکت آنتروپیک با همکاری شرکت تئورم، فعال در حوزه راستی‌آزمایی نرم‌افزار، با استفاده از مدل کلود توانسته است ویژگی‌های امنیتی مشخصی را در ۱۲۳ کتابخانه متن‌باز واقعی اثبات کند. این پروژه که نتایج آن در ۲۲ اکتبر ۲۰۲۶ منتشر شد، نشان می‌دهد هوش مصنوعی چگونه می‌تواند دامنه استفاده از روش‌های رسمی راستی‌آزمایی نرم‌افزار را گسترش دهد. پژوهشگران برنامه‌های اجرایی را در سطح کد اسمبلی معماری RISC-V بررسی کردند و باگ‌هایی را یافتند که با وجود آزمایش‌های گسترده، همچنان شناسایی نشده بودند. به گفته آنتروپیک، تا آنجا که این شرکت اطلاع دارد، این همکاری نخستین تلاش گسترده برای به‌کارگیری راستی‌آزمایی رسمی مبتنی بر هوش مصنوعی در نرم‌افزارهای عملیاتی و در سطح کد اسمبلی است.
پژوهشگران همچنین بخشی از اثبات‌های خود و مدل‌های معنایی زیربنایی مربوط به RISC-V و سیستم‌عامل را منتشر کردند تا امکان بررسی مستقل و استفاده مجدد از آن‌ها فراهم شود. این اثبات‌ها تضمین‌های مشخصی ارائه می‌کنند، اما به معنای عاری بودن کامل کتابخانه‌ها از نقص نیستند. بر اساس فرض‌های تعریف‌شده، برنامه‌های راستی‌آزمایی‌شده باید برای هر ورودی کوچک‌تر از ۶۴ مگابایت و هر پاسخ مدل‌سازی‌شده از سیستم‌عامل لینوکس و چیدمان حافظه، بدون خطای ایمنی حافظه یا شکست در گزاره‌های تأییدی، به‌طور عادی خاتمه یابند.
این تضمین‌ها زمانی معتبرند که برنامه به‌صورت یک فایل اجرایی ایستا و تک‌رشته‌ای، با بودجه حافظه ثابت، روی پردازنده RISC-V و تحت سیستم‌عامل لینوکس اجرا شود. آنتروپیک تأکید کرده است که این روش هنوز همه آسیب‌پذیری‌های احتمالی نرم‌افزار را از میان نمی‌برد.
راستی‌آزمایی رسمی با استفاده از استدلال ریاضی مشخص می‌کند که آیا یک نرم‌افزار از قواعدی که صریحاً برای آن تعریف شده‌اند پیروی می‌کند یا خیر. توسعه‌دهندگان ابتدا مشخصات رسمی رفتار مورد انتظار را تدوین می‌کنند و سپس می‌کوشند ثابت کنند که برنامه در تمام شرایط اجرایی مرتبط با این مشخصات سازگار است. اگر اثبات موفق نباشد، این شکست می‌تواند رفتاری مغایر با مشخصات را آشکار کند و به شناسایی نقص اصلی کمک کند. توسعه‌دهندگان می‌توانند مشکل را برطرف کنند و فرایند را تا زمانی که ویژگی‌های مورد نظر اثبات شوند، تکرار کنند.
آنتروپیک هزینه و پیچیدگی تولید اثبات‌ها را از موانع دیرینه گسترش استفاده از این روش دانسته است. اثبات‌ها ممکن است چندین برابر کد اصلی حجم داشته باشند و تهیه آن‌ها به‌طور سنتی مستلزم دانش تخصصی و صرف زمان مهندسی قابل‌توجهی بوده است. این شرکت برای نشان دادن ابعاد چنین دشواری‌ای به هسته سیستم‌عامل seL4 اشاره کرده است.
پیاده‌سازی این هسته به دو نفرـ‌سال کار نیاز داشت، در حالی که فرایند راستی‌آزمایی رسمی آن ۲۰ نفرـ‌سال زمان برد. در گذشته، چنین سرمایه‌گذاری سنگینی باعث شده بود استفاده از راستی‌آزمایی رسمی عمدتاً به سامانه‌های حیاتی محدود بماند؛ از جمله نرم‌افزارهای اویونیک ایرباس.
کار کلود به چالش دیگری نیز پرداخت: تعریف رفتار صحیح برای نرم‌افزارهای موجود. از آنجا که بسیاری از برنامه‌ها مشخصات جامع و بدون ابهامی ندارند، پژوهشگران مجموعه‌آزمایش‌های قابل‌کامپایلِ از پیش موجود را به مشخصات رسمی تبدیل کردند؛ به این صورت که الزام موفقیت همیشگی آزمایش‌ها را در قالب مشخصات کدگذاری کردند. این روش، مشخصات حاصل را با یک مدل عمومی از نحوه اجرای فایل‌های باینری کامپایل‌شده برای RISC-V در لینوکس ترکیب کرد.
به گفته آنتروپیک، این رویکرد به کلود امکان داد رفتار برنامه‌هایی با ده‌ها هزار دستور اسمبلی را در دامنه‌ای از ورودی‌ها و تعاملات احتمالی بررسی کند. این شرکت همچنین گزارش داد که کلود باگ‌هایی را کشف کرده است که با وجود تریلیون‌ها بار اجرای آزمایش، سال‌ها از شناسایی شدن گریخته بودند. این یافته‌ها نشان می‌دهند استدلال رسمی می‌تواند نقص‌هایی را آشکار کند که آزمایش‌های متعارف قادر به شناسایی آن‌ها نیستند؛ هرچند تضمین‌های حاصل همچنان به ویژگی‌های تعریف‌شده و شرایط اجرایی مشخص‌شده در هر اثبات محدود می‌شوند.
آنتروپیک علاوه بر پروژه مربوط به ۱۲۳ کتابخانه، از آزمایش‌های اولیه برای استفاده از روش‌های دیگر راستی‌آزمایی رسمی در مسائل بیشترِ امنیت و توسعه نرم‌افزار نیز خبر داد. این آزمایش‌ها شامل ارزیابی امنیت الگوریتم فشرده‌سازی zlib، اثبات هم‌ارزی رفتاری یک مفسر پایتون نوشته‌شده با زبان راست و بررسی نقص‌های دیرپای موجود در نرم‌افزارهای حیاتی بود.
شرکت تئورم اعلام کرده است که اجرای همین فرایند راستی‌آزمایی را برای پروژه‌های متن‌باز دیگر نیز ارائه می‌دهد. این شرکت همچنین مهارتی برای کلود منتشر می‌کند که هدف آن کمک به توسعه‌دهندگان برای آغاز راستی‌آزمایی کدهای خودشان است. آنتروپیک نیز انتظار دارد استفاده مجدد از اثبات‌های موجود و سازگار کردن آن‌ها با شرایط جدید، هزینه به‌کارگیری روش‌های رسمی را در پایگاه‌های کد مختلف کاهش دهد.