‏اتاقی پر از باگ: نقشه‌ی ساده‌ی ابزارهای درستی کد

جو هلرستاین تو این مقاله یه تصویر ساده برای ابزارهای درستی نرم‌افزار پیشنهاد می‌ده: برنامه‌ت یه اتاق پر از باگه. کف اتاق کد اسمبلیه و سقفش یه اثبات رسمی که برنامه دقیقا طبق مشخصاتش کار می‌کنه. هرچی بین کف و سقفه، جای باگ‌هاست. به گفته‌ی نویسنده باگ‌ها دو جورن: باگ‌هایی که قانون‌های عمومی رو می‌شکنن (مثل type safety و memory safety) و باگ‌هایی که قانون‌های مخصوص برنامه‌ی تو رو زیر پا می‌ذارن، مثلا «هر رأی‌دهنده فقط یه بار رأی بده».

راه اول correct by construction هست، یعنی زبان اصلا برنامه‌ای که یه قانون عمومی رو بشکنه کامپایل نمی‌کنه. این کار کف اتاق رو بالا می‌بره. اول type systemها اومدن، بعد Rust با borrow checker جلوی باگ‌های حافظه رو گرفت. مایکروسافت سال ۲۰۱۹ گفته بود حدود ۷۰ درصد CVEهای امنیتی‌ش از همین دسته‌ست. لایه‌ی بعدی که تیم نویسنده روش کار می‌کنه Hydro هست که جلوی Heisenbugهای سیستم‌های توزیع‌شده رو می‌گیره (یعنی باگ‌هایی که به ترتیب پیام‌ها و زمان‌بندی بستگی دارن و سخت تکرار می‌شن).

تو Hydro جاهایی که رفتار برنامه واقعا به محیط بستگی داره با کلمه‌ی کلیدی nondet! علامت می‌خورن و بقیه‌ی کد ذاتا قطعیه. راه دوم correct by verification هست: کد واقعی رو با مشخصات حاشیه‌نویسی می‌کنی و ابزاری مثل Verus، Prusti، Dafny یا Stainless با یه SMT solver ثابت می‌کنه کد درسته، وگرنه build شکست می‌خوره. هزینه‌ش نوشتن مشخصات و صبر برای solver هست و طبق قضیه‌ی Rice هم مسئله در حالت کلی حل‌نشدنیه، ولی هر تیکه که اثبات بشه دیگه تست نمی‌خواد.

هرچی باقی بمونه با تست‌های پیشرفته گشته می‌شه که نویسنده بهشون می‌گه یه «توری». model checkerها مثل TLA+ و P همه‌ی حالت‌ها رو تو یه محدوده‌ی کوچیک می‌گردن، پس بیرون اون محدوده سوراخه. fuzzerها و property-based testerها مثل QuickCheck، Hypothesis و proptest ورودی تصادفی می‌سازن و AFL با دنبال کردن مسیرهای کد جست‌وجو رو هدفمندتر می‌کنه. ابزارهای شبیه‌سازی مثل Shuttle، Turmoil، HydroSim و Antithesis هم زمان‌بندی‌های بدشانس رو قابل تکرار می‌کنن.

انتقاد اصلی نویسنده به ابزارهاییه که یه مدل جدا رو چک می‌کنن، مثل TLA+، P، Alloy یا اثبات‌هایی تو Lean و Rocq. مدل به یه زبان مخصوص نوشته می‌شه و سیستم واقعی به Java یا Go. هیچ‌چیز تضمین نمی‌کنه این دو با هم بخونن و با گذشت زمان کد از مدل دور می‌شه. یعنی model checker هنوز می‌گه مشکلی نیست، در حالی که سیستمی که توصیف می‌کنه شش ماهه دیگه وجود نداره.

راه‌حل نویسنده اینه که خود کد اصلی چک بشه. تو Hydro همون کدی که تو production اجرا می‌شه رو HydroSim بررسی می‌کنه و invariantها همون unit testهای معمولی‌ان. HydroSim هر unit test رو زیر همه‌ی ترتیب‌ها و از دست رفتن پیام‌هایی که type system مجاز دونسته اجرا می‌کنه و چون بقیه‌ی کد قطعیه، کل وقتش رو روی بخش‌های nondet! می‌ذاره.

نکات کلیدی:

• سه راه برای کم کردن باگ: correct by construction، correct by verification و تست‌های پیشرفته
• Rust جلوی باگ‌های حافظه رو می‌گیره که طبق گزارش ۲۰۱۹ مایکروسافت حدود ۷۰ درصد CVEها بودن
• Verus، Prusti، Dafny و Stainless کد واقعی رو با SMT solver اثبات می‌کنن
• model checkerهایی مثل TLA+ و P فقط یه محدوده‌ی کوچیک از حالت‌ها رو کامل می‌گردن
• ابزارهایی که مدل جدا چک می‌کنن با تغییر کد اصلی از واقعیت دور می‌شن
• HydroSim خود کد production رو با unit testهای معمولی و زیر همه‌ی ترتیب‌های مجاز چک می‌کنه