در سال‌های اخیر، تمرکز بسیاری از شرکت‌های امنیتی بر استفاده از مدل‌های زبانی برای بازبینی کد (Code Review) بوده است. اما رویکرد جدید نشان می‌دهد که پتانسیل واقعی هوش مصنوعی، پیش از شروع بازبینی کد و در مرحله ساخت ابزارهای سفارشی و مدل‌های رسمی (Formal Models) نهفته است.
چالش‌های تحلیل ماشین‌های پشته‌ای (Stack-Machine)
در بررسی اخیر یک ماشین مجازی Zero-Knowledge (zkVM) به نام Miden، تیم تحلیل با چالش‌های جدی روبرو بود. این سیستم از زبان اسمبلی اختصاصی (MASM) استفاده می‌کند که در آن ورودی‌ها و خروجی‌های دستورات به صورت ضمنی از طریق پشته (Stack) مدیریت می‌شوند. نبود ابزارهای توسعه مانند IDE، Linter و LSP Server، تحلیل دستی کد را بسیار دشوار می‌کرد.
توسعه اکوسیستم ابزاری با کمک AI
برای غلبه بر این محدودیت‌ها، از مدل‌های AI (مانند Claude و Codex) برای ساخت ابزارهای زیر در بازه زمانی شش ماهه استفاده شد:
- LSP Server: ایجاد یک سرور پروتکل زبان برای VS Code جهت فراهم کردن قابلیت‌هایی نظیر Syntax Highlighting و Goto Definition.
- Decompiler: توسعه یک دکامپایلر برای تبدیل کدهای MASM به شبه‌کد (Pseudocode) جهت درک بهتر جریان داده و کنترل.
- Static Analysis Engine: پیاده‌سازی موتور تحلیل استاتیک بر پایه تفسیر انتزاعی (Abstract Interpretation) برای شناسایی نقص‌های منطقی.
یافته‌های امنیتی و نتایج عملی
استفاده از این ابزارهای تولید شده توسط AI منجر به شناسایی بیش از ۴۰۰ نقطه ضعف در اعتبارسنجی نوع داده‌ها (Type Validation) شد. مهم‌ترین یافته، یک آسیب‌پذیری با شدت بالا (High-Severity) در تابع mod_12289 بود. در این مورد، یک مقدار ورودی توسط Prover ارائه می‌شد که به دلیل عدم اعتبارسنجی، امکان جعل امضاهای Falcon و سرقت وجوه از حساب‌های کاربران را فراهم می‌کرد.
مدل‌سازی رسمی با Lean
علاوه بر تحلیل استاتیک، از AI برای ترجمه کدهای MASM به زبان Lean (یک دستیار اثبات یا Proof Assistant) استفاده شد. این فرآیند منجر به تولید ۹۵ اثبات صحت (Correctness Proofs) شد که توسط هسته Lean تایید شدند. این مدل‌سازی رسمی توانست دو باگ بسیار پیچیده در عملیات چرخش ۶۴ بیتی (rotr) و ضرب ۲۵۶ بیتی (wrapping_mul) را شناسایی کند که حتی تست‌های واحد (Unit Tests) نیز قادر به یافتن آن‌ها نبودند.
تغییر پارادایم در اقتصاد ممیزی
تفاوت اصلی امروز با دو سال پیش این است که هزینه توسعه ابزارهای اکتشافی (Exploratory Tools) به شدت کاهش یافته است. در گذشته، اختصاص زمان برای ساخت ابزارهای سفارشی برای هر پروژه توجیه اقتصادی نداشت، اما اکنون با کمک Agentهای هوشمند، هزینه این پروژه‌ها تنها به مقدار مصرف Tokenها محدود شده و بازدهی آن‌ها در شناسایی باگ‌های بحرانی، بسیار چشمگیر است.
