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

في ربيع عام 2015 ، حاول فريق من المتسللين اقتحام طائرة هليكوبتر عسكرية بدون طيار تسمى ليتل بيرد ("بيرد"). وتقع المروحية ، على غرار النسخة المأهولة من الطائرات المفضلة للقوات الخاصة الأمريكية ، في بوينج في أريزونا. كان للمخترقين بداية مسبقة: في بداية عملهم ، تمكنوا من الوصول إلى أحد الأنظمة الفرعية للكمبيوتر التحكم. يمكنهم فقط اختراق الكمبيوتر الرئيسي على متن الطائرة والسيطرة على الطائرات بدون طيار.

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

تقول كاثلين فيشر : "لم يتمكنوا من كسر أو تعطيل العملية"، أستاذ علوم الكمبيوتر في جامعة تافتس ومدير مشروع الأنظمة العسكرية السيبرانية عالية التأمين (HACMS). "ونتيجة لذلك ، نهض ممثلو DARPA وقالوا ، يا إلهي ، يمكنك في الواقع استخدام هذه التكنولوجيا في الأنظمة المهمة".

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

يقول بريان بارنو ، الباحث في الأبحاث والأمن الرسمي في Microsoft Research: "تكتب صيغة رياضية تصف سلوك البرنامج ، وتستخدم أداة إثبات المفهوم التي تختبر صلاحية هذا البيان" .

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

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

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

كاثلين فيشر

أحلام البرامج المثالية

في أكتوبر 1973 ، توصل Edsger Dijkstra بفكرة إنشاء رمز بدون أخطاء. في الليل ، أثناء وجوده في أحد الفنادق في أحد المؤتمرات ، فكر فجأة في كيفية جعل البرمجة أكثر رياضية. قال في شرح الفكرة لاحقًا: "بعقل متحمس ، خرجت من السرير في الساعة 2:30 صباحًا ، وكتبت لأكثر من ساعة". كانت هذه المادة بداية كتابه المثمر لعام 1976 ، "تأديب البرمجة" ، الذي حدد ، إلى جانب عمل تشارلز هواري (مثل Dijkstra ، الذي حصل على جائزة تورينج ) ، وجهات نظر حول استخدام إثبات الصحة في كتابة البرامج.

لكن علم الكمبيوتر لم يتبع هذه الفكرة ، ويرجع ذلك أساسًا إلى أنه لسنوات عديدة بدا من غير العملي ، أو حتى المستحيل ، تحديد وظيفة البرنامج باستخدام قواعد المنطق الرسمي.

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

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

"حفرة واحدة في مكان ما في البرنامج ، وهذه ثغرة أمنية. يقول بارنو: "من الصعب جدًا التحقق من جميع المسارات بحثًا عن جميع المدخلات الممكنة".

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

في اللغة البشرية ، من السهل وصف هذا. إن تحويل المواصفات إلى لغة رسمية يفهمها الكمبيوتر أصعب بكثير - وهو ما يفسر المشكلة الرئيسية في كتابة البرامج.

يقول بارنو: "إن إنشاء مواصفات رسمية مفهومة للكمبيوتر أمر صعب في جوهره". "من السهل على المستوى الأعلى أن تقول" لا تدع تسرب كلمة المرور "، ولكن عليك التفكير في كيفية تحويل هذا إلى تعريف رياضي."

مثال آخر هو برنامج يقوم بفرز قائمة من الأرقام. يمكن للمبرمجة في محاولة إضفاء الطابع الرسمي على مواصفات لها أن تأتي بهذا:

لكل عنصر j في القائمة ، تأكد من j ≤ j + 1

ولكن حتى في هذه المواصفات الرسمية - للتأكد من أن كل عنصر في القائمة أقل أو يساوي العنصر التالي - هناك خطأ. يفترض المبرمج أن الناتج سيحتوي على المدخلات المعدلة. إذا كانت القائمة [7 ، 3 ، 5] ، فإنه يتوقع أن يعود البرنامج [3 ، 5 ، 7]. لكن مخرجات البرنامج [1 ، 2] ستفي بالمواصفات - لأنها "هي أيضًا قائمة مصنفة ، ولكنها ليست القائمة التي تتوقعها على الأرجح" ، يقول بارنو.

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

منع الأمان

في الواقع ، من الضروري كتابة كل من المواصفات والتعليقات الإضافية اللازمة للبرنامج لاستخلاص استنتاجات حول التعليمات البرمجية. يمكن أن يبلغ حجم البرنامج ، بما في ذلك تأكيده الرسمي ، خمسة أضعاف حجم البرنامج العادي المكتوب لنفس الغرض.

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

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

( ) , … , , .

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

يقول أبيل: "لم نفهم تمامًا". "هناك برامج مفتوحة لجميع قراصنة الإنترنت ، وإذا كان هناك خطأ في مثل هذا البرنامج ، يمكن أن يصبح نقطة ضعف".

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

تقول جانيت وينج ، نائبة رئيس شركة Microsoft Research: "بدءًا من المواصفات في اللغة البشرية ، فقد واجهت بعض الغموض" . - أي لغة طبيعية تحتوي على غموض. في المواصفات الرسمية ، تكتب وصفًا دقيقًا يعتمد على الرياضيات لشرح ما تريده من البرنامج ".

جانيت وينج من Microsoft Research

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

يقول وينج: "نحن لا نقول أننا سنثبت أن النظام بأكمله صحيح بنسبة 100٪ ، وصولاً إلى الدوائر الإلكترونية". - مثل هذه التصريحات سخيفة. نحن دقيقون فيما نستطيع أو لا نستطيع فعله ".

يوضح مشروع HACMS كيف يمكنك تحقيق ضمانات أمنية رائعة من خلال وصف جزء صغير من نظام الكمبيوتر. كان الهدف الأول للمشروع هو إنشاء quadrocopter غير قابل للكسر للترفيه. كان البرنامج الذي جاء مع الرباعي متجانسة - أي من خلال الوصول إلى جزء واحد منه ، تمكن الهاكر من الوصول إلى جميع الأجزاء الأخرى. لمدة عامين ، قام فريق HACMS بتقسيم الرمز في كمبيوتر التحكم إلى أجزاء.

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

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

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

تحقق من الإنترنت

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

مع معدلات أعلى ، وضع الباحثون في الأسلوب الرسمي أهدافًا طموحة بشكل متزايد. يحاول فريق DeepSpec ، بقيادة Appel (يعمل أيضًا على HACMS) ، إنشاء نظام معقد ومختبر بالكامل ، مثل خادم الويب. في حالة نجاح المشروع ، الذي حصل على منحة من مؤسسة العلوم الحكومية بقيمة 10 ملايين دولار ، سيجمع العديد من المشاريع الناجحة الأصغر في العقد الماضي. ابتكر الباحثون العديد من المكونات الآمنة المؤكدة مثل نواة نظام التشغيل. يقول أبيل: "ما لم يتم فعله حتى الآن هو دمج هذه المكونات في واجهات خاصة بالمواصفات".

لدى Microsoft Research ، لدى المبرمجين مشروعين طموحين. الأول ، إيفرست ، يهدف إلى إنشاء نسخة معتمدة من HTTPS ، وهو بروتوكول لتأمين متصفحات الويب التي يطلق عليها وينج "كعب أخيل للإنترنت".

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

يوجد رمز غير منقطع

أحلام البرامج المثالية

منع الأمان

تحقق من الإنترنت

More articles: