دورة معهد ماساتشوستس للتكنولوجيا "أمن أنظمة الكمبيوتر". المحاضرة 10: التنفيذ الرمزي ، الجزء الأول

معهد ماساتشوستس للتكنولوجيا. محاضرة رقم 6.858. "أمن أنظمة الكمبيوتر." نيكولاي زيلدوفيتش ، جيمس ميكنز. 2014 سنة

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

المحاضرة 1: "مقدمة: نماذج التهديد" الجزء 1 / الجزء 2 / الجزء 3
المحاضرة 2: "السيطرة على هجمات القراصنة" الجزء 1 / الجزء 2 / الجزء 3
المحاضرة 3: "تجاوزات العازلة: المآثر والحماية" الجزء 1 / الجزء 2 / الجزء 3
المحاضرة 4: "فصل الامتيازات" الجزء 1 / الجزء 2 / الجزء 3
المحاضرة 5: "من أين تأتي أنظمة الأمن؟" الجزء 1 / الجزء 2
المحاضرة 6: "الفرص" الجزء 1 / الجزء 2 / الجزء 3
المحاضرة 7: "وضع حماية العميل الأصلي" الجزء 1 / الجزء 2 / الجزء 3
المحاضرة 8: "نموذج أمن الشبكات" الجزء 1 / الجزء 2 / الجزء 3
المحاضرة 9: "أمان تطبيق الويب" الجزء 1 / الجزء 2 / الجزء 3
المحاضرة 10: "التنفيذ الرمزي" الجزء 1 / الجزء 2 / الجزء 3

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



التنفيذ الرمزي هو العمود الفقري لتحليل البرنامج الحديث. هذه إحدى الطرق التي نشأت من البحث ثم بدأ استخدامها في العديد من التطبيقات. على سبيل المثال ، يوجد حاليًا في Microsoft نظام يسمى SAGE ، والذي يعمل مع الكثير من برامج Microsoft المهمة ، بدءًا من Power Point وتنتهي مع Windows نفسه ، للعثور على مشكلات الأمان ونقاط الضعف حقًا.

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

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

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



هنا لدينا جزء من كود بسيط للغاية من عدة فروع وبيان أنه إذا كانت قيمة t <x تحت شرط ما ، فهذا بيان خاطئ. نريد معرفة ما إذا كان من الممكن رفع هذا البيان. هل هذا ممكن؟ هل هناك أي مدخلات ستفشل هذا البيان؟

أحد الأشياء التي يمكنني القيام بها هو التحقق من تنفيذ هذا البرنامج باستخدام قيم محددة لبيانات الإدخال كمثال. لنفترض أننا نستخدم مدخلات يكون فيها X = 4 و Y = 4. قيمة T هي صفر ، كما تم الإعلان عنه في بداية البرنامج.

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

وبالتالي ، يمكن أن تتميز الدولة بشكل كامل بهذه المتغيرات الثلاثة ، إلى جانب معرفة مكاني في البرنامج. لذلك ، إذا بدأت التنفيذ من 4 و 4 و 0 ووصلت إلى نهاية الفرع ، فسوف أتحقق من التعبير: 4 أكبر من 4؟ من الواضح أنه لا.
الآن سأقوم بتنفيذ البرنامج على T = Y ، أي أن T لم يعد 0 ، ولكن له قيمة 4. هذه هي الحالة الحالية لبرنامجي ، ويمكنني الآن تقييم هذا الفرع.



هل صحيح أن T <X؟ لا. تهربنا من الرصاصة ، البيان الكاذب لم ينجح. لم تكن هناك مشاكل في هذا التنفيذ الخاص.

لكن هذا لا يخبرنا شيئًا عن أي إعدام آخر. نحن نعلم أنه مع القيم X = 4 و Y = 4 ، لن يفشل البرنامج. لكن هذا لا يخبرنا بأي شيء عما سيحدث إذا كانت قيم الإدخال 2 و 1.



باستخدام قيم الإدخال هذه ، سيتم تنفيذ التنفيذ بطريقة مختلفة. هذه المرة نرى أن T = X ، وبعد تنفيذ هذا السطر T سيأخذ قيمة تساوي 2. هل هناك أي مشاكل في هذا التنفيذ؟ هل سيكون هناك خطأ في التأكيد مع مثل هذا الإدخال؟

حسنا ، دعنا نرى. لذا ، إذا كانت T تساوي 2 و X تساوي 2 ، فإن T لا تقل عن X. يبدو أننا تجنبنا الرصاصة مرة أخرى. صحيح؟ لذا ، لدينا هنا قيمتا إدخال محددتان يعمل فيه البرنامج دون أخطاء. ولكن في الواقع ، لا يخبرنا أي شيء عن أي قيم إدخال أخرى.

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



بالنسبة لبرنامج مثل هذا ، يتم تحديد حالته من خلال قيمة هذه المتغيرات الثلاثة المختلفة: X و Y و T ، ومعرفة مكاني الحالي في البرنامج. ولكن الآن بدلاً من القيم المحددة لـ X و Y ، سيكون لي قيمة رمزية ، مجرد متغير. متغير يسمح لي بتسمية هذه القيمة ، والتي يستخدمها المستخدم كمدخل. هذا يعني أن حالة برنامجي لم تعد تتميز بمطابقة أسماء المتغيرات مع قيم معينة. الآن هذه خريطة لأسماء المتغيرات لهذه القيم الرمزية.

يمكن اعتبار القيمة الرمزية كصيغة. في هذه الحالة ، صيغة X تساوي X وصيغة Y هي Y ببساطة ، و T تساوي 0 في الواقع. نحن نعلم أنه لكل قيمة إدخال لا يهم ما تفعله. ستكون قيمة T بعد العبارة الأولى 0.

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

هل نعرف أي شيء عن X و Y؟ ماذا نعرف عنها؟ على الأقل نحن نعرف نوعهم ، نعلم أنهم سيختلفون من min int إلى max int ، ولكن هذا كل ما نعرفه عنهم. اتضح أن المعلومات التي نعرفها عنها ليست كافية لتحديد الاتجاه الذي يمكن أن يسلكه هذا الفرع. يمكنها الذهاب في أي اتجاه
هناك العديد من الأشياء التي يمكننا القيام بها ، ولكن ماذا يمكننا أن نفعل في الوقت الحالي؟ حاول أن تخمن أعنف.



الجمهور: يمكننا متابعة تنفيذ البرنامج على كلا الفرعين.

الأستاذ: نعم ، يمكننا تتبع التقدم في كلا الفرعين. اقلب عملة معدنية ، واعتمادًا على كيفية سقوطها ، اختر فرعًا أو فرعًا آخر.

لذا ، إذا أردنا أن نتبع كلا الفرعين ، يجب علينا أولاً اتباع أحدهما ثم الآخر ، أليس كذلك؟ لنفترض أننا بدأنا بهذا الفرع - T = X. نحن نعلم أنه إذا وصلنا إلى هذا المكان ، فإن T سيكون له نفس معنى X. لا نعرف ما هي هذه القيمة ، ولكن لدينا اسم لها - هذا هو البرنامج النصي X.



إذا أخذنا الفرع المقابل ، فماذا سيحدث؟ ستكون قيمة T مساوية لشيء آخر ، أليس كذلك؟ في هذا الفرع ، ستكون قيمة T هي القيمة الرمزية لـ Y.



إذن ماذا تعني قيمة T عندما نصل إلى هذه النقطة في البرنامج؟ ربما يكون X ، وربما يكون Y. لا نعرف بالضبط ما هذه القيمة ، ولكن لماذا لا نعطيها اسمًا؟ يطلق عليه ر ₀ . وماذا نعرف عن t ₀ ؟ في أي الحالات ستكون t ₀ مساوية لـ X؟

بشكل أساسي ، نعلم أنه إذا كانت X أكبر من Y ، فإن المتغير يساوي X ، وإذا كانت X أقل من أو تساوي Y ، فإن المتغير يساوي Y. لذلك ، لدينا قيمة حددناها ، فلنطلق عليها t ₀ ، ولها هذه الخصائص المنطقية.



لذا ، في هذه المرحلة من البرنامج ، لدينا اسم لقيمة T ، وهذا هو t ₀ . ماذا فعلنا هنا؟ أخذنا كلا فرعي عبارة if ، ثم قمنا بحساب القيمة الرمزية ، ونرى تحت أي ظروف سيتم تنفيذ أحد فروع البرنامج ، وتحت أي فرع.
الآن نصل إلى النقطة التي يجب أن نسألها عما إذا كان T يمكن أن يكون أقل من X. الآن قيمة T هي t ₀ ، ونريد أن نعرف ما إذا كان من الممكن أن يكون t ₀ أقل من X؟ تذكر الفرع الأول الذي قمنا بفحصه - لقد طرحنا سؤالًا حول X و Y ولم نعرف شيئًا عنهما ، إلا أنهما من النوع int.

ولكن بوجود t ₀ ، فنحن نعرف الكثير عنه. نحن نعلم أنه في بعض الحالات سيكون مساوياً لـ X ، وفي بعض الحالات سيكون مساوياً لـ Y. لذا فإنه يعطينا الآن مجموعة من المعادلات التي يمكننا حلها. لذا ، يمكننا أن نقول ما إذا كان من الممكن أن يكون t ₀ أقل من X ، مع العلم أن t ₀ يستوفي جميع هذه الشروط؟ وبالتالي ، يمكننا التعبير عن هذا على أنه تقييد ، مما يوضح ما إذا كان من الممكن _أن يكون t ₀ أقل من X. وإذا كانت X أكبر من Y ، فإن t ₀ تساوي X ، وإذا كانت X أقل من أو تساوي Y ، فهذا يعني أن t ₀ = ذ.



لذا لدينا معادلة. إذا كان لديه حل ، إذا كان من الممكن العثور على قيمة t ₀ وقيمة X وقيمة Y التي تلبي هذه المعادلة ، فإننا ندرك هذه القيم ، وعندما ندخلها في البرنامج ، فعند تنفيذها ، ستذهب على طول هذا الفرع إذا t <x و " سينفجر "عندما يقع في تأكيد كاذب.

إذن ماذا فعلنا هنا؟ قمنا بتنفيذ البرنامج ، ولكن بدلاً من تعيين أسماء المتغيرات لقيم معينة ، قدمنا ​​قيمًا رمزية لأسماء المتغيرات. في الواقع ، أعطوهم أسماء متغيرة أخرى. وفي هذه الحالة ، فإن أسماء المتغيرات الأخرى هي script X ، script Y ، t ₀ ، بالإضافة إلى ذلك ، لدينا مجموعة من المعادلات التي توضح كيفية ارتباط هذه القيم. لدينا معادلة تخبرنا عن كيفية ارتباط t ₀ بـ X و Y في هذه الحالة.

يتيح لنا حل هذه المعادلة الإجابة على السؤال عما إذا كان يمكن تنفيذ هذا الفرع أم لا. نلقي نظرة على المعادلة - هل من الممكن أن تأخذ هذا الفرع أم لا؟ يبدو أنه ليس كذلك ، لأننا نبحث عن الحالات التي تكون فيها t ₀ أقل من X ، ولكن إذا كانت الحالة الأولى t ₀ = X ، فلن يكون التعبير t ₀ <X صحيحًا.

وبالتالي ، هذا يعني أنه عندما تكون X> Y ، لا يمكن أن يحدث ذلك ، لأن t ₀ = X ولا يمكن أن تكون مساوية لـ X أو أقل منه في نفس الوقت.

ولكن ماذا يحدث إذا كانت t ₀ = Y؟ هل يمكن أن يكون t ₀ أقل من X في هذه الحالة؟

لا ، بالتأكيد لا يمكن ذلك ، لأننا نعلم أن X <Y. لذلك إذا كانت t ₀ أقل من X ، فستكون أيضًا أقل من Y. لكننا نعلم أنه في هذه الحالة t ₀ = Y. وبالتالي ، مرة أخرى ، لا يمكن استيفاء هذا الشرط. لذا ، لدينا هنا معادلة ليس لها حل ، ولا يهم القيم التي تدرجها في هذه المعادلة.

لا يمكنك حلها ، وهذا يخبرنا أنه بغض النظر عن المدخلات X و Y التي نمررها إلى البرنامج ، فلن ينزل الفرع إذا t <x.

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

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

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



الجمهور: ماذا لو لم يدعم البرنامج إدخال نوع معين من المتغيرات؟

البروفيسور: هذا سؤال جيد جدا! لنفترض أن لدينا نفس البرنامج ، ولكن بدلاً من t = x سيكون لدينا t = (x-1). ثم ، بشكل حدسي ، يمكننا أن نتخيل أن هذا البرنامج يمكن أن "ينفجر" الآن ، أليس كذلك؟



لأنه عندما يسير البرنامج بهذه الطريقة ، سيكون t أقل من x. ماذا سيحدث لمثل هذا البرنامج؟ كيف ستبدو دولتنا الرمزية؟ ماذا سيكون t ₀ عندما تكون x أكبر من y؟ نقوم بتصحيح الخطوط في معادلاتنا وفقًا لقيمة أخرى عندما تكون t = (x-1). الآن قد يفشل البرنامج ، وتذهب إلى المطور وتقول له: "مهلاً ، يمكن أن تنفجر هذه الوظيفة عندما تكون x أكبر من y"!

ينظر المطور إلى هذا ويقول: "أوه ، لقد نسيت أن أخبرك - في الواقع ، لن يتم استدعاء هذه الوظيفة مع المعلمات ، حيث تكون x أكبر من y. "لقد كتبتها للتو لأسباب تاريخية ، لذلك لا تقلق ، لن أتذكرها إذا لم تخبرني".

افترض أن لدينا افتراض أن س سيكون أقل من أو يساوي ص.



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

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

السؤال هو ، هل يمكنني إيجاد x و y يستوفيان كل هذه القيود وفي نفس الوقت يمتلكان الخصائص المطلوبة؟ يمكنك أن ترى أن هذا التقييد X ≤ Y يمثل الفرق بين الحالة عندما يتم تحقيق هذا التقييد والحالة عندما لا يتم الوفاء به.

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

كيف تفعل ذلك بطريقة ميكانيكية؟ هناك جانبان لهذه المشكلة. الجانب الأول - كيف توصلت بالفعل إلى هذه الصيغ؟

في هذه الحالة ، من الواضح بشكل بديهي كيف توصلنا إلى هذه الصيغ ، قمنا ببساطة بتكوينها يدويًا. ولكن كيف يمكن إنشاء هذه الصيغ ميكانيكيًا؟

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



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

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

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

. , SMT, NP- , «» «».
, NP- ? -, ? , SMT – : « ».



, , , , : « ». , , .

27:30

MIT « ». 10: « », 2


النسخة الكاملة من الدورة متاحة هنا .

شكرا لك على البقاء معنا. هل تحب مقالاتنا؟ هل تريد رؤية مواد أكثر إثارة للاهتمام؟ ادعمنا عن طريق تقديم طلب أو التوصية به لأصدقائك ، خصم 30 ٪ لمستخدمي Habr على نظير فريد من خوادم مستوى الدخول التي اخترعناها لك: الحقيقة الكاملة حول VPS (KVM) E5-2650 v4 (6 نوى) 10GB DDR4 240GB SSD 1Gbps من 20 $ أو كيفية تقسيم الخادم؟ (تتوفر الخيارات مع RAID1 و RAID10 ، حتى 24 مركزًا وحتى 40 جيجابايت DDR4).

VPS (KVM) E5-2650 v4 (6 نوى) 10GB DDR4 240GB SSD 1Gbps حتى ديسمبر مجانًا عند الدفع لمدة ستة أشهر ، يمكنك الطلب هنا .

ديل R730xd أرخص مرتين؟ 2 Intel Dodeca-Core Xeon E5-2650v4 128GB DDR4 6x480GB SSD 1Gbps 100 $249 ! اقرأ عن كيفية بناء مبنى البنية التحتية الطبقة باستخدام خوادم Dell R730xd E5-2650 v4 بتكلفة 9000 يورو مقابل سنت واحد؟