← أحدث الأبحاث
💻 computer science

From Specs to Apps: Verifying and Monitoring Models of Signal and WhatsApp

تجسر هذه الورقة البحثية الفجوة بين المواصفات البروتوكولية الرسمية والتنفيذات الواقعية باستخدام أداة المراقبة وقت التشغيل SpecMon للتحقق من أن التنفيذات المرصودة لـ WhatsApp Web وSignal Desktop تتوافق مع نماذج مطورة حديثاً ومتوافقة مع Tamarin، مما يؤكد الخصائص الأمنية ويكشف عن الاختلافات غير الموثقة بين التطبيقين.

المؤلفون الأصليون: Moustafa Said, Aurora Naska, Kevin Morio, Robert Künnemann

نُشر 2026-09-11✓ Author reviewed ⓘ
📖 4 دقيقة قراءة☕ قراءة في استراحة قهوة
CC BY 4.0

المؤلفون الأصليون: Moustafa Said, Aurora Naska, Kevin Morio, Robert Künnemann

البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل

في العصر الرقمي، يعتمد مليارات البشر على تطبيقات المراسلة لمشاركة أكثر أفكارهم خصوصية، وتأمين بياناتهم المالية، وتنسيق حياتهم اليومية. وخلف كواليس هذه التطبيقات يكمن مجموعة معقدة من القواعد تُعرف باسم "البروتوكول"، والذي يعمل بمثابة المخطط لكيفية تشفير الرسائل وإرسالها وفك تشفيرها. وأشهر هذه المخططات هو "بروتوكول سيجنال" (Signal protocol)، وهو نظام صُمم لضمان أنه حتى لو اعترض مخترق رسالة ما، فإنه لن يتمكن من قراءتها. لسنوات طويلة، استخدم خبراء الأمن أدوات حاسوبية قوية لإثبات أن هذا المخطط سليم من الناحية الرياضية؛ حيث أظهروا أنه إذا تم اتباع القواعد بدقة، فإن النظام سيكون غير قابل للاختراق. ومع ذلك، فإن المخطط ليس هو البناء نفسه؛ فمجرد كون التصميم يبدو مثاليًا على الورق لا يعني أن طاقم البناء اتبع كل التعليمات، أو استخدم المواد الصحيحة، أو تجنب الأخطاء العرضية أثناء بناء الجدران. وفي عالم البرمجيات، تكمن الثغرات الأمنية غالبًا في الفجوة بين التصميم النظري والكود الفعلي الذي يعمل على هاتف المستخدم.

لقد سعى فريق من الباحثين في مركز "سيسبا هيلمهولتز للأمن المعلوماتي" (CISPA Helmholtz Center for Information Security) لسد هذه الفجوة. أرادوا معرفة ما إذا كانت النسخ الواقعية من بروتوكول "سيجنال"، كما تعمل داخل تطبيقي "واتساب" و"سيجنال"، تتبع بالفعل القواعد الصارمة التي صُممت للالتزام بها. وبدلاً من محاولة قراءة كامل الكود المصدري لهذه التطبيقات الضخمة — وهي مهمة جعلها عدم الوضوح أو انغلاق بعض أجزائها أمراً صعباً — قام الباحثون ببناء "رقيب" متخصص. هذا الرقيب، الذي يُسمى "سبيك مون" (SpecMon)، يراقب التطبيق أثناء تشغيله، ويستمع إلى كل محادثة يجريها مع الشبكة وكل عملية حسابية يجريها مع مفاتيح الأمان الخاصة به. وهو يقارن هذه الأفعال الحية بالنموذج النظري المثالي في الوقت الفعلي؛ فإذا حاول التطبيق اتخاذ طريق مختصر، أو تخطي خطوة، أو استخدام طريقة مختلفة عما يسمح به المخطط، يطلق الرقيب إنذاراً.

طبق الباحثون هذه الطريقة على تطبيقين رئيسيين: "سيجنال ديسكتوب" (Signal Desktop)، وهو مفتوح للمراجعة من قبل أي شخص، و"واتساب ويب" (WhatsApp Web)، وهو نظام مغلق ومملوك لشركة ضخمة. بالنسبة لتطبيق "سيجنال ديسكتوب"، بدأوا بنموذج رياضي موجود ومفصل للغاية للبروتوكول، وأضافوا إليه التفاصيل المعقدة الموجودة في البرمجيات الفعلية، مثل كيفية تعامله مع أنواع جديدة من التشفير المصممة لمقاومة الحواسيب الكمومية المستقبلية. أما بالنسبة لـ "واتساب"، فقد اضطروا للعمل بشكل عكسي؛ فبدءاً من عدم وجود نموذج مسبق، راقبوا سلوك التطبيق، وسجلوا أفعاله، وبنوا مخططاً جديداً مخصصاً يتطابق تماماً مع ما تفعله البرمجيات. كان هذا إنجازاً كبيراً، حيث كان أول مرة يتم فيها اشتقاق نموذج رسمي مباشرة من تنفيذ نسخة "واتساب" للبروتوكول.

بمجرد تجهيز هذه النماذج، وضع الباحثون الاختبار عليها. أجروا آلاف المحادثات المحاكية، بما في ذلك سيناريوهات تأخرت فيها الرسائل، أو أُرسلت بترتيب خاطئ، أو حيث انقطع الاتصال بالشبكة. وفي كل حالة، تصرفت التطبيقات تماماً كما توقعت النماذج، مما أكد أن آليات الأمان الأساسية تعمل بشكل صحيح. كما قام الباحثون بحقن أخطاء متعمدة في البرمجيات لمعرفة ما إذا كان "الرقيب" الخاص بهم سيكتشفها. لقد جعلوا التطبيقات تعيد استخدام مفاتيح تشفير قديمة، أو تتخطى عمليات التحقق من التوقيع، أو تسرب بيانات سرية بطرق غير متوقعة. وقد رصد النظام كل واحدة من هذه الأخطاء الأمنية، مما أثبت أن أداة المراقبة حساسة بما يكفي لرصد الانحرافات الخطيرة عن القواعد.

ومع ذلك، كشفت المراقبة أيضاً عن اختلافات دقيقة بين التطبيقين لم تكن واضحة للوهلة الأولى. وجد الباحثون أن "واتساب" يتعامل مع "إيصالات القراءة" — وهي الإشعارات التي تخبر المرسل بأن الرسالة قد تمت قراءتها — بشكل مختلف عن "سيجنال". في "سيجنال"، يتم تغليف هذه الإيصالات بنفس التشفير القوي المستخدم في الرسائل وتشارك في التحديث المستمر لمفاتيح الأمان. أما في "واتساب"، فتُرسل هذه الإيصالات خارج طبة التشفير تلك، مما يعني أنها لا تحفز تحديثات أمنية مماثلة. وبينما لم يجد الباحثون طريقة لكسر أمان "واتساب" بناءً على هذا الاختلاف، إلا أنهم أشاروا إلى أن هذا يعني أن التطبيق قد يستغرق وقتاً أطول لاستعادة أمانه إذا ما سُرق مفتاح سري ما. كما أكدوا أن "واتساب" لا يتضمن بعد ميزات الخصوصية المتقدمة، مثل إخفاء هوية المرسل عن الخادم، والتي تتوفر في تطبيق "سيجنال".

تُظهر هذه الدراسة أنه من الممكن مراقبة البرمجيات المعقدة في العالم الحقيقي والتحقق من التزامها بوعودها الأمنية دون الحاجة لرؤية كل سطر من كودها المصدري. كانت العملية فعالة، حيث استغرقت بضعة أسابيع فقط للإعداد والتشغيل، ولم تضف سوى قدر ضئيل جداً من التأخير إلى سرعة التطبيقات. ومن خلال إنشاء نظام يتشارك فيه النموذج النظري والمراقبة الحية نفس اللغة، قدم الباحثون طريقة للمطورين وخبراء الأمن للتحقق باستمرار من بقاء تطبيقاتهم آمنة مع تطورها. يوفر هذا النهج مساراً جديداً لبناء الثقة في الأدوات الرقمية التي نستخدمها كل يوم، مما يضمن أن المباني التي نسكن فيها آمنة بقدر المخططات التي بُنيت منها.

غارق في أبحاث مجالك؟

تصلك نشرة يومية بأحدث الأبحاث المطابقة لكلماتك البحثية المفتاحية — مع ملخصات تقنية، بلغتك.

جرّب Digest →

أبحاث مشابهة

عرض الكل في هذا التصنيف 💻 cs →