LLM ها تأیید نرم افزار رسمی را در مقیاس بسیار بزرگتر امکان پذیر می کنند

کین لوکاس، انگوس لینچ، لونا تانگ، لوک شامپین، زیگی استرازنیکاس، دینو دیستفانو، هارشیکا آگراوال اویاتار بن اشر، آوا هاول، سامی جوهر، کریس روهلف، نیکولای زلدویچ نیکلاس کارلینی، راجاشری آگراوال، جیسون گروس

اکثر نرم‌افزارها مملو از باگ‌هایی هستند که هوش مصنوعی اکنون می‌تواند به راحتی آن‌ها را پیدا کرده و از آنها سوء استفاده کند. دفاع استاندارد در برابر حملات سایبری دیگر کافی نیست: ما به راه هایی نیاز داریم که ثابت کنیم کد عاری از اشکال است. راستی‌آزمایی رسمی نرم‌افزار می‌تواند این تضمین را ارائه دهد، اما از نظر تاریخی به سال‌ها تلاش متخصص نیاز داشته است و آن را برای اکثر پروژه‌های دنیای واقعی غیرعملی می‌سازد. با این حال، در همکاری با Theorem، نشان می‌دهیم که دیگر اینطور نیست: LLMها اکنون می‌توانند مدارک رسمی را در مقیاس بزرگ تولید کنند، و گردش‌های کاری توسعه نرم‌افزار جدید را که شامل تضمین‌های امنیتی اثبات‌شده است، فعال می‌کنند.

با استفاده از Claude، ویژگی‌های امنیتی را در سطح کد اسمبلی (RISC-V) در بیش از 100 کتابخانه نرم‌افزار منبع باز دنیای واقعی اثبات کردیم. طبق دانش ما، این اولین تلاش در مقیاس بزرگ برای استفاده از هوش مصنوعی برای اعمال تأیید رسمی در نرم افزار تولید در سطح کد اسمبلی است. در حین نوشتن مدارک، کلود همچنین باگهایی را کشف کرد که علیرغم تریلیون‌ها آزمایش، سال‌ها از شناسایی دور مانده بودند. همانطور که قابلیت‌های مدل همچنان در حال بهبود هستند، انتظار داریم تأیید رسمی به بخشی ضروری از توسعه نرم‌افزار ایمن تبدیل شود.

حتی نرم‌افزارهای بالغ و به‌شدت آزمایش‌شده حاوی اشکالاتی هستند و LLM‌ها به طور فزاینده‌ای در یافتن آنها مهارت دارند. هسته لینوکس - یکی از تست‌شده‌ترین نرم‌افزارهای امروزی که بر روی میلیاردها دستگاه در سراسر جهان مستقر شده است - اخیرا بیش از 1000 آسیب‌پذیری فاش شده است. با افزایش توانایی مدل‌های مرزی برای زنجیر کردن باگ‌های به ظاهر خوش‌خیم به اکسپلویت‌های حیاتی، به تکنیک‌هایی نیاز داریم که بتوانند این اشکال‌ها را قبل از اینکه در طبیعت مورد سوء استفاده قرار گیرند، شناسایی و برطرف کنند.

در حالت ایده‌آل، چنین تکنیک‌هایی می‌توانند همه باگ‌ها را پیدا کرده و وصله کنند، و سپس شواهدی ارائه کنند که نشان می‌دهد دیگر چیزی برای یافتن وجود ندارد. تایید رسمی یکی از راه های انجام این کار است. در تأیید رسمی، توسعه‌دهندگان کد خود را به یک مدل ریاضی ترجمه می‌کنند، سپس سعی می‌کنند ثابت کنند که همیشه از مجموعه‌ای از قوانین امنیتی تعریف‌شده پیروی می‌کند. اگر آنها نتوانند این را ثابت کنند، به این معنی است که ممکن است یک اشکال در کد وجود داشته باشد که یک قانون را نقض می کند، و ماهیت شکست نشان می دهد که این اشکال ممکن است چیست.

تکرار این فرآیند (پس از از بین بردن علت خرابی هر بار) در نهایت اثبات می کند که کد فاقد هرگونه اشکالی است که آن قوانین را نقض می کند.

با این حال، تأیید رسمی آسان نیست. اثبات‌ها می‌توانند چندین برابر بزرگ‌تر از کد اصلی باشند و نوشتن آن‌ها به تلاش قابل توجه و مجموعه‌ای از مهارت‌های خاص و بسیار تخصصی نیاز دارد. برای مثال، اجرای هسته سیستم عامل seL4 دو نفر-سال طول کشید، اما تأیید رسمی آن 20 نفر-سال طول کشید. بر این اساس، راستی‌آزمایی رسمی تنها در برنامه‌های واقعا حیاتی، مانند کدهای هوایی ایرباس، عملی بوده است.

اما LLM ها این کار را بسیار آسان تر می کنند. مدل‌های مرزی اکنون می‌توانند به‌طور کاملا مستقل برای نرم‌افزارهای دنیای واقعی اثبات صحت تولید کنند. برای نشان دادن این موضوع، از کلود خواستیم تا ویژگی‌های امنیتی مفیدی را در 123 کتابخانه منبع باز ثابت کند، از جمله نشان دهد که برخی از مصنوعات اجرایی آنها هرگز نمی‌توانند تحت شرایط خاص خراب شوند.

به طور خاص، کلود ثابت کرد که این برنامه‌ها همیشه به‌طور معمول بدون ایجاد خطاهای ایمنی حافظه یا اظهارات ناموفق، برای هر ورودی کمتر از 64 مگابایت و هر پاسخ سیستم‌عامل لینوکس (OS) مدل‌سازی‌شده و طرح‌بندی حافظه، تحت مفروضات خاصی (یعنی اینکه برنامه به‌عنوان یک threaded single-threaded Static memory با استفاده از یک باینری باینری لینوکس SCV با یک سیستم‌عامل باینری SCRI ثابت اجرا می‌شود) خارج می‌شوند. این هنوز تا رفع تمام اشکالات احتمالی فاصله دارد، اما ما را بسیار نزدیکتر از قبل می کند و نقشه راه را برای رسیدن به این هدف فراهم می کند.

ما زیرمجموعه‌ای از این اثبات‌ها را منتشر می‌کنیم تا هر کسی بتواند آن‌ها را تأیید و مجددا استفاده کند، همراه با معنای RISC-V و OS. Theorem، همکار ما در این پروژه، اجرای همان خط لوله را برای سایر پروژه‌های منبع باز نیز پیشنهاد می‌کند و در حال انتشار یک مهارت Claude است تا به توسعه‌دهندگان کمک کند تا با تأیید کد خود شروع کنند.

راستی‌آزمایی رسمی حوزه وسیعی با روش‌های متعدد است. در زیر، ما همچنین کاوش‌های اولیه خود را با استفاده از روش‌های تأیید رسمی دیگر برای تسریع سایر وظایف امنیتی یا توسعه نرم‌افزار، مانند ارزیابی امنیت الگوریتم فشرده‌سازی zlib، اثبات معادل‌سازی رفتاری یک مفسر پایتون نوشته شده در Rust، و ریشه‌یابی باگ‌های طولانی مدت در نرم‌افزارهای حیاتی، شرح می‌دهیم.

راه پیش رو برای تأیید رسمی امیدوارکننده است. با هوشمندتر شدن مدل ها، هزینه نوشتن مدارک در حال کاهش است. علاوه بر این، با رسمی شدن کد بیشتر و استاندارد شدن روش‌های دستیابی به تضمین‌های امنیتی، امکان استفاده مجدد یا تغییر اثبات‌ها در پایه‌های کد، هزینه را کاهش می‌دهد. ما همه برنامه‌نویس‌ها را تشویق می‌کنیم تا تأیید رسمی را با LLM‌ها بررسی کنند - به‌خصوص آن‌هایی که قبلا آن را با مدل‌های کم‌توان‌تر امتحان کرده‌اند و متوجه شده‌اند که کار نمی‌کند.

در ادامه این پست، آزمایش‌های تأیید رسمی خود را با جزئیات بیشتری پوشش می‌دهیم.

برای اثبات درستی یک نرم افزار، ابتدا باید بگوییم که «درست» به چه معناست. صحت با مشخصات (مشخصات) تعریف می شود. در برخی از برنامه ها، راه روشنی برای مشخص کردن رسمی رفتار مورد نظر برنامه وجود دارد. برای مثال، رمزگشای PNG دنباله ای از بایت ها را می گیرد و (به دنبال RFC 2083) این بایت ها را در تصویر مربوطه رمزگشایی می کند. اما برای اکثر برنامه ها، همه چیز چندان ساده نیست.

"صحیح" بودن یک ویرایشگر متن یا یک مرورگر وب به چه معناست؟ دشواری دستیابی به یک مشخصات جامع و بدون ابهام مانع مهمی برای تأیید نرم افزار در مقیاس بزرگتر است.

برای پرداختن به این موضوع برای کد موجود در کتابخانه‌های منبع باز که به دنبال اثبات آن بودیم، با استفاده از یک مدل کلی از معنای اجرای هر باینری کامپایل‌شده RISC-V در لینوکس، رویکردی را اتخاذ می‌کنیم که مجموعه‌های آزمایشی کامپایل از قبل موجود آن‌ها را به صورت خودکار به یک مشخصات رمزگذاری کنیم.

از نظر تاریخی، با توجه به پیچیدگی ذاتی نوشتن یک اثبات که می تواند همه رفتارها و تعاملات ممکن ده ها هزار دستورالعمل اسمبلی را در هر ورودی (و این واقعیت که در نتیجه اثبات ها بسیار بزرگ هستند) در بر گیرد و استدلال کند، اثبات چنین مشخصاتی غیرقابل حل بود. این همان جایی است که LLM های امروزی وارد می شوند: ایجاد میلیون ها خط کد برای دستیابی به یک هدف کاملا تعریف شده، کاری است که LLM ها برای آن بسیار مناسب هستند.

برای این پروژه، ما با تست های فازی شروع کردیم. در این آزمایش‌ها، توسعه‌دهندگان یک نقطه ورودی 2 را در کد خود می‌نویسند که ورودی‌ها را دریافت می‌کند، به طوری که هر ورودی که باعث خرابی شود، اشکالی است که نویسندگان به آن اهمیت می‌دهند. سپس فازر، یک موتور آزمایش، تعداد زیادی ورودی نیمه تصادفی و جهش یافته را در نقطه ورودی تولید می کند تا یک اشکال را پیدا کند (تجسم شده در شکل 1). هرچه یک فازر بیشتر اجرا شود، باگ های بیشتری را می تواند پیدا کند. اما این ذاتا یک فرآیند brute-force است، بدون هیچ تضمینی برای اعمال هر مسیر کد ممکن، صرف نظر از اینکه چند ورودی را امتحان می‌کنید.

برای یافتن تمام اشکالاتی که توسط یک تست فازی ظاهر می شدند، ما تست فاز را به مشخصاتی تبدیل کردیم که روی دستورالعمل های کامپایل شده RISC-V تعریف شده است. این مشخصات می گوید که تست فاز برای هیچ ورودی کمتر از 64 مگابایت خراب نمی شود. 3 اگر کلود بتواند این مشخصات را اثبات کند، آزمایش فازی در RISC-V غیرضروری می‌شود: مبهم کردن آن نقطه ورودی هرگز هیچ اشکالی را پیدا نمی‌کند.

ما این کار را برای صدها پروژه در ابتکار Google OSS-Fuzz انجام دادیم که آزمایش فازی مداوم را برای پروژه‌های منبع باز واجد شرایط ارائه می‌دهد. OSS-Fuzz حاوی هزاران نقطه ورودی است که توسط توسعه‌دهندگان نوشته شده است که با خراب شدن به دنبال ویژگی‌های کد شکسته می‌گردند (مثلا در یک ادعای ناموفق). OSS-Fuzz به طور خودکار برنامه‌های C و C++ را با AddressSanitizer 4 (ASan) ابزار می‌کند، و باعث می‌شود هر زمان که حافظه به درستی دسترسی نداشته باشد، از کار بیفتد (که یکی از دلایل اصلی آسیب‌پذیری‌های نرم‌افزاری است). مشخصات گسترده ای مانند ایمنی حافظه تقریبا برای همه نرم افزارها اعمال می شود.

در طول چند هفته، کلود با موفقیت باگ‌هایی را که پیدا کرده بود اصلاح کرد و سپس ثابت کرد که در هیچ ورودی (تا 64 مگابایت) برای 239 نقطه ورودی در 123 کتابخانه مختلف OSS-Fuzz هیچ خرابی وجود ندارد. این اثبات‌ها بر روی دستورالعمل‌های کامپایل‌شده RISC-V (یعنی باینری‌های اجرایی) کار می‌کنند، و حدود 180 میلیون خط Rocq را شامل می‌شوند که یک اثبات معمولی تا حدود 600000 خط برای ارائه تضمین‌های امنیتی روی باینری‌هایی با طول متوسط ​​18000 دستورالعمل RISC-V است.

این اثبات‌ها با ترجمه کد اسمبلی RISC-V به یک مدل ریاضی با استفاده از دستورات RISC-V قضیه و معناشناسی فرآیند لینوکس ساخته می‌شوند. این بدان معناست که این شواهد در حال حاضر فرض می‌کنند که برنامه به‌صورت یک باینری استاتیک تک رشته‌ای با بودجه حافظه ثابت بر روی یک CPU RISC-V با استفاده از سیستم عامل لینوکس اجرا می‌شود. گسترش دامنه این اثبات ها به خوبی در دسترس است، زیرا مستلزم استانداردسازی معنایی برای معماری های مونتاژ بیشتر و سایر فرآیندهای سیستم عامل است. نگاه یک متخصص در مورد شواهدی که کلود نوشته است را ببینید.

در حالی که این حجم عظیمی از کد اثبات است، تقریبا هیچ یک از آن‌ها نیاز به بررسی دستی ندارند. بررسی‌کننده اثبات Rocq تضمین می‌کند که مشخصات به درستی توسط اثبات برآورده شده است. در نتیجه، تنها مصنوعاتی که یک توسعه دهنده باید به آنها اعتماد کند عبارتند از:

این بدان معنا نیست که این کتابخانه ها فاقد اشکال هستند. در عوض، به این معنی است که هر گونه اشکال باقیمانده یا باید در مصنوعات ذکر شده در بالا یافت شود یا خارج از محدوده اثبات کلود است. سخت کردن آن مولفه‌های مطمئن هنوز احتمالا باگ (روک، RISC-V، و معناشناسی لینوکس) بی‌اهمیت نیست، اما کار بسیار قابل انجام‌تری نسبت به اشکال‌زدایی هر خط کدی است که مدارک کوچک‌شده پوشش می‌دهند – به خصوص که این رویکرد می‌تواند تعداد دلخواه پروژه‌های مورد اعتماد را بدون افزایش اندازه مؤلفه‌ها ایمن کند.

ما از تأیید مستقل شواهد خود استقبال می کنیم و اصلاح رویکرد خود را تشویق می کنیم. برای این منظور، ما مؤلفه‌های مورد اعتماد (بالا) ساخته شده برای این پروژه را منتشر می‌کنیم که قبلا عمومی نیستند. اثبات کامل Rocq کلود برای تست های فازی که نیازی به وصله نداشتند. و مشخصات دیگر تست های فازی که ما قادر به اثبات آن نبودیم.

در بالا، نشان دادیم که می‌توانید بسیاری از آزمایش‌های نوشته شده توسط توسعه‌دهنده کتابخانه‌های منبع باز (تست‌های فاز) را به مشخصاتی تبدیل کنید که کلود می‌تواند ثابت کند، گاهی اوقات پس از اصلاح باگ‌های باقی‌مانده که پیدا کرده، همیشه موفق خواهند بود. به همین دلیل، روند تلاش برای اثبات این مشخصات صدها اشکال را کشف کرد.

بسیاری از اشکالات در طول تلاش های کلود برای اثبات صدها نقطه ورود ظاهر شد. برای اطمینان از اینکه کلود مجبور نیست هر بار که این اتفاق می‌افتد برای یک انسان متوقف شود، به کلود اجازه دادیم اشکالاتی را که پیدا کرده بود برطرف کند: کد را اصلاح کرد که باعث شد مشخصات با آن کد وصله‌شده دوباره تولید شود و سپس کلود به اثبات آن مشخصات جدید ادامه داد. 6

بسیاری از اشکالاتی که ما پیدا کردیم، مواردی هستند که بعید است یک fuzzer هرگز آنها را پیدا کند. Fuzzerها ورودی‌های کوچک را تغییر می‌دهند که معمولا 1 مگابایت محدود می‌شوند و معمولا به پوشش کد برای هدایت آنها به سمت اشکالات متکی هستند. کلود در حین اثبات یک نقطه ورودی در یک کتابخانه، در نسخه‌ای از یک کمپرسور خود، یک زیر جریان شمارنده پیدا کرد که منجر به نوشتن خارج از محدوده می‌شد، اما فقط در ورودی‌های حدود 20 مگابایت که دارای یک طرح‌بندی خاص و کمیاب بودند.

سایر اشکالات عبارتند از خواندن خارج از کران در یک رمزگشای تصویر که به ورودی 64 مگابایت و بیش از 2 گیگابایت حافظه نیاز داشت، خواندن خارج از کران در کتابخانه دیگری که به دنباله خاصی از تماس ها در دو دسته به یک فایل نیاز داشت، و کشف مجدد CVE-2026-56132 که در libexs نیاز داشت. کلود همچنین باگ های منطقی را پیدا کرد که هرگز خراب نمی شوند. برای مثال، در حالی که ثابت می‌کرد یک کتابخانه از نظر حافظه ایمن است، متوجه شد که ویژگی محدود کردن فایل‌هایی که برنامه می‌تواند بارگذاری کند همیشه اعمال نمی‌شود.

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

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

اگر ویژگی ثابت نباشد، برنامه خراب می‌شود—بنابراین اثبات اینکه تست هرگز خراب نمی‌شود معادل اثبات خود ویژگی است.

حتی زمانی که ویژگی‌ها مستقیما توسط توسعه‌دهنده مشخص نشده باشند، این ممکن است رخ دهد. به عنوان مثال، برای اینکه کلود بتواند اثبات OSS-Fuzz خود را برای cpp-httplib کامل کند، لازم بود که احتمال سرریز پشته به دلیل بازگشت بیش از حد در تخریبگر std::set را رد کنیم. این عمق بازگشتی با حداکثر عمق یک درخت محدود می‌شود، بنابراین کلود باید ثابت می‌کرد (در کد ماشین!) که الگوریتم متعادل‌سازی مجدد درخت قرمز-سیاه libc++ به درستی بهینه‌سازی شده است تا عمق درخت را از نظر لگاریتمی محدود نگه دارد.

تأیید رسمی یک دامنه گسترده است. مثال fuzz-test-to-proof در بالا یکی از نمونه‌های LLM است که تأیید رسمی را با اعمال مستقیم اثبات‌ها در کد ماشین به طور گسترده‌تر قابل استفاده‌تر می‌کند.

ما همچنین شاهد موفقیت در استفاده از LLM با تأیید رسمی به روش‌های دیگر بوده‌ایم. به عنوان مثال، از کلود خواستیم تا مشخصات رسمی RFC 1950 را بنویسد، سند فنی که فرمت فایل فشرده سازی zlib را تعریف می کند. سپس، کلود را مجبور کردیم که ثابت کند پیاده سازی zlib در هسته لینوکس به درستی آن مشخصات را پیاده سازی می کند. همانند مثال‌های بالا، کلود این ویژگی را در سطح باینری ثابت کرد، به جز اینکه به‌جای RISC-V، کلود مستقیما باینری کامپایل‌شده با x86 را با استفاده از معناشناسی رسمی X86 ISA تولید شده توسط کلود (و به شدت آزمایش‌شده) ثابت کرد.

7 سپس این فرآیند را برای نیم دوجین کتابخانه پرکاربرد دیگر تکرار کردیم. در طول مسیر، برخی از اشکالات جزئی (غیرقابل بهره برداری) را در موارد گوشه ای یافتیم که در مراحل بالادستی پرونده هستند. ما از این تمرین دو نتیجه می گیریم: (1) این پایگاه های کد بسیار خوب آزمایش شده در حال حاضر تقریبا کاملا صحیح هستند، و (2) می توان ویژگی های صحت انتها به انتها را در مورد پایگاه های کد واقعی موجود ثابت کرد.

در آزمایش دیگری، ما از کلود خواستیم که یک مفسر برای زیرمجموعه بزرگی از Python در Rust ایجاد کند و ثابت کند (با استفاده از Verus، یک ابزار تأیید برای Rust) که به معنای CPython که در یک مقاله دانشگاهی آمده است، پایبند است. سپس پایبندی به رفتار CPython را به صورت تجربی اندازه‌گیری کردیم، با اجرای بیش از 1.7 میلیون برنامه پایتون که به‌طور تصادفی تولید شده بودند، رفتاری مشابه با CPython در 99.95٪ از تست‌ها یافتیم، با تفاوت‌های آزمون باقی مانده به عنوان موارد گوشه‌ای شناخته شده غیرقابل تعجب.

ما همچنین مشکلاتی را در چندین برنامه کاربردی پرکاربرد و حیاتی از طریق تلاش‌های تأیید رسمی ویژگی‌های امنیتی ساده پیدا کردیم. در یکی از آنها، یک باگ منطقی ناشناخته را کشف کردیم که بیش از یک دهه پنهان بود. در طی تلاشی برای تأیید یک پی‌دی‌اف‌خوان پرکاربرد، ما در یک هفته به همان تعداد باگ امنیتی که معمولا در یک سال گزارش می‌شود، پیدا کردیم.

برای جزئیات بیشتر در مورد برخی از این تلاش ها به پیوست مراجعه کنید.

یکی از محدودیت‌های کلیدی تأیید رسمی با کمک LLM این است که اثبات می‌تواند صدها میلیون توکن را برای تولید نیاز داشته باشد. اگر هدف ما این باشد که این روش ها را برای کل اکوسیستم نرم افزاری در دسترس قرار دهیم، کارایی هزینه بسیار مهم است. خوشبختانه، دلایل قانع‌کننده‌ای برای انتظار بهبود کارایی وجود دارد.

ما 36 کار راستی‌آزمایی کوچک را از کد OSS-Fuzz واقعی ساختیم. Opus 5.5 نیمی از آنها را با حدود 40٪ توکن کمتر از Opus 5 ثابت می کند. ما انتظار داریم که این روند ادامه یابد زیرا مدل ها برای کارهای تأیید طولانی مدت آموزش می بینند.

هنگامی که نمایندگان به طور جداگانه کار می کنند، اغلب در نهایت تلاش های زیادی را تکرار می کنند. اثبات‌ها، مانند نرم‌افزار، به‌صورت بازگشتی از برهان‌های کوچک‌تر ساخته می‌شوند – و هرچه این اثبات‌ها کوچک‌تر باشند، تمایل بیشتری به استفاده مجدد دارند. برای اندازه‌گیری تأثیر این امر، به مأموران اجازه می‌دهیم که مدارک یکدیگر را در حین کار بر روی اثبات اهداف خود کپی کنند. هنگام دسترسی به این فضای کاری مشترک، نمایندگان به 17 درصد توکن کمتری نسبت به زمانی که به تنهایی کار می کردند نیاز داشتند، و برخی از نمایندگان حتی پس از شکست قبلی در تلاش انفرادی موفق شدند.

ما در طول تلاش خود برای اثبات OSS-Fuzz، پدیده مشابهی را در مقیاس مشاهده کردیم. بیشتر یک اثبات مربوط به کدهایی است که هر برنامه حاوی آن است (مخصوصا مقداردهی اولیه زمان اجرا C و AddressSanitizer)، بنابراین برنامه های بسیار متفاوت می توانند به طور قابل توجهی با اثبات همپوشانی داشته باشند. تیم‌های عامل با کپی کردن اثبات نهایی تیم دیگری و سپس تطبیق آن با برنامه خود از این مزیت استفاده کردند (شکل 6).

این قابلیت استفاده مجدد از اثبات ها به این صورت است که Mathlib، یک کتابخانه مشترک ریاضیات رسمی در Lean، به نزدیک به 300000 قضیه ارائه شده توسط بیش از 700 مشارکت کننده افزایش یافته است: هر اثبات جدید بر روی بدنه کار موجود استوار است. ما مجموعه‌ای از شواهد مشابه را در طول تلاش OSS-Fuzz خود جمع‌آوری کردیم، که برخی از آنها را در نسخه خود گنجانده‌ایم (شواهدی را منتشر نمی‌کنیم که ممکن است یک باگ اصلاح‌نشده را در نرم‌افزار منبع باز نشان دهد).

همانطور که از این آزمایش‌های اولیه فارغ‌التحصیل می‌شویم، به یک استراتژی برای تأیید حجم عظیم نرم‌افزار موجود نیاز داریم، که از مهم‌ترین وابستگی‌ها شروع می‌شود. همانطور که نشان دادیم، با استفاده از مشخصات عمومی و کار در سطح باینری، می‌توان این کار را در مقیاس به دست آورد، و نیاز به بازنویسی کل پایگاه‌های کد به زبان دیگر را کنار گذاشت.

این رویکرد همچنین استفاده مجدد از اثبات‌ها را در سطح بسته‌بندی تسهیل می‌کند، به این معنی که هر وابستگی فقط باید یک بار تأیید شود. وابستگی‌ها از قانون قدرت پیروی می‌کنند: اثبات حتی مجموعه کوچکی از کتابخانه‌های مشترک، بخش عظیمی از نرم‌افزار را امکان‌پذیر می‌کند. برای جزئیات بیشتر، نقشه راه قضیه را برای تأیید کلیت اکوسیستم Nix، که شامل زیرساخت های حیاتی مانند glibc، OpenSSL و cURL است، ببینید.

در عمل، تأیید رسمی گاهی اوقات می تواند کمتر از آنچه ما می خواهیم در مورد امنیت کد ثابت کند.

"رسما تایید شده" به معنای "بدون اشکال" نیست. کلود می تواند اثباتی بنویسد که نشان دهد رفتار یک برنامه کامپایل شده الزامات یک مشخصات رسمی را برآورده می کند (که توسط یک بررسی کننده اثبات خارجی تأیید می شود). با این حال، یک بررسی کننده اثبات نمی تواند به شما بگوید که آیا مشخصات شما با واقعیت مطابقت دارد یا خیر. برای مطابقت با واقعیت، مشخصات باید به درستی همه چیز را در مورد ماشین واقعی که برنامه تأیید شده روی آن اجرا می‌کند، شامل CPU و سیستم عامل، مدل‌سازی کند. وقتی اشکالات در کد تأیید شده ظاهر می شوند، به این دلیل است که مشخصات یا معنایی فرضی دستگاه با واقعیت متفاوت است.

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

ماشین واقعی کاری را انجام می دهد که مدل آن را توصیف نمی کند. شواهد ما در مورد باینری های تک رشته ای و استاتیک RISC-V است که در برابر musl libc متصل شده اند. با این حال، اکثر مردم این کتابخانه ها را بر روی x86 یا ARM اجرا می کنند و به صورت پویا آنها را با glibc پیوند می دهند. برای از بین بردن این شکاف، به مدل‌های سیستمی نیاز داریم که بیشتر شبیه سیستم‌های مستقر شده باشند. به عنوان مثال، گامی در جهت این امر تولید معنایی دقیق برای x86 است.