سياسة الأصل نفسه

إونسوك كانغ طالب دكتوراه وعضو في مجموعة تصميم البرمجيات في معهد التقنية (MIT). وقد حصل على درجة SM (ماجستير العلوم) في علوم الحاسوب من معهد التقنية سنة 2010، وعلى بكالوريوس هندسة البرمجيات من جامعة واترلو سنة 2007. وقد ركّزت مشاريعه البحثية على تطوير أدوات وتقنيات لنمذجة البرمجيات والتحقّق منها، وتطبيقاتها في الأمن وفي الأنظمة الحرجة من ناحية السلامة.

سانتياغو بيريز دي روسو طالب دكتوراه في مجموعة تصميم البرمجيات في معهد التقنية (MIT). وقد حصل على درجة SM في علوم الحاسوب من معهد التقنية سنة 2015، وعلى بكالوريوس من معهد تيتكنولوغي بوسايتس (ITBA) سنة 2011. وقد عمل في السابق في Google حيث طوّر أطراً وأدوات لزيادة إنتاجية المهندسين سنة 2012. وهو يقضي الآن معظم وقته في التفكير في التصميم وفي التحكّم بالإصدارات (version control).

دانيال جاكسون أستاذ في قسم الهندسة الكهربائية وعلوم الحاسوب في معهد التقنية (MIT)، ويقود مجموعة تصميم البرمجيات في مختبر علوم الحاسوب والذكاء الاصطناعي. وقد حصل على درجة MA من جامعة أكسفورد سنة 1984 في الفيزياء، وعلى درجتي SM سنة 1988 وPhD سنة 1992 في علوم الحاسوب من معهد التقنية. وقد عمل مهندس برمجيات في شركة Logica UK Ltd. بين سنتي 1984 و1986، وأستاذاً مساعداً لعلوم الحاسوب في جامعة كارنيجي ميلون بين سنتي 1992 و1997، وهو في معهد التقنية منذ سنة 1997. وله اهتمامات واسعة بهندسة البرمجيات، ولا سيما بطرائق التطوير، وبالتصميم والمواصفات، وبالطرق الشكلية، وبالأنظمة الحرجة من ناحية السلامة.

مقدمة

سياسة الأصل نفسه (same-origin policy، SOP) جزء مهم من آلية الأمان في كل متصفّح حديث. فهي تتحكّم في متى يمكن للسكربتات العاملة داخل المتصفّح أن تتواصل فيما بينها (وبعبارة أخرى، متى يكون مصدرها الموقع الإلكتروني نفسه). أُدخِلت للمرة الأولى في Netscape Navigator، وهي تلعب اليوم دوراً حاسماً في أمان تطبيقات الويب؛ فبدونها لقَد كان الأمر أسهل بكثير على المخترق الخبيث بأن يتصفّح صورك الخاصة على Facebook، أو يقرأ بريدك الإلكتروني، أو يُفرغ حسابك البنكي.

غير أن سياسة الأصل نفسه بعيدة كل البعد عن الكمال. ففي بعض الأحيان تكون مقيّدة أكثر من اللازم؛ فهناك حالات (مثل التطبيقات المركّبة mashups) ينبغي أن تتمكّن فيها سكربتات من أصول مختلفة منتقاسم مورد، لكنها لا تستطيع. وفي أحيان أخرى لا تكون مقيّدة بما يكفي، فتترك حالات طرفية (corner cases) يمكن استغلالها عبر هجمات شائعة مثل تزوير الطلب عبر المواقع (CSRF). وإضافةً إلى ذلك، فقد تطوّر تصميم سياسة الأصل نفسه عبر السنين بصورة عضوية (organically)، وهو ما يُحيّر كثيراً من المطوّرين.

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

• لماذا سياسة الأصل نفسه ضرورية؟ وما أنواع انتهاكات الأمان التي تمنعها؟
• كيف يؤثّر تطبيقها في سلوك تطبيق الويب؟
• ما الآليات المختلفة لتجاوزها؟
• ما مدى أمان هذه الآليات؟ وما مشكلات الأمان المحتملة التي تُحدثها؟

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

النمذجة باستخدام Alloy

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

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

ولبناء هذا النموذج نستخدم Alloy، وهي لغة لنمذجة تصميم البرمجيات وتحليله. ولا يمكن تنفيذ نموذج Alloy بالمعنى التقليدي لتشغيل البرامج. وبدلاً من ذلك، يمكن (1) أن نحاكي النموذج لإنتاج نموذجاً (_instance) يمثّل سيناريو أو تهيئة صالحة لنظام ما، و(2) أن نفحص (check) النموذج لنرى هل يحقّق خاصية مرغوبة.

ورغم أوجه التشابه هذه، فإن النمذجة الرشيقة تختلف عن البرمجة الرشيقة في جانب أساسي واحد: ورغم أننا سنشغّل اختبارات، فلن نكتب أياً منها في الواقع. فمُحلّل Alloy يولّد حالات الاختبار تلقائياً، وكل ما يلزم تقديمه هو الخاصية المراد فحصها. ومن البديهي أن هذا يوفّر عنا عناءً كبيراً (ونصاً كثيراً). وهو ينفّذ المحلّل فعلياً جميع حالات الاختبار الممكنة حتى حجم معيّن (يسمى نطاقاً (scope))؛ وهذا يعني عادةً توليد جميع الحالات الابتدائية التي تتضمّن عدداً لا يتجاوز حداً ما من العناصر، ثم اختيار العمليات والوسائط لتطبيقها حتى عدد معيّن من الخطوات. ولأن عدداً هائلاً من الاختبارات (يبلغ عادةً المليارات) يُنفَّذ، ولأن جميع التهيئات الممكنة التي يمكن أن تتخذها حالة ما مشمولة (ضمن النطاق على أي حال)، فإن هذا التحليل يكشف الأخطاء على نحو أكثر فاعلية من الاختبارات التقليدية (ويُوصف أحياناً بأنه «تحقّق مقيَّد» (bounded verification)).

التبسيطات

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

على سبيل المثال، نتعامل مع طلبات HTTP كأنها استدعاءات إجراءات عن بُعد (remote procedure calls)، متجاهلين حقيقة أنّ استجابات الطلبات قد تصل خارج الترتيب. كما نفترض أن نظام أسماء النطاقات (DNS) ثابت، لذا لا يمكننا أن نأخذ في الحسبان هجمات يغيّر فيها ربطُ DNS أثناء تفاعل ما. لكن من حيث المبدأ، كان من الممكن تمديد نموذجنا لتغطية جميع هذه الجوانب، وإن كان تحليلُ الأمان بطبيعته لا يسمح لأي نموذج (ولو يمثّل قاعدة الشيفرة بأكملها) بأن يُضمن اكتماله.

خارطة الطريق

إليك الترتيب الذي سنسير عليه في نموذجنا لسياسة الأصل نفسه. سنبدأ ببناء نماذج لثلاثة مكوّنات رئيسية نحتاجها كي نتحدث عن سياسة الأصل نفسه: بروتوكول HTTP، والمتصفّح، والبرمجة من جهة العميل (client-side scripting). وسنبني على هذه النماذج الأساسية لنعرّف ما معنى أن يكون تطبيق الويب آمناً، ثم نقدّم سياسة الأصل نفسه كآلية تحاول تحقيق خصائص الأمان المطلوبة.

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

لا تتردّد في استكشاف الأقسام بأي ترتيب تحبّه. فإذا كنت جديداً على Alloy، فإننا نوصي بالبدء بالأقسام الثلاثة الأولى (HTTP وBrowser وScript)، لأنها تقدّم بعض المفاهيم الأساسية للغة النمذجة. وفي أثناء تقدّمك في الفصل، نوصيك أيضاً بأن تتلاعب بالنماذج في محلّل Alloy؛ شغّلها، واستكشف السيناريوهات المولَّدة، وحاول إجراء تعديلات وشاهد أثرها. وهو متاح للتنزيل مجاناً.

نموذج الويب

HTTP

الخطوة الأولى في بناء نموذج Alloy هي التصريح عن بعض المجموعات (sets) من العناصر. لنبدأ بالموارد (resources):

sig Resource {}

الكلمة المفتاحية sig تحدّد أن هذا تصريح عن توقيع (signature) في Alloy. وهو يُدخل مجموعة من عناصر الموارد؛ تخيّل هذه العناصر، تماماً كعناصر صنف لا يحمل أي متغيّرات نسخة (instance variables)، ككتل لها هوية لكن بلا محتوى. وعندما يُنفَّذ التحليل، تتحدّد هذه المجموعة، تماماً كما يأتي الصنف في لغة كائنية التوجه مجموعة من العناصر عند تشغيل البرنامج.

تُسمّى الموارد بعناوين URL (محدّدات الموارد المنتظمة):

sig Url {
  protocol: Protocol,
  host: Domain,
  port: lone Port,
  path: Path
}
sig Protocol, Port, Path {}
sig Domain { subsumes: set Domain }

لدينا هنا خمسة تصريحات بتوقيعات (signatures)، تُدخل مجموعة من عناوين URL وأربع مجموعات إضافية لكل نوع أساسي من العناصر التي تتألف منها. وداخل تصريح URL لدينا أربعة حقول. والحقول تشبه متغيّرات النسخة في الصنف؛ فإذا كان u عنوان URL مثلاً، فإن u.protocol يمثّل بروتوكول ذلك العنوان (تماماً كنقطة في Java). لكن في الحقيقة، كما سنرى لاحقاً، هذه الحقول علاقات (relations). يمكنك أن تتصوّر كل واحد منها وكأنه جدول قاعدة بيانات من عمودين. وبالتالي protocol جدول عموده الأول يحتوي عناوين URL وعموده الثاني يحتوي البروتوكولات. ومشغّل النقطة، الذي يبدو بريئاً، هو في الحقيقة نوع عام من الدمج العلائقي (relational join)، بحيث يمكنك أيضاً كتابة protocol.p لكل عناوين URL ذات البروتوكول p—وسنعود إلى هذا الأمر أكثر لاحقاً.

لاحظ أن المسارات (paths)، بخلاف عناوين URL، تُعامَل وكأنها بلا بنية—وهو تبسيط. والكلمة المفتاحية lone (يمكن قراءتها «صفر أو واحد») تقول إن لكل عنوان URL منفذاً واحداً على الأكثر. أما المسار فهو السلسلة التي تلي اسم المضيف في عنوان URL، والتي تقابل (بالنسبة لخادم ساكن بسيط) مسار ملف المورد؛ ونحن نفترض أنه حاضر دائماً، لكنه قد يكون مساراً فارغاً.

لنقدّم الآن العملاء والخوادم، وكلٌّ منها يحتوي ربطاً من المسارات إلى الموارد:

abstract sig Endpoint {}
abstract sig Client extends Endpoint {}
abstract sig Server extends Endpoint {
  resources: Path -> lone Resource
}

الكلمة المفتاحية extends تُدخل مجموعة فرعية، فمجموعة Client التي تضمّ كل العملاء هي مثلاً مجموعة فرعية من مجموعة Endpoint التي تضمّ كل نقاط النهاية. والامتدادات متباعدة (disjoint)، فلا نقطة نهاية عميل وخادم في الوقت نفسه. أما الكلمة المفتاحية abstract فتقول إن جميع امتدادات التوقيع تستنفد التوقيع، فوجودها في تصريح Endpoint مثلاً يعني أن كل نقطة نهاية يجب أن تنتمي إلى إحدى المجموعتين الفرعيتين (في هذه المرحلة، Client وServer). وبالنسبة إلى خادم s، فإن التعبير s.resources يدلّ على ربط من المسارات إلى الموارد (ولذلك السهم في التصريح). وتذكّر أن كل حقل هو في الحقيقة علاقة تتضمن التوقيع المالك كعمود أول، لذا فإن هذا الحقل يمثّل علاقة من ثلاثة أعمدة على Server وPath وResource.

ولربط عنوان URL بخادم، نقدّم مجموعة Dns من خوادم أسماء النطاقات، ولكل منها ربط من النطاقات إلى الخوادم:

one sig Dns {
  map: Domain -> Server
}

الكلمة المفتاحية one في تصريح التوقيع تعني أننا (من أجل البساطة) سنفترض وجود خادم أسماء نطاقات واحد بالضبط، وأن هناك ربط DNS واحداً يعبّر عنه التعبير Dns.map. ومرة أخرى، كما في حالة موارد الخدمة، يمكن أن يكون هذا ديناميكياً (وفي الواقع هناك هجمات أمنية معروفة تعتمد على تغيير ربط DNS أثناء تفاعل ما) لكننا نبسّط الأمر.

ولنمذجة طلبات HTTP، نحتاج أيضاً إلى مفهوم ملفات تعريف الارتباط (cookies) فلنصرّح بها:

sig Cookie {
  domains: set Domain
}

كل ملف تعريف ارتباط مُعرَّف بنطاق (نطاقات)؛ وهذا يجسّد حقيقة أنّ ملف تعريف الارتباط يمكن أن ينطبق على *.mit.edu، وهو ما يشمل جميع النطاقات التي تنتهي باللاحقة mit.edu.

وأخيراً، يمكننا أن نجمع كل ذلك معاً لنبني نموذجاً لطلبات HTTP:

abstract sig HttpRequest extends Call {
  url: Url,
  sentCookies: set Cookie,
  body: lone Resource,
  receivedCookies: set Cookie,
  response: lone Resource,
}{
  from in Client
  to in Dns.map[url.host]
}

نحن نمذذج طلب HTTP واستجابته في عنصر واحد؛ فـ url وsentCookies وbody يرسلها العميل، بينما receivedCookies وresponse تُرسَل استجابةً من الخادم.

وحين كتبنا توقيع HttpRequest، وجدنا أنه يتضمّن خصائص عامة في الاستدعاءات، وهي أنها تكون من أشياء محددة إلى أشياء محددة. لذلك كتبنا في الواقع وحدة Alloy صغيرة تصريحاً بتوقيع Call، ولكي نستخدمها هنا نحتاج إلى استيرادها:

open call[Endpoint]

إنها وحدة متعددة الأشكال (polymorphic module)، لذا تُنشأ بنوع Endpoint، وهو مجموعة الأشياء التي تُوجَّه منها الاستدعاءات وإليها. (وتظهر الوحدة كاملة في \aosasecref{500l.sop.appendix}.)

وتتبع تصريحات الحقول في HttpRequest مجموعة من القيود. وينطبق كل قيد من هذه القيود على جميع أعضاء مجموعة طلبات HTTP. وتقول هذه القيود إن (1) كل طلب يأتي من عميل، و(2) كل طلب يُرسَل إلى أحد الخوادم التي يحدّدها مضيف العنوان ضمن ربط DNS.

ومن أبرز مزايا Alloy أنه يمكن تنفيذ النموذج في أي وقت، مهما كان بسيطاً أو مفصّلاً، لتوليد نماذج نظام نموذجية. فلنستخدم الأمر run لنطلب من محلّل Alloy تنفيذ نموذج HTTP الذي بلغناه حتى الآن:

run {} for 3	-- generate an instance with up to 3 objects of every signature type

وفي اللحظة التي يجد فيها المحلّل نموذجاً ممكناً للنظام، ينتج تلقائياً مخطّطاً لذلك النموذج، كما في fig http 1.

يُظهر هذا النموذج عميلاً (يمثّله العنصر Client) يُرسِل HttpRequest إلى Server، الذي يعود بدوره بمورد عنصر، ويطلب من العميل أن يخزّن Cookie عند Domain.

ولاحظ أن المورد المُعادة من الطلب (Resource1) غير موجود في الخادم. فقد أهملنا أن نذكر حقيقةً بديهية عن الخادم،وهي أن كل استجابة لطلب هي مورد يخزّنه الخادم. يمكننا العودة إلى تعريفنا لـ HttpRequest وإضافة قيد:

abstract sig HttpRequest extends Call { ... }{
  ...
  response = to.resources[url.path]
}

وإعادة التشغيل الآن تنتج نماذج خالية من ذلك الخلل.

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

check { 
    all r1, r2: HttpRequest | r1.url = r2.url implies r1.response = r2.response 
} for 3 

بالإعطاء لهذا الأمر check، يستكشف المحلّل كل سلوك ممكن للنظام (حتى الحد المحدَّد)، وعندما يجد سلوكاً ينتهك الخاصية، يعرض ذلك النموذج بوصفه مثالاً مضاداً (counterexample)، كما هو مبيّن في fig http 2a و fig http 2b.

يُظهر هذا المثال المضاد مرة أخرى طلب HTTP يُنجَزه عميل، لكن مع خادمين مختلفين. (وفي المُصوِّر البصري لـ Alloy، تُميَّز العناصر من النوع نفسه بإلحاق لواحق رقمية بأسمائها؛ وإذا كان هناك عنصر واحد فقط من نوع معيّن فلا تُضاف أي لاحقة. وكل اسم يظهر في مخطّط لقطة هو اسم عنصر. لذا—وربما بدا ذلك مربكاً في أول نظرة—فالأسماء Domain وPath وResource وUrl تشير جميعها إلى عناصر مفردة، لا إلى أنواع.)

لاحظ أن DNS يربط Domain بـ Server0 وServer1 معاً (وهذا في الواقع ممارسة شائعة لموازنة الحمل)، لكن Server1 فقط هو ما يربط Path بعنصر مورد، مما يجعل HttpRequest1 ينتج استجابة فارغة: خطأ آخر في نموذجنا. ولإصلاحه، نضيف حقيقةَ (fact) في Alloy تسجّل أن أي خادمين يربط DNS بينهما مضيف واحدَ لهما، يوفّران مجموعة الموارد نفسها:

fact ServerAssumption {
  all s1, s2: Server | 
    (some Dns.map.s1 & Dns.map.s2) implies s1.resources = s2.resources
}

وحين نعيد تشغيل الأمر check بعد إضافة هذه الحقيقة، لم يعد المحلّل يبلّغ عن أي مثال مضاد للخاصية. وهذا لا يعني أن الخاصية قد بُرهن أنها صادقة، إذ قد يوجد مثال مضاد في نطاق أكبر. لكن من المرجّح ألّا تكون الخاصية خاطئة، لأن المحلّل قد اختَبَر جميع النماذج الممكنة التي تتضمّن 3 عناصر من كل نوع.

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

المتصفّح

لنقدّم الآن المتصفّحات إلى نموذجنا:

sig Browser extends Client {
  documents: Document -> Time,
  cookies: Cookie -> Time,
}

هذا هو مثالنا الأول على توقيع له حقول ديناميكية. فلا لدى Alloy مفاهيم مدمجة للزمن أو للسلوك، مما يعني أنه يمكن استخدام مجموعة من الأنماط (idioms) المختلفة. وفي هذا النموذج نستخدم نمطاً شائعاً تُقدَّم به فكرة Time وتُرفَق كعمود أخير لكل حقل متغيّر مع الزمن. فمثلاً، التعبير b.cookies.t يمثّل مجموعة ملفات تعريف الارتباط المخزّنة في المتصفّح b عند زمن معيّن t. وعلى نحو مماثل، يرتبط حقل documents مجموعة من المستندات بكل متصفّح عند زمن معيّن. (لمزيد من التفاصيل حول كيفية نمذجة السلوك الديناميكي، انظر \aosasecref{500l.sop.appendix}.)

تُنشأ المستندات من استجابة لطلب HTTP. ويمكن أيضاً إتلافها إذا أغلق المستخدم لسان تبويب أو المتصفّح مثلاً، لكننا نُسقط ذلك من النموذج. ولكل مستند عنوان URL (العنوان الذي أُنشئ منه المستند)، ومحتوى (DOM)، ونطاق:

sig Document {
  src: Url,
  content: Resource -> Time,
  domain: Domain -> Time
}

وإدراج عمود Time في الحقلين الأخيرين يخبرنا أنهما يمكن أن يتغيّرا مع الزمن، وإغناؤه عن الحقل الأول (src، ويمثّل عنوان URL المصدر للمستند) يدلّ على أن عنوان URL المصدر ثابت.

ولنمذجة أثر طلب HTTP على متصفّح، نقدّم توقيعاً جديداً، إذ ليس كل طلبات HTTP ستنشأ من مستوى المتصفّح؛ فالبقية ستأتي من السكربتات.

sig BrowserHttpRequest extends HttpRequest {
  doc: Document
}{
  -- the request comes from a browser
  from in Browser
  -- the cookies being sent exist in the browser at the time of the request
  sentCookies in from.cookies.start
  -- every cookie sent must be scoped to the url of the request
  all c: sentCookies | url.host in c.domains

  -- a new document is created to display the content of the response
  documents.end = documents.start + from -> doc
  -- the new document has the response as its contents
  content.end = content.start ++ doc -> response
  -- the new document has the host of the url as its domain
  domain.end = domain.start ++ doc -> url.host
  -- the document's source field is the url of the request
  doc.src = url

  -- new cookies are stored by the browser
  cookies.end = cookies.start + from -> sentCookies
}

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

فمثلاً، لفهم القيد documents.end = documents.start + from -> doc تذكّر أن documents علاقة من ثلاثة أعمدة على المتصفّحات والمستندات والأزمنة. ويأتي الحقلان start وend من تصريح Call (الذي لم نره بعد، لكنه مُدرَج في القائمة في نهاية الفصل)، ويمثّلان زمنَي بداية الاستدعاء ونهايته. ويعطي التعبير documents.end الربط من المتصفّحات إلى المستندات عند انتهاء الاستدعاء. لذا يقول هذا القيد إن الربط بعد الاستدعاء هو نفسه، باستثناء مُدخل جديد في الجدول يربط from بـ doc.

وتستخدم بعض القيود مشغّل الاستبدال العلائقي ++: فـ e1 ++ e2 يحتوي جميع الثنائيات (tuples) في e2، إضافةً إلى أي ثنائيات في e1 يكون عنصرها الأول ليس العنصر الأول لأي ثنائية في e2. فمثلاً، القيد content.end = content.start ++ doc -> response يقول إن ربط content بعد الاستدعاء سيُحدَّث ليربط doc بـ response (مستبدلاً أي ربط سابق لـ doc). ولو استخدمنا مشغّل الاتحاد + بدلاً من ذلك، لأمكن (على نحو غير صحيح) أن يُربط المستند نفسه بعدة موارد في الحالة اللاحقة.

السكربت

بعد ذلك، سنبني على نموذجي HTTP والمتصفّح لنقدّم السكربتات من جهة العميل (client-side scripts)، وهي قطع شيفرة (عادةً بـ JavaScript) تُنفَّذ داخل مستند في المتصفّح (context).

sig Script extends Client { context: Document }

السكربت كيان ديناميكي يستطيع أن ينفّذ نوعين مختلفين من الأفعال: (1) أن يُرسِل طلبات HTTP (أي طلبات Ajax)، و(2) أن ينفّذ عمليات المتصفّح لتعديل محتوى المستند وخصائصه. ومرونة السكربتات من جهة العميل إحدى المحفّزات الرئيسية للتطوّر السريع لـ Web 2.0، لكنها أيضاً السبب الذي أُنشئت سياسة الأصل نفسه من أجله في المقام الأول. فبدون سياسة الأصل نفسه، كان بإمكان السكربتات أن تُرسِل طلبات اعتباطية إلى الخوادم، أو أن تعدّل المستندات داخل المتصفّح بحرية—وكون أمراً سيئاً إن اتضح أن واحداً أو أكثر من تلك السكربتات خبيث.

يستطيع السكربت أن يتواصل مع خادم بإرسال XmlHttpRequest:

sig XmlHttpRequest extends HttpRequest {}{
  from in Script
  noBrowserChange[start, end] and noDocumentChange[start, end]
}

يمكن استخدام XmlHttpRequest من قِبل سكربت لإرسال/استقبال الموارد إلى/من خادم، لكن بخلاف BrowserHttpRequest، لا يؤدّي فوراً إلى إنشاء صفحة جديدة أو إلى تغييرات أخرى في المتصفّح ومستنداته. وللقول إن استدعاءً لا يعدّل هذه الجوانب من النظام، نعرّف مسندَين هما noBrowserChange وnoDocumentChange:

pred noBrowserChange[start, end: Time] {
  documents.end = documents.start and cookies.end = cookies.start  
}
pred noDocumentChange[start, end: Time] {
  content.end = content.start and domain.end = domain.start  
}

ما نوع العمليات التي يمكن أن ينفّذها السكربت على المستندات؟ أولاً، نقدّم فكرة عامة عن عمليات المتصفّح (browser operations) لتمثيل مجموعة من دوال واجهة المتصفّح (browser API) التي يمكن استدعاؤها من قِبل سكربت:

abstract sig BrowserOp extends Call { doc: Document }{
  from in Script and to in Browser
  doc + from.context in to.documents.start
  noBrowserChange[start, end]
}

يشير الحقل doc إلى المستند الذي سيُتّاح لهذا الاستدعاء أو ستُعدَّل محتوياته. ويقول القيد الثاني في حقائق التوقيع إن كلاً من doc والمستند الذي يُنفَّذ فيه السكربت (from.context) يجب أن يكونا مستندين موجودين حالياً داخل المتصفّح. وأخيراً، قد يعدّل BrowserOp حالة مستند، لكنه لا يعدّل مجموعة المستندات أو ملفات تعريف الارتباط المخزّنة في المتصفّح. (في الواقع، يمكن ربط ملفات تعريف الارتباط بمستند وتعديلها باستخدام واجهة متصفّح، لكننا نُسقط هذا التفصيل الآن.)

يستطيع السكربت أن يقرأ من أجزاء مختلفة من المستند وأن يكتب إليها (وهي ما تُسمّى عادةً عناصر DOM). وفي متصفّح نموذجي، هناك عدد كبير من دوال واجهة المتصفّح للوصول إلى DOM (مثل document.getElementById)، لكن حصر جميعها ليس مهماً لغرضنا. وبدلاً من ذلك، سنكتفي بتجميعها في نوعين—ReadDom وWriteDom—ونمذجة التعديلات بوصفها استبدالات شاملة للمستند بأكمله:

sig ReadDom extends BrowserOp { result: Resource }{
  result = doc.content.start
  noDocumentChange[start, end]
}
sig WriteDom extends BrowserOp { newDom: Resource }{
  content.end = content.start ++ doc -> newDom
  domain.end = domain.start
}

يُعيد ReadDom محتوى المستند الهدف لكنه لا يعدّله؛ أما WriteDom فيضبط المحتوى الجديد للمستند الهدف على newDom.

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

تطبيقات نموذجية

كما رأينا سابقاً، عند إعطاء أمر run أو check، يولّد محلّل Alloy سيناريو (إن وُجد) يتسق مع وصف النظام في النموذج. وافتراضياً، يختار المحلّل بشكل عشوائي أيّ سيناريو ممكن من سيناريوهات النظام (حتى الحد المحدَّد)، ويأسند معرّفات رقمية لنسخ التوقيع (Server0 وBrowser1 وما إلى ذلك) في السيناريو.

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

في Alloy، تقدّم الكلمات المفتاحية one sig توقيعاً من نوع مفرد (singleton) يحتوي على عنصر واحد بالضبط؛ وقد رأينا مثالاً أعلاه مع Dns. ويمكن استخدام هذه الصياغة لتحديد ذرّيات ملموسة (concrete atoms). فمثلاً، للقول إن هناك صفحة صندوق وارد واحدة ولافتة إعلانية واحدة (كلٌّ منهما مستند)، يمكننا أن نكتب:

one sig InboxPage, AdBanner extends Document {}

مع هذا التصريح، سيحتوي كل سيناريو يولّده Alloy على هذين العنصرين من Document على الأقل.

وعلى نحو مماثل، يمكننا تحديد خوادم ونطاقات معيّنة وهكذا، بقيد (أسميّناه Configuration) يحدّد العلاقات بينها:

one sig EmailServer, EvilServer extends Server {}
one sig EvilScript extends Script {}
one sig EmailDomain, EvilDomain extends Domain {}
fact Configuration {
  EvilScript.context = AdBanner
  InboxPage.domain.first = EmailDomain
  AdBanner.domain.first = EvilDomain  
  Dns.map = EmailDomain -> EmailServer + EvilDomain -> EvilServer
}

فمثلاً، يحدّد القيد الأخير في هذه الحقيقة كيف تهيّأ DNS لتربط أسماء النطاقات بالخادمين في نظامنا. وبدون هذا القيد، قد يولّد محلّل Alloy سيناريوهات تُربط فيها EmailDomain بـ EvilServer، وهي سيناريوهات لا تهمّنا. (وفي الممارسة العملية، قد يكون هذا الربط ممكناً نتيجة لهجوم يُعرف بـ خداع DNS (DNS spoofing)، لكننا سنستبعده من نموذجنا لأنه يقع خارج فئة الهجمات التي صُمّمت سياسة الأصل نفسه لمنعها.)

لنقدّم تطبيقين إضافيين: تقويماً على شبكة الويب ومنشوراً مدوّناً (blog):

one sig CalendarServer, BlogServer extends Document {} 
one sig CalendarDomain, BlogDomain extends Domain {}

وينبغي أن نحدّث القيد الخاص بربط DNS أعلاه ليُضمّن أسماء النطاقات لهذين الخادمين:

fact Configuration {
  ...
  Dns.map = EmailDomain -> EmailServer + EvilDomain -> EvilServer + 
            CalendarDomain -> CalendarServer + BlogDomain -> BlogServer  
}

وإضافةً إلى ذلك، لنفترض أن تطبيقات البريد والمدوّن والتقويم كلها طوّرتها مؤسسة واحدة، وبالتالي تتشارك اسم النطاق الأساسي نفسه. ومن المفاهيمي أن نتخيّل EmailServer وCalendarServer لهما نطاقان فرعيان هما email وcalendar يتشاركان example.com كنطاق أعلى مشترك. وفي نموذجنا، يمكن تمثيل ذلك بإدخال اسم نطاق يستوعب (subsumes) نطاقات أخرى:

one sig ExampleDomain extends Domain {}{
  subsumes = EmailDomain + EvilDomain + CalendarDomain + this
}   

لاحظ أن this مُدرَج كعضو في subsumes، لأن كل اسم نطاق يستوعب نفسه.

وهناك تفاصيل أخرى عن هذه التطبيقات نُسقطها هنا (انظر example.als للحصول على النموذج الكامل). لكننا سنعود إلى هذه التطبيقات بوصفها المثال الاسترشادي طوال بقية هذا الفصل.

خصائص الأمان

قبل أن نصل إلى سياسة الأصل نفسه بحد ذاتها، هناك سؤال مهم لم نناقشه بعد: ما الذي نعنيه بالضبط حين نقول إن نظامنا آمن؟

ولن يكون مفاجئاً أن الإجابة عن هذا السؤال صعبة. فغرضنا هنا سنلجأ إلى مفهومين مدروسين جيداً في أمن المعلومات—السرّية (confidentiality) و_السلامة_ (integrity). ويتناول كل من هذين المفهومين كيفية السماح للمعلومات بأن تعبر أجزاء النظام المختلفة. وبعبارة تقريبية، تعني السرّية أن جزءاً حرجاً من البيانات لا ينبغي أن يكون في متناول إلا الأجزاء التي تُعدّ موثوقة، بينما تعني السلامة أن الأجزاء الموثوقة لا تعتمد إلا على بيانات لم تُعدَّل بشكل خبيث.

خصائص تدفّق البيانات

ولتحديد خصائص الأمان هذه بدقّة أكبر، نحتاج أولاً إلى تعريف ما يعنيه أن يتدفّق (flows) جزء من البيانات من جزء من النظام إلى جزء آخر. وفي نموذجنا حتى الآن، وصفنا التفاعلات بين نقطتَي نهاية بأنها تتم عبر الاستدعاءات (calls)؛ فمثلاً يتفاعل المتصفّح مع خادم عبر إجراء طلبات HTTP، ويتفاعل سكربت مع المتصفّح عبر استدعاء عمليات واجهة المتصفّح. ومن البديهي، أثناء كل استدعاء، قد يتدفّق جزء من البيانات من نقطة نهاية إلى أخرى بوصفه وسيطاً (argument) أو قيمةَ إرجاع (return value) للاستدعاء. لتمثيل ذلك، نقدّم فكرة DataflowCall في النموذج، ونربط كل استدعاء بمجموعة حقول بيانات هي args وreturns:

sig Data in Resource + Cookie {}

sig DataflowCall in Call {
  args, returns: set Data,  --- arguments and return data of this call
}{
 this in HttpRequest implies
    args = this.sentCookies + this.body and
    returns = this.receivedCookies + this.response
 ...
}

فمثلاً، أثناء كل استدعاء من نوع HttpRequest، ينقل العميل sentCookies وbody إلى الخادم، ويتلقّى receivedCookies وresponse كقيم إرجاع.

وبوجه عام، تتدفّق الوسائط من مُرسِل الاستدعاء إلى المُستلِم، وتتدفّق قيم الإرجاع من المُستلِم إلى المُرسِل. وهذا يعني أن الطريقة الوحيدة المتاحة لنقطة نهاية للوصول إلى جزء جديد من البيانات هي أن تتلقّاه كوسيط لاستدعاء تقبله، أو كقيمة إرجاع لاستدعاء تستدعيه. ونقدّم فكرة DataflowModule، ونُسند الحقل accesses لتمثيل مجموعة عناصر البيانات التي يمكن للوحدة الوصول إليها في كل خطوة زمنية:

sig DataflowModule in Endpoint {
  -- Set of data that this component initially owns
  accesses: Data -> Time
}{
  all d: Data, t: Time - first |
	 -- This endpoint can only access a piece of data "d" at time "t" only when
    d -> t in accesses implies
      -- (1) It already had access in the previous time step, or
      d -> t.prev in accesses or
      -- there is some call "c" that ended at "t" such that
      some c: Call & end.t |
        -- (2) the endpoint receives "c" that carries "d" as one of its arguments or
        c.to = this and d in c.args or
        -- (3) the endpoint sends "c" that returns "d" 
        c.from = this and d in c.returns 
}

كما نحتاج إلى تقييد عناصر البيانات التي يمكن للوحدة أن تقدّمها كوسائط أو كقيم إرجاع لاستدعاء. وإلّا فقد حصلنا على سيناريوهات غريبة تستطيع فيها وحدة إجراء استدعاء بوسيط لا تملك الوصول إليه:

sig DataflowCall in Call { ... } {
  -- (1) Any arguments must be accessible to the sender
  args in from.accesses.start
  -- (2) Any data returned from this call must be accessible to the receiver
  returns in to.accesses.start
}

والآن وقد توفّرت لنا وسيلة لوصف تدفّق البيانات بين أجزاء النظام المختلفة، أصبحنا (إلى حد كبير) قادرين على صوغ خصائص الأمان التي تهمّنا. لكن تذكّر أن السرّية والسلامة مفهومان يعتمدان على السياق (context-dependent)؛ فهاتان الخاصيتان لا معنى لهما إلا إذا استطعنا الحديث عن بعض الوكلاء داخل النظام باعتبارهم موثوقين (أو خبيثين). وعلى نحو مماثل، ليس كل المعلومات متساوية الأهمية: فنحتاج إلى التمييز بين عناصر البيانات التي نعدّها حرجة أو خبيثة (أو لا هذه ولا تلك):

sig TrustedModule, MaliciousModule in DataflowModule {}
sig CriticalData, MaliciousData in Data {}

وعندئذٍ يمكن صوغ خاصية السرّية بوصفها تأكيداً (assertion) على تدفّق البيانات الحرجة إلى الأجزاء غير الموثوقة من النظام:

// No malicious module should be able to access critical data
assert Confidentiality {
  no m: Module - TrustedModule, t: Time |
    some CriticalData & m.accesses.t 
}

أما خاصية السلامة فهي نظير خاصية السرّية:

// No malicious data should ever flow into a trusted module
assert Integrity {
  no m: TrustedModule, t: Time | 
    some MaliciousData & m.accesses.t
}

نموذج التهديد

نموذج التهديد (threat model) يصف مجموعة أفعال قد ينفّذها المهاجم في محاولة لاختراق خاصية أمان ما في نظام. ويعدّ بناء نموذج التهديد خطوة مهمة في أي تصميم نظام آمن؛ فهو يتيح لنا تحديد الافتراضات (التي قد تكون غير صحيحة) التي لدينا عن النظام وعن بيئته، وترتيب أولويات أنواع المخاطر التي يلزم تخفيفها.

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

فحص الخصائص

والآن وقد عرّفنا خصائص الأمان وسلوك المهاجم، فلنُرِ كيف يمكن استخدام محلّل Alloy لفحص هذه الخصائص تلقائياً على أنها تصمد حتى في حضور المهاجم. فعند إعطائه أمر check، يستكشف المحلّل كل مسارات تدفّق البيانات الممكنة في النظام وينتج مثالاً مضاداً (إن وُجد) يُظهر كيف يمكن لتأكيد ما أن يُنتهك:

check Confidentiality for 5

فمثلاً، عند فحص نموذج تطبيقنا النموذجي مقابل خاصية السرّية، يولّد المحلّل السيناريو المبيّن في fig attack 1a و fig attack 1b، وهو يُظهر كيف يمكن لـ EvilScript الوصول إلى جزء من البيانات الحرجة (MyInboxInfo).

ينطوي هذا المثال المضاد على خطوتين. في الخطوة الأولى (fig attack 1a)، يقرأ EvilScript الذي يُنفَّذ داخل AdBanner المنتمي إلى EvilDomain محتوى InboxPage، وهو محتوى مصدره EmailDomain. وفي الخطوة التالية (fig attack 1b)، يُرسِل EvilScript المحتوى نفسه (MyInboxInfo) إلى EvilServer عبر استدعاء XmlHtttpRequest. وجوهر المشكلة هنا أن سكربتاً يُنفَّذ تحت نطاق واحد قادر على قراءة محتوى مستند من نطاق آخر؛ وكما سنرى في القسم التالي، فهذا تحديداً أحد السيناريوهات التي صُمّمت سياسة الأصل نفسه لمنعها.

قد تكون هناك أمثلة مضادة متعدّدة لتأكيد واحد. لننظر في fig attack 2، وهو يُظهر طريقة أخرى قد ينتهك بها النظام خاصية السرّية.

في هذا السيناريو، بدلاً من قراءة محتوى صفحة صندوق الوارد، يُرسِل EvilScript طلب GetInboxInfo مباشرةً إلى EmailServer. ولاحظ أن الطلب يتضمّن ملف تعريف ارتباط (MyCookie) مُعرَّفاً على النطاق نفسه الذي يقع عليه الخادم الهدف. وهذا قد يكون خطيراً، فإذا استُخدم ملف تعريف الارتباط لتمثيل هوية المستخدم (كملف تعريف ارتباط جلسة مثلاً)، استطاع EvilScript أن يتقمّص شخصية المستخدم فعلياً ويخدع الخادم ويُجبره على الرد ببيانات المستخدم الخاصة (MyInboxInfo). وهنا المشكلة أيضاً تتعلق بالطرق المتساهلة التي يمكن بها للسكربت الوصول إلى المعلومات عبر النطاقات المختلفة—وهي تحديداً أن سكربتاً يُنفَّذ تحت نطاق واحد قادر على إجراء طلب HTTP إلى خادم له نطاق مختلف.

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

سياسة الأصل نفسه

قبل أن نتمكن من صياغة سياسة الأصل نفسه، ينبغي أولاً أن نقدّم فكرة الأصل (origin)، وهو يتألف من بروتوكول ومضيف ومنفذ اختياري:

sig Origin {
  protocol: Protocol,
  host: Domain,
  port: lone Port
}

ولراحة الاستخدام، لنعرّف دالةً تعطي عنوان URL فتُعيد الأصل المقابل له:

fun origin[u: Url] : Origin {
    {o: Origin | o.protocol = u.protocol and o.host = u.host and o.port = u.port }
}

أما سياسة الأصل نفسه نفسها فلها جزآن، يقيّدان قدرة السكربت على (1) إجراء استدعاءات واجهة DOM، و(2) إرسال طلبات HTTP. ويقول الجزء الأول من السياسة إن السكربت لا يستطيع إلا أن يقرأ من مستند ويكتب إليه إذا جاء من أصل السكربت نفسه:

fact domSop {
  all o: ReadDom + WriteDom |  let target = o.doc, caller = o.from.context |
    origin[target] = origin[caller] 
}

فمثل هذا سيناريو السكربت الأول (من القسم السابق) غير ممكن في ظل domSop، لأن Script غير مسموح له باستدعاء ReadDom على مستند من أصل مختلف.

أما الجزء الثاني من السياسة فيقول إن السكربت لا يمكنه إرسال طلب HTTP إلى خادم ما لم يكن سياقه (context) هو نفسه أصل عنوان URL الهدف—وهو ما يمنع فعلياً سيناريوهات مثل سيناريو السكربت الثاني.

fact xmlHttpReqSop { 
  all x: XmlHttpRequest | origin[x.url] = origin[x.from.context.src] 
}

وكما يمكننا أن نرى، فقد صُمّمت سياسة الأصل نفسه لمنع نوعَي الثغرات اللذين قد ينشآن عن أفعال سكربت خبيث؛ فبدونها كانت شبكة الويب مكاناً أكثر خطورة بكثير مما هي عليه اليوم.

غير أنه تبيّن أن سياسة الأصل نفسه قد تكون مقيّدة أكثر من اللازم. فمثلاً، أحياناً ما تريد فعلاً السماح بالاتصال بين مستندين من أصلين مختلفين. وبموجب التعريف أعلاه للأصل، لن يستطيع سكربت من foo.example.com قراءة محتوى bar.example.com، أو إرسال طلب HTTP إلى www.example.com، لأن هذه كلّها تُعدّ مضيفات متمايزة.

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

تقنيات تجاوز سياسة الأصل نفسه

سياسة الأصل نفسه مثال كلاسيكي على التوتر بين الوظيفة والأمان؛ فنحن نريد التأكّد من أن مواقعنا متينة وعملية، لكن آلية تأمينها قد تعترض الطريق أحياناً. وبالفعل، حين قُدِّمت سياسة الأصل نفسه في البداية، واجّه المطوّرون صعوبات في بناء مواقع تستعمل الاتصال عبر النطاقات استخداماً مشروعاً (مثل التطبيقات المركّبة mashups).

وسنتناول في هذا القسم أربع تقنيات ابتكرها مطوّرو الويب واستخدموها على نطاق واسع لتجاوز القيود التي تفرضها سياسة الأصل نفسه: (1) تخفيف الخاصية document.domain؛ و(2) JSONP؛ و(3) PostMessage؛ و(4) CORS أي تبادل الموارد عبر المصادر. هذه أدوات قيّمة، لكنّ استعمالها من دون حذر قد يجعل تطبيق ويب معرّضاً بالضبط لأنواع الهجمات التي صُمّمت سياسة الأصل نفسه أصلاً لصدّها.

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

check Confidentiality for 5
check Integrity for 5

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

الخاصية document.domain

وإلى جانب التقنية الأولى في قائمتنا، سننظر في استعمال الخاصية document.domain وسيلةً لتجاوز سياسة الأصل نفسه. فالفكرة وراء هذه التقنية هي السماح لمستندين من أصلين مختلفين بالوصول إلى DOM كلٍّ منهما بمجرد ضبط الخاصية document.domain على القيمة نفسها. فمثلاً، يستطيع سكربت من email.example.com أن يقرأ DOM مستند من calendar.example.com أو يكتب فيه، إذا ضبطت السكربتات في المستندين الخاصية document.domain على example.com (بافتراض أن لكل من عنوانين المصدرين البروتوكول والمنفذ نفسيهما).

ونمذجة سلوك ضبط الخاصية document.domain نقدّمها كنوع من عمليات المتصفّح اسمه SetDomain:

// Modify the document.domain property
sig SetDomain extends BrowserOp { newDomain: Domain }{
  doc = from.context
  domain.end = domain.start ++ doc -> newDomain
  -- no change to the content of the document
  content.end = content.start
}

يمثّل الحقل newDomain القيمة التي ينبغي أن تُضبط عليها الخاصية. غير أنّ ثمّة تحفّظاً: فلا تستطيع السكربتات أن تضبط خاصية النطاق إلّا على جزء أيمن (right-hand) ومُعرَّف بالكامل (fully qualified) من اسم مضيفها. (أي أن email.example.com تستطيع ضبطها على example.com لكن ليس على google.com.) ونستخدم حقيقة (fact) لالتقاط قاعدة النطاقات الفرعية هذه:

// Scripts can only set the domain property to only one that is a right-hand,
// fully-qualified fragment of its hostname
fact setDomainRule {
  all d: Document | d.src.host in (d.domain.Time).subsumes
}

ولولا هذه القاعدة، لأمكن لأي موقع أن يضبط الخاصية document.domain على أي قيمة، ما يعني أنه يمكن لموقع خبيث أن يضبط خاصية النطاق على نطاقك المصرفي، وأن يحمّل حسابك المصرفي في إطار مضمّن (iframe)، وأن (بافتراض أن صفحة البنك قد ضبطت بدورها خاصية نطاقها) يقرأ DOM صفحة البنك.

لنعد إلى تعريفنا الأصلي لسياسة الأصل نفسه، ونخفّف قيده على الوصول إلى DOM حتى نأخذ في الحسبان أثر الخاصية document.domain. فإذا ضبط سكربتان الخاصية على القيمة نفسها، وكان لهما البروتوكول والمنفذ نفسيهما، أمكن لهما التفاعل مع بعضهما (أي قراءة DOM كلٍّ منهما والكتابة فيه).

fact domSop {
  -- For every successful read/write DOM operation,
  all o: ReadDom + WriteDom |  let target = o.doc, caller = o.from.context |
    -- (1) target and caller documents are from the same origin, or
    origin[target] = origin[caller] or
    -- (2) domain properties of both documents have been modified
    (target + caller in (o.prevs <: SetDomain).doc and
      -- ...and they have matching origin values.
      currOrigin[target, o.start] = currOrigin[caller, o.start])
}

وهنا، currOrigin[d, t] دالة تعيد أصل المستند d بعد أن تكون الخاصية document.domain عند الزمن t هي اسم مضيفه.

ومن الجدير بالإشارة إلى أن خاصتي document.domain في المستندين كلاهما يجب أن تُضبطا صراحةً (explictly) في وقت ما بعد تحميلهما في المتصفّح. لنفترض أن المستند A محمَّل من example.com، وأن خاصية نطاق المستند B المحمَّل من calendar.example.com عُدِّلت لتصبح example.com. فرغم أن المستندين أصبح لهما الآن خاصية نطاق واحدة، إلا أنهما لن يستطيعا التفاعل مع بعضهما، ما لم يضبط المستند A بدوره خاصيته صراحةً على example.com. ويبدو هذا في البداية سلوكاً غريباً نوعاً ما. غير أنه بدون هذا، يمكن أن تحدث أمور سيئة مختلفة. فمثلاً، قد يتعرّض موقع ما لهجوم برمجة عابرة للمواقع (cross-site scripting) من نطاقاته الفرعية: فقد يعدّل سكربت خبيث في المستند B خاصية نطاقه لتصبح example.com، ثم التلاعب بـ DOM المستند A، رغم أن الأخير لم ينوِ إطلاقاً التفاعل مع المستند B.

التحليل: الآن بعد أن خفّفنا سياسة الأصل نفسه للسماح بالاتصال عبر الأصول في ظروف معيّنة، هل ما تزال الضمانات الأمنية لسياسة الأصل نفسه تصمد؟ لنطلب من محلّل Alloy أن يخبرنا ما إذا كان يمكن للمهاجم أن يُسيء استعمال الخاصية document.domain للوصول إلى بيانات المستخدم الحسّاسة أو التلاعب بها.

وبالفعل، بالنظر إلى تعريف سياسة الأصل نفسه الجديد المخفَّف، يولّد المحلّل سيناريو مثالاً مضاداً لخاصية السرّية:

check Confidentiality for 5

يتكوّن هذا السيناريو من خمس خطوات؛ تُظهر الخطوات الثلاث الأولى استعمالاً نموذجياً لـ document.domain، حيث يتبادل مستندان من أصلين متباعدين، وهما CalendarPage وInboxPage، الاتصال يضبطان خاصية النطاق فيهما على قيمة مشتركة (ExampleDomain). وتُقدّم الخطوتان الأخيرتان مستنداً آخر هو BlogPage، قد أُخترق بسكربت خبيث يحاول الوصول إلى محتوى المستندين الآخرين.

في بداية السيناريو (fig setdomain 1a و fig setdomain 1b)، تملك InboxPage و CalendarPage خاصيتي نطاق بقيمتين متباعدتين (EmailDomain وExampleDomain على التوالي)، لذا سيمنع المتصفّح أحدهما من الوصول إلى DOM الآخر. وتنفّذ السكربتات العاملة داخل المستندين (InboxScript وCalendarScript) كلٌّ منهما عملية SetDomain ليعدّل خاصية نطاقه إلى ExampleDomain (وهو مسموح لأن ExampleDomain نطاق أعلى للنطاق الأصلي).

وبعد أن فعلوا ذلك، أصبح بإمكانهم الآن الوصول إلى DOM بعضهم البعض عبر تنفيذ عمليات ReadDom أو WriteDom، كما في fig setdomain 1c.

لاحظ أن حين تضبط نطاق email.example.com وcalendar.example.com على example.com، فأنت لا تسمح لهاتين الصفحتين بالاتصال بينهما فحسب، بل تسمح لأي صفحة أخرى لها example.com نطاقاً أعلى (مثل blog.example.com). ويدرك المهاجم ذلك أيضاً، فيبني سكربتاً خاصاً (EvilScript) يعمل داخل صفحة المدونة الخاصة بالمهاجم (BlogPage). وفي الخطوة التالية (fig setdomain 2a)، ينفّذ السكربت عملية SetDomain لتعديل خاصية نطاق BlogPage إلى ExampleDomain.

والآن بعد أن صارت BlogPage تملك خاصية النطاق نفسها التي تملكها المستندان الآخران، استطاعت بنجاح تنفيذ عملية ReadDOM للوصول إلى محتواهما (fig setdomain 2b.)

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

JSON مع حشو (JSONP)

قبل إدخال تبادل الموارد عبر المصادر (CORS) (وسنناقشه قريباً)، كانت JSONP على الأرجح التقنية الأكثر رواجاً لتجاوز قيد سياسة الأصل نفسه على XMLHttpRequest، ولا تزال مستخدمة على نطاق واسع حتى اليوم. وتستغل JSONP حقيقة أن وسوم إدراج السكربتات في HTML (أي <script>) معفاة من سياسة الأصل نفسه*؛ أي أنك تستطيع إدراج سكربت من أي عنوان URL، ويستطيع المتصفّح تنفيذه بسهولة داخل المستند الحالي:

(* بدون هذا الإعفاء، لما أمكن تحميل مكتبات JavaScript، مثل JQuery، من نطاقات أخرى.)

<script src="http://www.example.com/myscript.js"></script>

يمكن لوسم السكربت أن يُستخدم للحصول على شيفرة، لكن كيف نستخدمه لاستقبال بيانات عشوائية (مثل كائن JSON) من نطاق مختلف؟ والمشكلة أن المتصفّح يتوقّع أن يكون محتوى src قطعة شيفرة JavaScript، لذا فإن مجرد توجيهه إلى مصدر بيانات (مثل ملف JSON أو HTML) يؤدّي إلى خطأ نحوي.

ومن الحلول الوسطية أن نلفّ البيانات المرغوبة داخل سلسلة يتعرّف عليها المتصفّح على أنها شيفرة JavaScript صالحة؛ وتُسمّى هذه السلسلة أحياناً الحشو (padding) (ومن هنا اسم «JSON مع حشو»). ويمكن أن يكون هذا الحشو أي شيفرة JavaScript اعتباطية، لكن العرف أنه اسم دالة استدعاء (معرَّفة أصلاً في المستند الحالي) يُفترض أن تُنفَّذ على بيانات الاستجابة:

<script src="http://www.example.com/mydata?jsonp=processData"></script>

يتعرّف الخادم في www.example.com على أنه طلب JSONP، ويلفّ البيانات المطلوبة داخل الوسيط jsonp:

processData(mydata)

وهذا جملة JavaScript صالحة (وهي تطبيق الدالة "processData" على القيمة "mydata")، ينفّذها المتصفّح داخل المستند الحالي.

وفي نموذجنا، تُنمذَج JSONP كنوع من طلبات HTTP يتضمّن مُعرِّف دالة الاستدعاء في الحقل padding. وبعد تلقّي طلب JSONP، يعيد الخادم استجابةً يلتفّ فيها المورد المطلوب (payload) داخل دالة الاستدعاء (cb).

sig CallbackID {}  // identifier of a callback function
// Request sent as a result of <script> tag
sig JsonpRequest in BrowserHttpRequest {
  padding: CallbackID
}{
  response in JsonpResponse
}
sig JsonpResponse in Resource {
  cb: CallbackID,
  payload: Resource
}

وحين يتلقّى المتصفّح الاستجابة، ينفّذ دالة الاستدعاء على الحمولة:

sig JsonpCallback extends EventHandler {
  cb: CallbackID,
  payload: Resource
}{
  causedBy in JsonpRequest
  let resp = causedBy.response | 
    cb = resp.@cb and
    -- result of JSONP request is passed on as an argument to the callback
    payload = resp.@payload
}

(وEventHandler نوع خاص من الاستدعاءات يجب أن يقع في وقت ما بعد استدعاء آخر، ويُشار إليه بـ causedBy؛ وسنستخدم معالِجات الأحداث لنمذجة الأفعال التي ها السكربتات استجابةً لأحداث المتصفّح.)

ولاحظ أن دالة الاستدعاء المنفَّذة هي نفسها التي تتضمّنها الاستجابة (cb = resp.@cb)، لكن ليست بالضرورة هي نفسها padding في طلب JSONP الأصلي. بمعنى آخر، لكي يعمل اتصال JSONP، يتحمّل الخادم مسؤولية بناء استجابة صحيحة تتضمّن الحشو الأصلي بوصفه دالة الاستدعاء (أي ضمان أن JsonRequest.padding = JsonpResponse.cb). ومن حيث المبدأ، يمكن للخادم أن يختار تضمين أي دالة استدعاء (أو أي قطعة JavaScript)، بما في ذلك دالة لا علاقة لها بـ padding في الطلب. وهذا يبرز خطراً محتملاً لـ JSONP: يجب أن يكون الخادم الذي يقبل طلبات JSONP موثوقاً وآمناً، لأنه يملك القدرة على تنفيذ أي قطعة شيفرة JavaScript داخل مستند العميل.

التحليل: فحص الخاصية Confidentiality بمحلّل Alloy يعيد مثالاً مضاداً يُظهر أحد مخاطر JSONP الأمنية المحتملة. وفي هذا السيناريو، يجعل تطبيق التقويم (CalendarServer) موارده متاحة لمواقع الأطراف الثالثة عبر نقطة نهاية JSONP (GetSchedule). وحصراً للوصول إلى تلك الموارد، لا يعيد CalendarServer استجابةً تتضمن جدول المستخدم إلا إذا كان الطلب يتضمّن ملف تعريف ارتباط يحدّد ذلك المستخدم بدقّة.

ولاحظ أن بمجرد أن يوفّر خادم ما نقطة نهاية HTTP كخدمة JSONP، يصبح بإمكان أي شخص إجراء طلب JSONP إليها، بما في ذلك المواقع الخبيثة. وفي هذا السيناريو، تتضمّن صفحة اللافتة الإعلانية من EvilServer وسم سكربت يسبّب طلب GetSchedule، مع دالة استدعاء اسمها Leak بوصفها padding. وعادةً ما لا يملك مطوّر AdBanner وصولاً مباشراً إلى ملف تعريف ارتباط جلسة المستخدم الضحية (MyCookie) لـ CalendarServer. غير أن طلب JSONP يُرسَل إلى CalendarServer، لذا يُضمّنه المتصفّح تلقائياً MyCookie؛ وCalendarServer الذي تلقّى طلب JSONP يحمل MyCookie سيعيد مورد الضحية (MySchedule) ملتفّاً داخل الحشو Leak (fig jsonp 1.)

وفي الخطوة التالية، يفسّر المتصفّح استجابة JSONP على أنها استدعاء لـ Leak(MySchedule) (fig jsonp 2). وبقية الهجوم بسيطة؛ إذ يمكن ببساطة برمجة Leak لتوجيه الوسيط الوارد إلى EvilServer، مما يتيح للمهاجم الوصول إلى المعلومات الحسّاسة للضحية.

وهذا الهجوم، وهو مثال على تزوير الطلب عبر المواقع (cross-site request forgery، CSRF)، يُظهر ضعفاً جوهرياً في JSONP؛ فـ أي موقع على الويب يستطيع إجراء طلب JSONP بمجرد إدراج وسم <script> والوصول إلى الحمولة داخل الحشو. ويمكن التخفيف من هذا الخطر بطريقتين: (1) التأكّد من أن طلب JSONP لا يعيد بيانات حسّاسة أبداً، أو (2) استعمال آلية أخرى بدلاً من ملفات تعريف الارتباط (كالبطاقات السرّية مثلاً) لتفويض الطلب.

PostMessage

PostMessage ميزة جديدة في HTML5 تتيح للسكربتات من مستندين (قد يكون أصلهما مختلفين) أن تتواصل فيما بينهما. وهي تقدّم بديلاً أكثر انضباطاً من طريقة ضبط الخاصية domain، لكنها تحمل مخاطرها الأمنية الخاصة.

PostMessage هي دالة في واجهة المتصفّح تأخذ وسيطين: (1) البيانات المراد إرسالها (message)، و(2) أصل المستند الذي يستقبل الرسالة (targetOrigin):

sig PostMessage extends BrowserOp {
  message: Resource,
  targetOrigin: Origin
}

ولتلقّي رسالة من مستند آخر، يسجّل المستند المستقبِل معالِج أحداث يستدعيه المتصفّح نتيجةً لـ PostMessage:

sig ReceiveMessage extends EventHandler {
  data: Resource,
  srcOrigin: Origin
}{
  causedBy in PostMessage
  -- "ReceiveMessage" event is sent to the script with the correct context
  origin[to.context.src] = causedBy.targetOrigin
  -- messages match
  data = causedBy.@message
  -- the origin of the sender script is provided as "srcOrigin" param 
  srcOrigin = origin[causedBy.@from.context.src]
}

يمرّر المتصفّح وسيطين إلى ReceiveMessage: مورداً (data) يوافق الرسالة المُرسَلة، وأصل المستند المُرسِل (srcOrigin). وتحتوي حقيقة التوقيع على أربعة قيود تضمن أن كل ReceiveMessage سليم التكوين بالنسبة إلى PostMessage المقابل له.

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

ولاحظ أن آلية PostMessage افتراضياً لا تقيّد من يُسمح له بإرسال PostMessage؛ بمعنى آخر، يستطيع أي مستند أن يرسل رسالة إلى مستند آخر ما دام الأخير قد سجّل معالِج ReceiveMessage. فمثلاً، في النموذج المولَّد من Alloy التالي، يرسل EvilScript الذي يعمل داخل AdBanner رسالة PostMessage خبيثة إلى مستند أصله الهدف هو EmailDomain (fig postmessage 1.)

ثم يوجّه المتصفّح هذه الرسالة إلى المستند (المستندات) ذات الأصل المقابل (في هذه الحالة، InboxPage). ما لم يفحص InboxScript قيمة srcOrigin تحديداً لاستبعاد الرسائل القادمة من أصول غير مرغوب فيها، فإن InboxPage سيقبل البيانات الخبيثة، وقد يقود ذلك إلى هجمات أمنية أخرى. (فمثلاً، قد يضمّن قطعة JavaScript لتنفيذ هجوم XSS.) وهذا مبيّن في fig postmessage 1.

وكما يوضّح هذا المثال، فإن PostMessage ليست آمنة افتراضياً، ومن مسؤولية المستند المستقبِل إضافةً إلى ذلك أن يفحص الوسيط srcOrigin للتأكّد من أن الرسالة قادمة من مستند موثوق. وللأسف، فإن كثيراً من المواقع تُسقط هذا الفحص في الممارسة العملية، مما يمكّن مستنداً خبيثاً من حقن محتوى سيّئ ضمن PostMessage^[1].

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

تبادل الموارد عبر المصادر (CORS)

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

وباختصار، تنطوي عملية CORS النموذجية على خطوتين: (1) يُضمّن سكربت يريد الوصول إلى مورد من خادم خارجي، في طلبه، ترويسة "Origin" تحدّد أصل السكربت، و(2) يُضمّن الخادم ترويسة "Access-Control-Allow-Origin" ضمن استجابته، إشارةً إلى مجموعة الأصول المسموح لها بالوصول إلى مورد الخادم. وافتراضياً، من دون CORS، كان المتصفّح يمنع السكربت من إجراء طلب عبر المصادر من الأساس، امتثالاً لسياسة الأصل نفسه. لكن مع تفعيل CORS، يسمح المتصفّح للسكربت بإرسال الطلب والوصول إلى استجابته، لكن فقط إذا كانت "Origin" إحدى الأصول المحدَّدة في "Access-Control-Allow-Origin".

(ويتضمّن CORS إضافةً إلى ذلك فكرة الطلبات التحقّق المسبقة (preflight requests)، التي لا نتناولها هنا، لدعم أنواع معقّدة من الطلبات عبر المصادر إلى جانب GET و POST.)

في Alloy، نمذذج طلب CORS كنوع خاص من XmlHttpRequest، بحقلين إضافيين هما origin وallowedOrigins:

sig CorsRequest in XmlHttpRequest {
  -- "origin" header in request from client
  origin: Origin,
  -- "access-control-allow-origin" header in response from server
  allowedOrigins: set Origin
}{
  from in Script
}

ثم نستخدم حقيقة في Alloy اسمها corsRule لوصف ما الذي يشكّل طلب CORS صالحاً:

fact corsRule {
  all r: CorsRequest |
    -- the origin header of a CORS request matches the script context
    r.origin = origin[r.from.context.src] and
    -- the specified origin is one of the allowed origins
    r.origin in r.allowedOrigins
}

التحليل: هل يمكن إساءة استعمال CORS بطريقة تسمح للمهاجم باختراق أمان موقع موثوق؟ وعند سؤاله، يعيد محلّل Alloy مثالاً مضاداً بسيطاً لخاصية Confidentiality.

وهنا، يقرّر مطوّر تطبيق التقويم أن يشارك بعض موارده مع تطبيقات أخرى باستخدام آلية CORS. وللأسف، ضُبط CalendarServer بحيث يعيد Origin (الذي يمثّل مجموعة قيم الأصول كلها) لترويسة access-control-allow-origin في استجابات CORS. ونتيجةً لذلك، يُسمح لسكربت من أي أصل، بما في ذلك EvilDomain، بإجراء طلب عبر المواقع إلى CalendarServer وقراءة استجابته (fig cors).

يُبرز هذا المثال خطأً شائعاً يرتكبه المطوّرون مع CORS: استعمال القيمة "*" القيمة البديلة لترويسة "access-control-allow-origin"، ما يسمح لأي موقع بالوصول إلى مورد على الخادم. وهذا النمط من الوصول مناسب إذا كان المورد يُعدّ عاماً ومتاحاً للجميع. لكن اتضح أن مواقع كثيرة تستعمل "*" القيمة الافتراضية حتى للموارد الخاصة، فتسمح بذلك عَرَضاً للسكربتات الخبيثة بالوصول إليها عبر طلبات CORS^[2].

ولماذا يستخدم مطوّر القيمة البديلة على الإطلاق؟ تبيّن أن تحديد الأصول المسموح بها قد يكون صعباً، إذ قد لا يتضح وقت التصميم أي الأصول ينبغي منحها الوصول وقت التشغيل (على نحو مشابه لمشكلة PostMessage التي ناقشناها أعلاه). فمثلاً، قد تسمحمعين الخدمة لتطبيقات الأطراف الثالثة بالاشتراك في مواردها ديناميكياً.

الخلاصة

في هذا الفصل، انطلقنا لبناء وثيقة تقدّم فهماً واضحاً لسياسة الأصل نفسه وآلياتها المرتبطة، عبر بناء نموذج (model) للسياسة في لغة اسمها Alloy. ونموذجنا لسياسة الأصل نفسه ليس تطبيقاً بالمعنى التقليدي، ولا يمكن نشره للاستخدام، بخلاف المخرجات المعروضة في الفصول الأخرى. وبدلاً من ذلك، أردنا أن نُظهر العناصر الرئيسية وراء نهجنا في «النمذجة الرشيقة»: (1) البدء بنموذج صغير ومجرَّد للنظام وإضافة التفاصيل على نحو تزايدي حسب الحاجة، و(2) تحديد خصائص يُتوقّع أن يحققها النظام، و(3) تطبيق تحليل صارم (rigorous analysis) لاستكشاف أي عيوب محتملة في تصميم النظام. وبطبيعة الحال، فقد كُتب هذا الفصل بعد وقت طويل من إدخال سياسة الأصل نفسه، لكننا نعتقد أن هذا النوع من النمذجة قد يكون أكثر فائدة لو أُنجز في مرحلة مبكرة من تصميم النظام.

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

ملحق: إعادة استعمال الوحدات في Alloy

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

وفي نموذجنا لسياسة الأصل نفسه، نمذج النظام كمجموعة من نقاط النهاية تتواصل فيما بينها عبر إجراء استدعاء call واحد أو أكثر. وبما أن مفهوم الاستدعاء (call) مفهوم عام إلى حد كبير، فإننا نغلّف وصفه في وحدة Alloy منفصلة، تُستورد من وحدات أخرى تعتمد عليه -- على نحو يشبه المكتبات القياسية في لغات البرمجة:

module call[T] 

في تصريح الوحدة هذا، تمثّل T وسيط نوع (type parameter) يمكن أن يُنشأ بنوع ملموس يُقدَّم عند استيراد الوحدة. وسنرى بعد قليل كيف يُستعمل وسيط النوع هذا.

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

open util/ordering[Time] as ord
sig Time {}

في Alloy، تُعد util/ordering وحدة مدمجة تفرض ترتيباً كلياً (total order) على وسيط النوع، ولذلك فإن استيراد ordering[Time] يمنحنا مجموعة من عناصر Time تتصرّف مثل غيرها من المجموعات المرتّبة كلياً (مثل الأعداد الطبيعية).

ولاحظ أن Time لا تحمل أي شيء مميّز على الإطلاق؛ كان يمكننا أن نسمّيها بأي اسم آخر (مثل Step أو State) دون أن يغيّر ذلك سلوك النموذج إطلاقاً. وكل ما نفعله هنا هو استعمال عمود إضافي في علاقة بوصفه طريقة لتمثيل محتوى حقل عند نقاط مختلفة في تنفيذ النظام؛ فمثلاً cookies في توقيع Browser. وبهذا المعنى، فإن عناصر Time ليست سوى عناصر مساعدة تُستعمل كفهرس من نوع ما.

ويحدث كل استدعاء بين نقطتين زمنيتين—زمنَي start وend— ويرتبط بمُرسِل (يمثّله from) ومستلِم (to):

abstract sig Call { start, end: Time, from, to: T } 

وتذكّر أننا في مناقشتنا لطلبات HTTP استوردنا الوحدة call بتمرير Endpoint كوسيط نوع لها. ونتيجةً لذلك، يُنشأ النوع المُعامَل T بنوع Endpoint، فنحصل على مجموعة من عناصر Call المرتبطة بزوج من نقطتَي الإرسال والاستلام. ويمكن استيراد الوحدة عدّة مرّات؛ فمثلاً يمكننا أن نصرّح بتوقيع اسمه UnixProcess، وأن ننشئ الوحدة call للحصول على مجموعة منفصلة من عناصر Call تُرسَل من عملية Unix إلى أخرى.

---

1. Sooel Son and Vitaly Shmatikov. The Postman Always Rings Twice: Attacking and Defending postMessage in HTML5 Websites. Network and Distributed System Security Symposium (NDSS), 2013. ↩︎

2. Sebastian Lekies, Martin Johns, and Walter Tighzert. The State of the Cross-Domain Nation. Web 2.0 Security and Privacy (W2SP), 2011. ↩︎