کد AlphaProof

چگونه محققان Google DeepMind یک چارچوب عاملی جدید ساختند که به طور رسمی کد پروتکل رمزنگاری سیگنال را تأیید می کرد - مدت هاست که به عنوان یک چالش امنیتی بزرگ شناخته می شود.

امروز، ما نقطه عطفی در امنیت نرم‌افزاری به اشتراک می‌گذاریم که مدت‌ها به عنوان یک چالش بزرگ شناخته می‌شد: محققان Google DeepMind عوامل هوش مصنوعی را راهنمایی کردند تا ویژگی‌های امنیتی کلیدی کد واقعی زیربنای پروتکل سیگنال را به صورت ریاضی اثبات کنند، فناوری که از میلیاردها مکالمه خصوصی در برنامه‌هایی مانند Signal و Google Messages محافظت می‌کند.

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

کار ما اولین باری است که از هوش مصنوعی برای تأیید رسمی یک پروتکل رمزنگاری گسترده در این عمق استفاده شده است. همچنین این اولین بار است که اجرای پروتکل گسترده ای مانند این به طور رسمی با هر روشی، با یا بدون هوش مصنوعی تأیید می شود.

AlphaProof Code یک چارچوب عامل چند LLM است که کار تأیید رسمی را به روشی که یک تیم تحقیقاتی انجام می دهد تقسیم می کند: متخصصان انسانی با هوش مصنوعی کار می کنند تا تصمیم بگیرند چه چیزی را ثابت کنند، و گروهی از عوامل هوش مصنوعی این کار را انجام می دهند.

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

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

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

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

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

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

در AlphaProof Code، عوامل هوش مصنوعی به کاربران کمک می‌کنند تا یک مشخصات را بنویسند، سپس به طور مستقل ثابت کنند که پیاده‌سازی با آن مطابقت دارد. هر مدرکی توسط Lean بررسی می شود تا کار نمایندگان را تأیید کند.

Ehren Kret، مدیر ارشد فناوری سیگنال گفت: در حالی که تأیید رسمی قبلی بر بخش‌های کوچک‌تری از کد متمرکز بود، رویکرد Google DeepMind گسترش قابل توجهی را امکان‌پذیر می‌کند. «استفاده از عوامل هوش مصنوعی برای ترجمه کد زنده به قضایای ناب معتبر، یک پیشرفت بزرگ است. با افزایش تهدیدات امنیتی مبتنی بر هوش مصنوعی، تأیید دقیق اجرای پروتکل سیگنال به ما اطمینان بیشتری نسبت به تضمین حریم خصوصی کدمان می‌دهد.

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

دستیابی به این چالش طولانی مدت نشان می دهد که چگونه هوش مصنوعی می تواند تضمین امنیتی نخبگان را برای مشاغل، دولت ها و زیرساخت های حیاتی به ارمغان بیاورد و به دفاع در برابر تهدیدات سایبری عامل محور کمک کند.

تأیید رمزنگاری اصلی سیگنال، زمینه ای را برای ایمن سازی سایر سیستم های حیاتی، از سیستم عامل دستگاه پزشکی گرفته تا نرم افزار شبکه برق، فراهم می کند.

مقیاس بندی این تکنیک ها مستلزم تحقیقات مداوم است. همراه با عوامل دفاعی خودکار مانند CodeMender، تأیید رسمی می‌تواند به مقابله با سرعت و مقیاس تهدیدات سایبری مدرن برای ایجاد نرم‌افزاری با اثبات ریاضی مبنی بر کارکرد محافظت‌های آن کمک کند.

ما مصنوعات راستی‌آزمایی رسمی خود را برای استفاده جامعه منبع باز می‌گیریم. مقاله فنی زیر را بخوانید.

این تحقیق توسط Swarat Chaudhuri، Andrew Ferraiuolo، Anton Kovsharov، Tej Chajed، Sam Schlesinger، Karn Seth، Jonathan Katz، Charles Sutton و Pushmeet Kohli توسعه یافته است.

ما از اریک ویزر برای کمک به کد منبع باز، اوون جونز برای پشتیبانی مدیریت برنامه و مارتین آبادی، کریستوفر هنسون، کاترینا هریستوا، هنریک میکالوسکی، جاناتان پروتزنکو و جورج تسوکالاس برای بحث های مفید تشکر می کنیم. ما از Rolfe Schmidt، Michael Rosenberg و Ehren Kret از Signal برای بازخوردشان در مورد روش‌شناسی ما تشکر می‌کنیم. همچنین از تولسی دوشی، فور فلین، کیت اولشوسکا، آلیسیا هوانگ، اندی لیو، بنوا شیلینگز، رالوکا آدا پوپا، ملوین جانسون، کورای کاووکچو اوغلو، دمیس حسابیس و ساندار پیچای برای حمایت از پروژه تشکر می کنیم.