VUPER: Verified ASN.1 UPER Parser
تقدم هذه الورقة VUPER، وهو إطار عمل يقوم بتوليد أدوات تحليل وتسلسل (parsers and serializers) لبروتوكول ASN.1 UMP، تكون محققة رسمياً ودقيقة على مستوى البت، والتي استُخدمت للكشف عن 20 نوعاً من التناقضات والثغرات الأمنية الملموسة في أدوات تحليل شائعة مفتوحة المصدر وتجارية من خلال الاختبار الديناميكي على بروتوكولات 5G وV2X.
البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل
تخيل الإنترنت وهواتفنا المحمولة كمدينة ضخمة وصاخبة حيث تنتقل مليارات الرسائل بين المباني كل ثانية. وللحفاظ على سير العمل في هذه المدينة، تحتاج هذه الرسائل إلى لغة عالمية حتى تتمكن هاتف في نيويورك من التحدث مع برج في طوكيو دون ارتباك. هذه اللغة تسمى ASN.1، وهي تشبه القواعد والمفردات التي تخبر الحواسيب بدقة كيفية تعبئة المعلومات في صناديق رقمية صغيرة وفعالة. لكن الجزء الصعب هو أنه لغرض توفير المساحة وزيادة السرعة، يتم تعبئة هذه الصبوات بإحكام شديد بحيث لا تكون حتى محاذية لصفوف مرتبة من البايتات (مثل الكلمات الحاسوبية القياسية)؛ بل يتم تعبئتها وصولاً إلى آخر بت (bit)، وهو أصغر جزء من البيانات. طريقة التعبئة المحددة والضيقة للغاية هذه تسمى UPER.
المشكلة هي أن كتابة مترجم (أو "محلل" - parser) لتفريغ هذه الصناديق الصغيرة على مستوى "البت" أمر صعب للغاية. إذا ارتكب المترجم خطأً بسيطاً واحدًا — مثل قراءة بت واحد بشكل خاطئ أو نسيان قاعدة حول كيفية التعامل مع معلومات جديدة وغير معروفة — فقد يتسبب ذلك في تعطل النظام بأكامل، أو تسريب أسرار، أو السماح للمخترقين بالتسلل. لسنوات، حاول المهندسون إصلاح هذه الأخطاء عن طريق اختبار المترجمات برسائل عشوائية بالملايين، آملين في رصد الأخطاء، لكن هذا يشبه محاولة العثور على إبرة في كومة قش عن طريق هز القش فقط؛ قد تجد بعض الإبر، لكن لا يمكنك التأكد أبداً مما إذا كنت قد وجدت جميعها أو ما إذا كانت هي الإبر الحقيقية المنشودة.
هنا يأتي دور VUPER، وهي أداة جديدة ابتكرها باحثون من جامعة بن ستيت (Penn State) تغير قواعد اللعبة. فبدلاً من مجرد هز كومة القش، يقوم VUPER ببناء مترجم مثالي رياضياً من الصفر. فكر في الأمر كإنشاء قاموس وكتاب قواعد "معيار ذهبي" مثبت بواسطة عالم رياضيات حاسوبي بأنه صحيح بنسبة 100%. استخدم الباحثون هذا المترجم المثالي لاختبار 11 مترجماً آخر شائع الاستخدام في شبكات الجيل الخامس (5G) وأنظمة الاتصال بين المركبات (V2X). واكتشفوا أن العديد من هذه المترجمات المستخدمة على نطاق واسع كانت في الواقع غير متوافقة، حيث تفتقر إلى 20 نوعاً مختلفاً من القواعد. وفي بعض الحالات، سمح عدم التوافق هذا للمخترقين بتعطيل الهواتف أو خداء الشبكات لإرسال رسائل غير مشفرة. يثبت VUPER أنه بينما لا يمكننا دائماً الوثوق بالمترجمات التي لدينا، يمكننا الآن بناء مترجمات مضمونة رياضياً بأنها آمنة، واستخدامها لإصلاح المترجمات المعيبة.
قصة VUPER: بناء المترجم المثالي
في عالم شبكات الكمبيوتر، تشبه البيانات تدفقاً طويلاً من المياه عبر الأنابيب. لإرسال رسالة، يقوم الكمبيوتر بعملية "تسلسل" (serialization)، أي عصر البيانات في تدفق مضغوط من البتات. ولاستقبالها، يقوم كمبيوتر آخر بعملية "تحليل" (parsing)، أي عصر البتات وإعادتها إلى رسالة قابلة للقراءة. في عالم الجيل الخامس (5G) عالي المخاطر واتصالات المركبات (V2X)، تستخدم هذه العملية مجموعة محددة من القواعد تسمى UPER (قواعد الترميز المعبأ غير المحاذي). وتسمى "غير محاذية" لأنها لا تهتم بحدود البايتات المرتبة؛ بل تقوم بتعبئة البيانات بأقصى قدر من الإحكام، بتّاً تلو الآخر، لتوفير عرض النطاق الترددي.
التحدي يكمكم في أن كتاب القواعد الرسمي لـ UPER مكتوب بنصوص وصفية كثيفة، وليس برمجية. وهذا يترك المهندسين للتخمين حول كيفية تنفيذ القواعد، مما يؤدي إلى أخطاء دقيقة. قرر الباحثون وراء VUPER التوقف عن التخمين؛ حيث بنوا إطار عمل يثبت رسمياً صحة المحلل. لم يكتفوا بكتابة الكود والأمل في نجاحه، بل استخدموا أداة رياضية قوية تسمى Rocq prover للتحقق من كل خطوة من خطوات المنطق.
اختبار "الرحلة الذهاب والإياب" (Round-Trip)
لفهم كيفية عمل VUPER، تخيل أن لديك مترجماً سحرياً يحول كتاباً إلى شفرة سرية والعكس. اختبار "الرحلة الذهاب والإياب" يعني أن تأخذ جملة، تحولها إلى شفرة، ثم تحول تلك الشفرة مرة أخرى إلى جملة. إذا حصلت على نفس الجملة تماماً، فإن المترجم يعمل بشكل صحيح.
ومع ذلك، فإن لـ UPER التواءً خاصاً وهو: الامتدادات (extensions). مع تطور التكنولوجيا (مثل الانتقال من 4G إلى 5G)، تُضاف ميزات جديدة إلى الرسائل. ويجب أن يكون المترجم القديم قادراً على قراءة رسالة جديدة، وتجاهل الأجزاء الجديدة التي لا يفهمها، ومع ذلك يظل مدركاً للأجزاء القديمة. يسمى هذا التوافق الأمامي (forward compatibility). يتعامل VUPER مع هذا من خلال إثبات شيئين:
- الرحلة الذهاب والإياب الصارمة: إذا كانت الرسالة من نفس الإصدار، يجب على المترجم تحويلها مرة أخرى إلى نفس نمط البتات بالضبط. لا بتات زائدة، ولا بتات مفقودة.
- الرحلة الذهاب والإياب الضعيفة: إذا كانت الرسالة تحتوي على امتدادات جديدة وغير معروفة، يمكن للمترجم تخطيها، ولكن يجب أن يظل قادراً على تحويل الأجزاء المعروفة إلى رسالة صالحة. ليس من الضروري أن يتطابق بتّاً ببت مع الأصل (لأن الأجزاء غير المعروفة قد حُذفت)، ولكنه يجب ألا يفسد بقية الرسالة.
اكتشاف الأخطاء
بنى الباحثون "أوراكل موثوقاً" (trusted oracle) — وهو محلل مثالي تم إنشاؤه بواسطة VUPER — واستخدموه لاختبار 11 محللاً آخر. تضمنت هذه المترجمات 7 أدوات مفتوحة المصدر (مثل asn1c و pycrate) و4 محللات تجارية مستخدمة داخل محطات القاعدة الفعلية لشبكات 4G و5G (الأجهزة التي تربط هاتفك بالشبكة).
لم يرسلوا مجرد بيانات عشوائية؛ بل استخدموا "fuzzer" ذكياً يفهم هيكل الرسائل لإنشاء ملايين حالات الاختبار المعقدة. وعند مقارنة النتائج، وجدوا 20 نوعاً مختلفاً من التناقضات في المترجمات الأخرى.
إليك بعض النتائج الأكثر إثارة للاهتمام:
- مشكلة "الطول الزائد": قبلت بعض المترجمات أرقاماً أكبر مما هو مخصص لها، أو أطوالاً لا تتطابق مع البيانات. هذا يشبه ساعي البريد الذي يقبل رسالة تقول "لدي 5 صفحات" ولكنها تحتوي في الواقع على 100 صفحة، مما يؤدي إلى فيضان صندوق البريد وتعطله.
- ارتباك "الامتداد غير المعروف": عندما تحتوي الرسالة على ميزات جديدة لا يعرفها المحلل القديم، ارتبكت بعض المحللات وبدأت في قراءة الجزء الخطأ من الرسالة، معتقدة أنه شيء آخر تماماً. هذا يشبه مترجماً يرى كلمة جديدة في لغة أجنبية، فيصاب بالارتباك ثم يترجم بقية الجملة بشكل خاطئ.
- خطأ "القيمة الافتراضية": تنص القواعد على أنه إذا كانت القيمة هي "الافتراضية"، فلا ينبغي إرسالها على الإطلاق لتوفير المساحة. لكن بعض المحللات كانت لا تزال ترسلها، أو تفشل في التعرف على غيابها.
الخطر في العالم الحقيقي
لم يكتفِ البحث بإيجاد أخطاء نظرية؛ بل أظهر كيف يمكن استغلالها. أظهر الباحثون أربعة هجمات ملموسة:
- تعطيل الهاتف: عبر إرسال رسالة تحتوي على قائمة بمعرفات الشبكة طويلة قليلاً (مما ينتهك قيداً معيناً)، تسببوا في تعطل برنامج الهاتف، مما أدى إلى هجوم حجب الخدمة (DoS).
- تعطيل البرج: يمكن لبرج خلوي مخترق أن يرسل رسالة مشوهة إلى برج آخر، مما يتسبب في تعطل البرج الثاني أثناء محاولته معالجة الرسالة.
- تسريب الأسرار: إذا أخطأ المحلل في تفسير رسالة بسبب امتداد غير معروف، فقد يعتقد أن إعداداً أمنياً "مغلق" بينما هو في الواقع "مفتوح"، أو العكس. قد يؤدي هذا إلى وضع يعتقد فيه الهاتف أنه يتواصل بشكل آمن، بينما ترسل الشبكة في الواقع بيانات بنص واضح، مما يسمح للمتنصتين بقراءتها.
- بصمة الجهاز (Device Fingerprinting): نظرًا لأن المترجمات المختلفة تتعامل مع الأخطاء بطرق مختلفة، يمكن للمخترق إرسال رسائل "خدعة" محددة ومراقبة رد فعل الجهاز. إذا قبل الجهاز رسالة غريبة، سيعرف المخترق أنه يستخدم عتاداً من علامة تجارية معينة (مثل نظام Samsung الأساسي)، مما يسمح له باستهداف ذلك الجهاز تحديداً بثغرات معروفة.
الأداء والمستقبل
يعترف الباحثون بأن محللهم المثالي والمثبت رياضياً ليس الأسرع في الخارج. فهو أبطأ بحوالي 4 مرات من مكتبات لغة C عالية التحسين المستخدمة حالياً في الصناعة. ومع ذلك، فهو أسرع بـ 4 مرات من المحللات القائمة على لغة بايثون.
الهدف من VUPER ليس استبدال المحللات السريعة فوراً، بل أن يعمل كـ نموذج مرجعي (reference implementation). تماماً كما يمكن للطاهي الماهر تذوق الطبق وإخبارك بالضبط بما هو خطأ في الوصفة، يمكن لـ VUPER أن يخبر المهندسين بالضبط أين تخفق محللاتهم. يأمل الباحثون أنه من خلال استخدام VUPER للعثور على هذه الأخطاء وإصلاحها، يمكن للصناعة في النهاية بناء محللات تكون سريعة ومضمونة رياضياً بأنها آمنة في آن واحد.
في النهاية، يثبت VUPER أنه في عالم الجيل الخامس وما بعده المعقد وعالي السرعة، لم يعد بإمكاننا الاعتماد على اختبار "جيد بما يكفي". نحن بحاجة إلى مترجمين مثبتين رياضياً للحفاظ على سلامة مدينتنا الرقمية، وأمنها، وسير عملها بسلاسة.
غارق في أبحاث مجالك؟
تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.