عندما تشتري شيئًا ما على Amazon ، يتم تحديث بيانات العميل تلقائيًا وتخزينها على آلاف الأجهزة الافتراضية في السحابة. بالنسبة للشركات مثل Amazon ، يعد ضمان سلامة وأمن بيانات ملايين العملاء أمرًا ضروريًا. هذا صحيح بالنسبة للمؤسسات الكبيرة والصغيرة على حد سواء. ولكن حتى الآن ، لا توجد طريقة لضمان أمان نظام البرنامج من الأخطاء والمتسللين ونقاط الضعف.
ربما يكون باحثو هندسة كولومبيا قد حلوا هذه المشكلة الأمنية. لقد طوروا نظام SeKVM ، وهو أول نظام يضمن - من خلال إثبات رياضي - أمان الأجهزة الافتراضية في السحابة. في ورقة جديدة سيتم تقديمها في 26 مايو 2021 ، في ندوة IEEE الثانية والأربعين حول الأمن والخصوصية ، يأمل الباحثون في وضع الأساس للابتكارات المستقبلية في التحقق من برمجيات النظام ، مما يؤدي إلى جيل جديد من برامج النظام المرنة عبر الإنترنت.
SeKVM هو أول نظام معتمد رسميًا للحوسبة السحابية. يعد التحقق الرسمي خطوة حاسمة حيث إنها عملية إثبات أن البرنامج صحيح رياضيًا ، وأن كود البرنامج يعمل كما ينبغي ، ولا توجد أخطاء أمنية مخفية تدعو للقلق.
قال جيسون نيه ، أستاذ علوم الكمبيوتر والمدير المشارك لمختبر أنظمة البرمجيات: "هذه هي المرة الأولى التي يظهر فيها نظام برمجي متعدد المعالجات في العالم الحقيقي صحيحًا وآمنًا من الناحية الحسابية". "هذا يعني أن بيانات المستخدمين تتم إدارتها بشكل صحيح عن طريق البرامج التي تعمل في السحابة وأنها في مأمن من الأخطاء الأمنية والمتسللين."
كان إنشاء برامج نظام صحيحة وآمنة أحد أكبر التحديات التي تواجه الحوسبة. | عمل نيه في جوانب مختلفة من أنظمة البرمجيات منذ انضمامه إلى Columbia Engineering في 1999. عندما انضم Ronghui Gu ، الأستاذ المساعد Tang Family في علوم الكمبيوتر وخبير التحقق الرسمي ، إلى قسم علوم الكمبيوتر في 2018 ، قرر هو و Nieh التعاون في استكشاف التحقق الرسمي من أنظمة البرمجيات.
حظي بحثهما باهتمام كبير: فاز كلا الباحثان بجائزة أمازون للأبحاث ، ومنح متعددة من مؤسسة العلوم الوطنية ، بالإضافة إلى عقد وكالة مشاريع البحوث الدفاعية المتقدمة (DARPA) بملايين الدولارات لتعزيز تطوير مشروع SeKVM. بالإضافة إلى ذلك ، مُنح نيه زمالة غوغنهايم لهذا العمل.
على مدى السنوات العشر الماضية ، كان هناك قدر كبير من الاهتمام بالتحقق الرسمي ، بما في ذلك العمل على التحقق من أنظمة التشغيل متعددة المعالجات. قال جو: "لكن كل تلك الأبحاث أُجريت على أنظمة صغيرة شبيهة بالألعاب لا يستخدمها أحد في الحياة الواقعية". "يُعتقد أن التحقق من نظام سلعة متعدد المعالجات ، وهو نظام واسع الاستخدام مثل Linux ، مستحيل إلى حد ما".
مكّن النمو الهائل للحوسبة السحابية الشركات والمستخدمين من نقل بياناتهم وحساباتهم خارج الموقع إلى أجهزة افتراضية تعمل على مضيفين في السحابة. ينشر موفرو الحوسبة السحابية ، مثل Amazon ، برامج Hypervisor لدعم هذه الأجهزة الافتراضية
برنامج Hypervisor هو الجزء الأساسي من البرنامج الذي يجعل الحوسبة السحابية ممكنة. يتوقف أمان بيانات الجهاز الظاهري على صحة وموثوقية برنامج Hypervisor. على الرغم من أهميتها ، فإن برامج Hypervisor معقدة - يمكنها تضمين نظام تشغيل Linux كامل. مجرد رابط ضعيف واحد في الشفرة - وهو ارتباط يكاد يكون من المستحيل اكتشافه عبر الاختبارات التقليدية - يمكن أن يجعل النظام عرضة للقراصنة. حتى إذا تمت كتابة برنامج Hypervisor بشكل صحيح بنسبة 99 ٪ ، فلا يزال بإمكان المتسلل التسلل إلى هذا الإعداد المحدد بنسبة 1 ٪ والتحكم في النظام.
يعتبر عمل Nieh و Gu أول من يتحقق من نظام سلعي ، وتحديداً جهاز Hypervisor KVM المستخدم على نطاق واسع ، والذي يتم استخدامه لتشغيل الأجهزة الافتراضية من قبل مزودي الخدمات السحابية مثل Amazon. لقد أثبتوا أن SeKVM ، وهو KVM مع بعض التغييرات الصغيرة ، آمن ويضمن عزل أجهزة الكمبيوتر الافتراضية عن بعضها البعض.
قال Xupeng Li ، دكتوراه في Gu: "لقد أظهرنا أن نظامنا يمكنه حماية وتأمين البيانات الخاصة والحوسبة التي يتم تحميلها على السحابة بضمانات رياضية". الطالب والمؤلف الرئيسي المشارك للورقة. "لم يتم القيام بذلك من قبل."
تم التحقق من SeKVM باستخدام MicroV ، وهو إطار عمل جديد للتحقق من خصائص الأمان للأنظمة الكبيرة. ويستند إلى الفرضية القائلة بأن التغييرات الصغيرة في النظام يمكن أن تسهل التحقق بشكل كبير ، وهي تقنية جديدة يسميها الباحثون التحقق من MICR. تعمل تقنية الطبقات الجديدة هذه على تعديل نظام موجود واستخراج المكونات التي تفرض الأمن في نواة صغيرة يتم التحقق منها وتضمن أمان النظام بأكمله.
التغييرات اللازمة لتعديل نظام كبير هي تغييرات متواضعة للغاية - أظهر الباحثون أنه إذا كانت النواة الصغيرة للنظام الأكبر سليمة ، فسيكون النظام آمنًا ولن يتم تسريب أي بيانات خاصة. هذه هي الطريقة التي تمكنوا بها من التحقق من نظام كبير مثل نظام KVM ، والذي كان يُعتقد سابقًا أنه مستحيل.
وأوضح نيه: "فكر في منزل - لا يعني وجود صدع في الحوائط الجافة أن سلامة المنزل في خطر". "لا تزال سليمة من الناحية الهيكلية والنظام الهيكلي الرئيسي جيد."
شيه وي لي ، دكتوراه نيه. وأضاف الطالب والمؤلف الرئيسي المشارك للدراسة ، "سيكون SeKVM بمثابة حماية في مختلف المجالات ، من الأنظمة المصرفية وأجهزة إنترنت الأشياء إلى المركبات المستقلة والعملات المشفرة."
كأول برنامج Hypervisor للسلع تم التحقق منه ، يمكن لـ SeKVM تغيير كيفية تصميم الخدمات السحابية وتطويرها ونشرها والوثوق بها. في عالم حيث الأمن السيبراني مصدر قلق متزايد ، هذه المرونة مطلوبة بشدة. تستكشف شركات السحابة الكبرى بالفعل كيف يمكنها الاستفادة من SeKVM لتلبية هذا الطلب.