هوش مصنوعی گوگل دیپ‌مایند در چهار هفته، درستی تضمین‌های کلیدی پروتکل سیگنال را اثبات کرد
اگر محصول شما به رمزگذاری مبتنی بر پروتکل سیگنال متکی است، ارائه یک اثبات رسمی که صحت آن با ابزارهای نرم‌افزاری بررسی شده باشد، ادعایی بسیار معتبرتر از استناد به گزارش ممیزی امنیتی است. البته پیش از مطرح کردن چنین ادعایی در معرفی محصول یا ارائه به سرمایه‌گذاران، باید محدوده دقیق این بررسی را بشناسید.
گوگل دیپ‌مایند با استفاده از سامانه هوش مصنوعی AlphaProof Code توانسته است برخی از تضمین‌های امنیتی پروتکل سیگنال را به‌صورت رسمی اثبات کند. این پروتکل، مبنای طراحی رمزگذاری پیام‌رسان سیگنال است و نسخه‌های تغییریافته آن نیز در Google Messages و واتس‌اپ به کار می‌روند. به گزارش WIRED که این هفته منتشر شد، پژوهشگران می‌گویند این فرایند چهار هفته طول کشیده و در بخش‌های بررسی‌شده هیچ آسیب‌پذیری تازه‌ای شناسایی نشده است.
بااین‌حال، این دستاورد یک اثبات مفهومی است، نه تأییدیه‌ای جامع مبنی بر بی‌نقص بودن یک اپلیکیشن پیام‌رسان. بر اساس گزارش منتشرشده درباره مطلب WIRED، دیپ‌مایند کل اپلیکیشن موبایل سیگنال را بررسی نکرده است؛ بلکه پژوهشگران تنها مجموعه‌ای از تضمین‌های مشخص پروتکل را آزموده‌اند، نه تمام اجزای این اپلیکیشن‌ها یا همه شیوه‌هایی را که ممکن است در آن‌ها اختلال امنیتی ایجاد شود.
اثبات رسمی تفاوت اساسی با بازبینی کد دارد. در بازبینی کد، متخصص طراحی و پیاده‌سازی را بررسی می‌کند و درباره درست به نظر رسیدن آن نظر می‌دهد. اما در روش اثبات رسمی، نرم‌افزار به‌صورت خط‌به‌خط و بر اساس مشخصاتی مکتوب، صحت ادعا را بررسی می‌کند. اعتبار نتیجه نیز به همان مشخصات و فرض‌هایی بستگی دارد که اثبات بر مبنای آن‌ها انجام شده است. گزارش‌های منتشرشده جزئیات روشنی درباره مؤلفه‌های بررسی‌شده یا سامانه اثباتی که برای کنترل نتایج به کار رفته، ارائه نمی‌کنند. ما نیز نتوانستیم گزارش رسمی خود دیپ‌مایند را تأیید کنیم. بنابراین، عبارت «امنیت سیگنال اثبات شده است» را باید صرفاً خلاصه‌ای از این ادعای محدود دانست که «ویژگی‌های مشخص‌شده، تحت فرض‌های تعیین‌شده، برقرار هستند».
یکی از جزئیات این پژوهش باعث می‌شود نتیجه آن معتبرتر از یک اعلام موفقیت ساده به نظر برسد. طبق گزارش‌های منتشرشده درباره مطلب WIRED، گروه پژوهشی ابزار خود را روی نسخه‌های قدیمی‌تر سیگنال نیز آزمایش کرد؛ نسخه‌هایی که آسیب‌پذیری‌های آن‌ها از قبل شناسایی و مدت‌ها پیش برطرف شده بود. سامانه توانست این آسیب‌پذیری‌ها را پیدا کند و همچنین نشان داد که آن نسخه‌ها قابلیت اثبات رسمی ندارند. ابزاری که بتواند کد معیوب را رد کند، دقیقاً همان کاری را انجام می‌دهد که از آن انتظار می‌رود.
با وجود استفاده از هوش مصنوعی، نظارت و مشارکت انسان همچنان بخشی از فرایند بود. سوارَت چودوری، پژوهشگر ارشد دیپ‌مایند، در گفت‌وگو با WIRED گفت: «از این نتیجه بسیار هیجان‌زده‌ایم، اما تا زمانی که بتوانیم این روش را به تمام نرم‌افزارهای جهان گسترش دهیم، راه بسیار طولانی در پیش داریم و هدفمان رسیدن به همین نقطه است.»
چرا اثبات تضمین‌های قدیمی همچنان ضروری بود؟
کسی انتظار نداشت طراحی پروتکل سیگنال از اساس دچار مشکل باشد. پژوهش‌های دانشگاهی، از جمله مطالعه دانشگاه آکسفورد در سال ۲۰۱۷ درباره سازوکار Double Ratchet، نقص عمده‌ای در این پروتکل پیدا نکرده بودند. مسئله اصلی کمبود شواهدی بود که نشان دهد کدی که کاربران واقعاً اجرا می‌کنند، با طراحی نظری و مستندات فنی مطابقت دارد. این همان شکافی است که پژوهش جدید به آن می‌پردازد.
بنیاد هوش مصنوعی سودمند (Beneficial AI Foundation) که مکس تگمارک از بنیان‌گذاران آن است، از مسیر دیگری به دنبال حل همین مسئله است. این بنیاد با همکاری سیگنال و پروژه Lean FRO، طرحی به نام Signal Shot را پیش می‌برد که بر پایه زبان Lean توسعه یافته و هدف آن اثبات رسمی صحت پروتکل سیگنال و پیاده‌سازی آن با زبان برنامه‌نویسی Rust است. دستاورد دیپ‌مایند نیز از مسیری متفاوت به همین حوزه وارد شده است.
واقعیت این است که جنبه جالب‌تر ماجرا فراتر از تیتر خبر است. تکمیل چنین کاری در چهار هفته زمان بسیار کوتاهی محسوب می‌شود. بااین‌حال، اثباتی که هوش مصنوعی در تهیه آن مشارکت داشته، تنها به این دلیل ارزشمند است که یک سامانه بررسی مستقل می‌تواند آن را تأیید یا رد کند.
این پیشرفت برای شرکت‌های تولیدکننده نرم‌افزارهای امنیتی چه معنایی دارد؟
اگر کیف پول رمزارزی، یک استارتاپ پیام‌رسان یا هر محصول دیگری مبتنی بر رمزگذاری عرضه می‌کنید، پیام مستقیم این دستاورد آن نیست که سیگنال امن است؛ بسیاری از متخصصان از قبل نیز چنین باوری داشتند. نکته مهم‌تر این است که تهیه اثبات‌های امنیتی قابل بررسی توسط ماشین، آن‌قدر ارزان‌تر و در دسترس‌تر شده که می‌توان انتظار داشت مشتریان و ممیزان امنیتی به‌زودی چنین مدارکی را مطالبه کنند. شرکتی که بتواند مشخصات فنی منتشرشده و اثبات رسمی و تأییدشده‌ای ارائه کند، در مقایسه با شرکتی که صرفاً به ممیزی یک مؤسسه معتبر استناد می‌کند، مزیت رقابتی واقعی خواهد داشت.
البته محدودیت‌های این روش نیز به همان اندازه اهمیت دارند. پروتکل سیگنال کوچک است، پژوهش‌های گسترده‌ای درباره آن انجام شده و مستندات عمومی و مشخصی دارد؛ بنابراین، تقریباً یکی از بهترین نمونه‌ها برای اجرای چنین روشی به شمار می‌رود. در مقابل، بیشتر نرم‌افزارهای تجاری بزرگ‌تر و پیچیده‌ترند و اغلب مشخصات فنی دقیق و منسجمی ندارند که بتوان صحت آن‌ها را بر اساس آن اثبات کرد. خود چودوری نیز تأکید کرده است که تعمیم این روش به تمام نرم‌افزارها هنوز به زمان زیادی نیاز دارد. بنابراین، اینکه استفاده از این رویکرد در سامانه‌های تجاری معمول از نظر هزینه و فایده مقرون‌به‌صرفه باشد، همچنان پرسشی بی‌پاسخ است.