فيتاليك: ما هو مفتاح المرحلة التالية من إيثيريوم؟

المؤلف: فيتاليك بوتيرين

ترجمة: جياهوا، تشين كاتشر

شكر خاص لكل من يويتشي هيراي، وجاستن دريك، ونديم كوبيسي، وأليكس هيكس على ملاحظاتهم ومراجعاتهم.

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

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

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

ما هو التحقق الرسمي؟

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

1 1 2 3 5 8 13 21 34 55 89 144 233 377 610 987 1597 2584 …

إحدى الطرق البسيطة لإثبات ذلك هي من خلال الاستقراء الرياضي، بالتقدم ثلاث خطوات في كل مرة.

أولاً، الحالة الأساسية. لنفترض أن F1 = F2 = 1، F3 = 2. بالملاحظة، نرى أن العبارة ("F1 زوجي عندما يكون i من مضاعفات 3، وإلا فهو فردي") صحيحة قبل x = 3.

ثم ننتقل إلى الحالة الاستقرائية. لنفترض أن العبارة صحيحة قبل 3k+3، أي أننا نعلم مسبقًا أن زوجية F3k+1 وF3k+2 وF3k+3 هي فردي، فردي، وزوجي على التوالي. يمكننا حساب زوجية المجموعة التالية المكونة من ثلاثة أعداد:

F3k+4 = F3k+2 + F3k+3 = فردي + زوجي = فردي

F3k+5 = F3k+3 + F3k+4 = زوجي + فردي = فردي

F3k+6 = F3k+4 + F3k+5 = فردي + فردي = زوجي

وبالتالي، من خلال معرفة أن العبارة صحيحة قبل 3k+3، نستنتج أنها صحيحة قبل 3k+6. ويمكننا تطبيق هذا المنطق مرارًا وتكرارًا، مما يؤكد لنا أن هذه القاعدة تنطبق على جميع الأعداد الصحيحة.

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

إليكم طريقة عرضها:

-- فيبوناتشي مع fib 0 = 0، fib 1 = 1، fib 2 = 1 (المؤشرات مزاحة بمقدار 1)

تعريف فيبوناتشي: طبيعي → طبيعي

| 0 => 0

| 1 => 1

| ن + ٢ => فيبوناتشي (ن + ١) + فيبوناتشي ن

-- الادعاء: fib (3k+1) فردي، fib (3k+2) فردي، fib (3k+3) زوجي.

-- بمعنى آخر: كل عدد ثالث من أعداد فيبوناتشي بدءًا من fib 3 يكون زوجيًا.

نبرهن على الحالات الثلاث جميعها دفعة واحدة بالاستقراء على k، لأن كل حالة

-- يتم بناء الكتلة التالية من الكتلة السابقة.

نظرية fib_triple (k : Nat) :

fib (3 * k + 1) % 2 = 1 ∧

fib (3 * k + 2) % 2 = 1 ∧

fib (3 * k + 3) % 2 = 0 := by

الحث k مع

| صفر => قرر

| succ k ih =>

-- أعد كتابة المؤشرات الجديدة على شكل (شيء ما) + 2 بحيث يتم فك فيبوناتشي.

تحسين ⟨?_, ?_, ?_⟩

· show (fib (3 * k + 3) + fib (3 * k + 2)) % 2 = 1

أوميغا

· show (fib (3 * k + 3) + fib (3 * k + 2) + fib (3 * k + 3)) % 2 = 1

أوميغا

· عرض (fib (3 * k + 3) + fib (3 * k + 2) + fib (3 * k + 3)

+ (فيب (3 * ك + 3) + فيب (3 * ك + 2))) % 2 = 0

أوميغا

هذا هو نفس منطق الاستدلال، ولكن مُعبَّر عنه بلغة Lean. Lean هي لغة برمجة شائعة الاستخدام لكتابة البراهين الرياضية والتحقق منها.

يبدو هذا مختلفًا عن البرهان "البشري" المذكور أعلاه لسبب وجيه: ما هو بديهي بالنسبة للكمبيوتر (بالمعنى التقليدي لكلمة "كمبيوتر"، أي برنامج "حتمي" يتكون من عبارات if/then، بدلاً من نماذج لغوية كبيرة) يختلف اختلافًا جوهريًا عما هو بديهي بالنسبة للبشر.

في البرهان أعلاه، لم تؤكد على حقيقة أن fib(3k+4) = fib(3k+3) + fib(3k+2)، بل أكدت على أن fib(3k+3) + fib(3k+2) عدد فردي، في حين أن استراتيجية في Lean تسمى omega تجمع هذا تلقائيًا مع معرفتها بتعريف fib(3k+4).

في البراهين الأكثر تعقيدًا، عليك أحيانًا أن تذكر صراحة القانون الرياضي الذي يسمح لك باتخاذ الخطوة الحالية، وأحيانًا عليك استخدام أسماء غامضة مثل Prod.mk.inj.

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

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

عندما تبدأ البراهين الرياضية في حماية الشفرة

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

ربما نستطيع حتى معرفة ما إذا كانت آراء شينيتشي موتشيزوكي حول فرضية ABC صحيحة!

لكن بغض النظر عن الفضول، فماذا في ذلك؟

هناك العديد من الإجابات المحتملة. لكن إحدى الإجابات التي تُعدّ بالغة الأهمية بالنسبة لي هي التحقق من صحة برامج الحاسوب، وخاصة تلك التي تؤدي مهام التشفير أو المهام المتعلقة بالأمان.

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

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

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

اتضح أن هناك بالفعل فريقًا يحاول حل هذه المشكلة تحديدًا! إحدى نظرياتهم الأمنية تبدو كالتالي:

نظرية السرية السلبية

(g : G)

(adv : PassiveAdversary G SK) :

ميزة السرية السلبية (F := F) g adv ≤

ProbComp.boolDistAdvantage

(DiffieHellman.ddhExpReal (F := F) g (ddhReduction adv))

(DiffieHellman.ddhExpRand (F := F) g (ddhReduction adv))

فيما يلي ملخص لمعناها من Leanstral:

تُعدّ نظرية دورة السرية السلبية لبروتوكول DDH اختزالًا مُختصرًا يُبيّن أن سرية الرسائل السلبية في بروتوكول X3DH لا تقلّ صعوبةً عن فرضية DDH في نموذج أوراكل العشوائي. فإذا استطاع المُهاجم اختراق سرية الرسائل السلبية في بروتوكول X3DH، فإنه يستطيع أيضًا اختراق بروتوكول DDH.

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

إذا قمت بدمج هذا مع دليل صحيح على تنفيذ تشفير AES، فستحصل على دليل على أن تشفير بروتوكول Signal آمن ضد المهاجمين السلبيين.

وقد أثبتت مشاريع مماثلة أيضاً أن تطبيقات بروتوكول أمان طبقة النقل (TLS) وأجزاء أخرى من التشفير الداخلي للمتصفح آمنة.

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

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

والآن، هناك بعض المحاذير المهمة التي يجب مراعاتها، خاصة فيما يتعلق بالمعنى الحقيقي لكلمة "آمن" ذات الأهمية البالغة.

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

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

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

التحقق الرسمي مصمم خصيصاً للأمان

الأخطاء البرمجية في برامج الكمبيوتر مرعبة.

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

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

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

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

بعض الاقتباسات:

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

و:

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

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

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

بالنسبة للأمن السيبراني، سيكون هذا مستقبلاً قاتماً. وخاصة بالنسبة لنا نحن المهتمين بلامركزية الإنترنت وحريته، فهذه نظرة متشائمة للغاية.

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

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

أنا لا أوافق؛ لدي رؤية أكثر تفاؤلاً لمستقبل الأمن السيبراني.

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

تتفق موزيلا مع وجهة نظري. إليكم ما قالوه:

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

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

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

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

على ماذا يعتمد ذلك؟ بشكل أساسي، على هذا الرسم البياني:

اتجاه ثغرات CVE بمرور الوقت

على مدى عقود، ساهمت العديد من التقنيات في انخفاض عدد الثغرات الأمنية:

أنظمة الكتابة

لغات آمنة للذاكرة

تحسينات في بنية البرمجيات (بما في ذلك الحماية المعزولة، والتحكم في الأذونات، والتمييز بشكل أوسع بين "قاعدة الحوسبة الموثوقة" و"البرامج الأخرى").

أساليب اختبار أفضل

قاعدة معرفية متنامية باستمرار حول أنماط البرمجة الآمنة وغير الآمنة

عدد متزايد من مكتبات البرامج المكتوبة مسبقًا والمدققة

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

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

برنامج STARK معقد للغاية. لكن خصائص الأمان الأساسية التي يطبقها سهلة الفهم والتحديد: إذا رأيت رمز تجزئة H يشير إلى البرنامج P، والمدخل x، والمخرج y، فإما (i) أن خوارزمية التجزئة المستخدمة في STARK قد تم اختراقها، أو (ii) أن P(x) = y.

وهكذا لدينا مشروع Arklib، الذي يحاول إنشاء تطبيق STARK تم التحقق منه رسميًا بالكامل (انظر VCV-io، الذي يوفر البنية التحتية الأساسية للحوسبة أوراكل للتحقق الرسمي من العديد من بروتوكولات التشفير الأخرى، والتي يعتبر الكثير منها من تبعيات STARK).

وبشكل أكثر طموحًا، هناك مشروع evm-asm: وهو مشروع لبناء تطبيق EVM كامل تم التحقق منه رسميًا بالكامل.

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

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

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

وثمة مجالان مهمان آخران هما:

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

لغات برمجة العقود الذكية: انظر التحقق الرسمي في Vyper و Verity.

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

بالنسبة للبشر، يُعدّ التفكير في النظام بأكمله من البداية إلى النهاية أمراً بالغ الصعوبة. لكن أنظمة التحقق الآلي من القواعد قادرة على القيام بذلك.

التحقق الرسمي مصمم لتحقيق الكفاءة

دعونا نلقي نظرة أخرى على evm-asm. هذا تطبيق لآلة EVM. ولكنه تطبيق لآلة EVM مكتوب مباشرة بلغة التجميع RISC-V.

أصيل.

إليك رمز عملية الإضافة (ADD opcode):

استيراد EvmAsm.Rv64.Program

مساحة الاسم EvmAsm.Evm64

افتح EvmAsm.Rv64

/-- عملية جمع EVM ذات 256 بت: ثنائية، تسحب 2، وتدفع 1.

الطرف 0: LD، LD، ADD، SLTU (حمل)، SD (5 تعليمات).

الأطراف 1-3: LD، LD، ADD، SLTU (حمل 1)، ADD (حمل للداخل)، SLTU (حمل 2)، OR (حمل للخارج)، SD (8 لكل منها).

ثم ADDI sp, sp, 32.

السجلات: x12=sp، x7=acc، x6=operand، x5=carry، x11=carry1. -/

def evm_add : Program :=

-- الطرف 0 (5 تعليمات)

LD .x7 .x12 0 ;; LD .x6 .x12 32 ;;

أضف .x7 .x7 .x6 ;; SLTU .x5 .x7 .x6 ;; SD .x12 .x7 32 ;;

-- الطرف 1 (8 تعليمات)

LD .x7 .x12 8 ;; LD .x6 .x12 40 ;;

أضف .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;

أضف .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;

أو .x5 .x11 .x6 ;; SD .x12 .x7 40 ;;

-- الطرف 2 (8 تعليمات)

LD .x7 .x12 16 ;; LD .x6 .x12 48 ;;

أضف .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;

أضف .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;

أو .x5 .x11 .x6 ;; SD .x12 .x7 48 ;;

-- الطرف الثالث (8 تعليمات)

LD .x7 .x12 24 ;; LD .x6 .x12 56 ;;

أضف .x7 .x7 .x6 ;; SLTU .x11 .x7 .x6 ;;

أضف .x7 .x7 .x5 ;; SLTU .x6 .x7 .x5 ;;

أو .x5 .x11 .x6 ;; SD .x12 .x7 56 ;;

ضبط السرعة

ADDI .x12 .x12 32

نهاية EvmAsm.Evm64

يُعزى اختيار معمارية RISC-V إلى أن مُثبتات ZK-EVM التي يتم بناؤها عادةً ما تعمل عن طريق إثبات معمارية RISC-V وتجميع عملاء إيثيريوم إلى معمارية RISC-V. لذا، إذا كان لديك تطبيق EVM مكتوب مباشرةً بمعمارية RISC-V، فسيكون هذا هو أسرع تطبيق يمكنك الحصول عليه.

يمكن أيضًا محاكاة RISC-V بكفاءة عالية على أجهزة الكمبيوتر العادية (وهناك أجهزة كمبيوتر محمولة RISC-V متوفرة في السوق).

بالطبع، لتحقيق التكامل التام، يجب عليك التحقق رسميًا من تنفيذ RISC-V نفسه (أو حسابات المُثبت)، ولكن لا تقلق، فالعمل في هذا المجال موجود بالفعل.

كتابة التعليمات البرمجية مباشرةً بلغة التجميع أمرٌ اعتدنا القيام به قبل خمسين عاماً. ومنذ ذلك الحين، تخلينا عن هذه الممارسة لصالح كتابة التعليمات البرمجية بلغات عالية المستوى.

تُضحي اللغات عالية المستوى بالكفاءة، ولكن في المقابل، تسمح ببرمجة أسرع بكثير، والأهم من ذلك، فهم أسرع بكثير لبرامج الآخرين، وهو أمر ضروري للأمان.

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

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

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

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

يمكن للمستخدمين التحقق من هذا الدليل (تلقائيًا) مرة واحدة، ومن ثم، ما عليهم سوى تشغيل النسخة السريعة.

هذا النهج قوي بشكل لا يصدق، وهناك سبب يجعل يويتشي هيراي يسميه "الشكل الأمثل لتطوير البرمجيات".

التحقق الرسمي ليس حلاً سحرياً

في مجالات التشفير وعلوم الحاسوب، هناك تقليد قديم قدم تاريخ الأساليب الرسمية نفسها تقريبًا: وهو تقليد انتقاد الأساليب الرسمية (أو بشكل أوسع، الاعتماد على "البراهين").

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

في عام 1979، اقترح رابين دالة تشفيرية "يمكن إثباتها" آمنة بمعنى ما، مما يعني أنها تتمتع بخاصية أمنية اختزالية.

يشير بيان الأمان الاختزالي إلى أن أي شخص يمكنه العثور على الرسالة m من النص المشفر y يجب أن يكون قادرًا أيضًا على تحليل n. ... بعد فترة وجيزة من اقتراح رابين لنظام التشفير الخاص به، أشار ريفست إلى أنه من المفارقات أن هذه الميزة بالذات التي تمنحه أمانًا إضافيًا ستؤدي إلى انهيار كامل في حالة مواجهة مهاجم يُعرف باسم "النص المشفر المختار".

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

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

والآن، لنعد إلى البراهين والبرمجيات القابلة للتحقق الآلي. إليكم ورقة بحثية من عام ٢٠١١ كشفت عن ثغرات أمنية في مُصرّف لغة C تم التحقق منه رسميًا: paper:

تتجلى مشكلة CompCert الثانية التي وجدناها في خطأين يؤديان إلى توليد الكود التالي: stwu r1, -44432(r1) حيث يتم تخصيص إطار مكدس PowerPC كبير.

تكمن المشكلة في أن حقل الإزاحة ذي الـ 16 بت قد تجاوز الحد المسموح به. لم تحدد دلالات CompCert الخاصة بمعالجات PPC حدًا لعرض هذه القيمة المباشرة؛ فقد افترضت أن المُجمِّع سيكتشف القيم الخارجة عن النطاق.

وهناك أيضاً ورقة بحثية صدرت عام 2022:

في CompCert-KVX، أصلح التعديل e2618b31 خطأً برمجيًا: حيث كانت تعليمة "nand" تُطبع على شكل "and"؛ إذ لم تُستخدم "nand" إلا في النمط النادر ~ (a & b). وقد اكتُشف هذا الخطأ أثناء تجميع برامج مُولّدة عشوائيًا.

واليوم، في عام 2026، إليكم كيف يصف نديم كوبيسي الثغرات الأمنية في البرامج التي تم التحقق منها رسميًا في Cryspen:

في نوفمبر 2025، أفاد فيليبو فالسوردا بشكل مستقل أن libcrux-ml-dsa v0.0.3 أنتجت مفاتيح عامة وتوقيعات مختلفة على منصات مختلفة بالنظر إلى نفس المدخلات الحتمية.

كان الخلل موجودًا في دالة التغليف الداخلية vxarqu64، التي نفذت عملية XAR المستخدمة في تبديل Keccak-f لخوارزمية SHA-3. وقد مررت آلية التراجع معلمات غير صحيحة إلى عملية الإزاحة، مما أدى إلى تلف ملخص SHA-3 على منصات ARM64 التي لا تدعم خوارزمية SHA-3 على مستوى الأجهزة.

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

و:

تُطبّق مكتبة libcrux-psq بروتوكول المفتاح المشترك المُسبق لما بعد الحوسبة الكمومية. في دالة decrypt_out، يستدعي مسار فك تشفير AES-GCM 128 الدالة .unwrap() على نتيجة فك التشفير بدلاً من نشر الأخطاء. قد يؤدي وجود نص مشفر غير صالح إلى تعطل العملية.

تندرج جميع هذه القضايا الأربع ضمن إحدى الفئتين التاليتين:

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

الحالات التي نسي فيها المؤلفون تحديد الخصائص الرئيسية التي كان من الضروري إثباتها.

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

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

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

هذه مقالة حول "تحليل القدرة التفاضلية"، وهو مثال مفهوم جيدًا على هذه التقنيات: مقالة.

يُعد تحليل القدرة التفاضلية نوعًا شائعًا من هجمات القنوات الجانبية. المصدر: ويكيبيديا

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

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

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

تقدم هذه المقالة تصنيفات لأشكال أخرى من التسرب.

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

بالنظر إلى الصورة الكلية، هناك خيط رئيسي هنا. التحقق الرسمي قوي.

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

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

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

في كلتا الحالتين، تتلخص الصحة والأمان في مقارنة بين الكائنات الرياضية والنوايا أو التوقعات البشرية.

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

لكنها كائنات رياضية معقدة للغاية لا يمكن لأجهزة الكمبيوتر ولا لنا أنفسنا فهمها أو حتى قراءتها.

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

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

لذا، فإنّ "الصحة القابلة للإثبات" و"الأمان القابل للإثبات" لا يثبتان في الواقع "الصحة" و"الأمان" كما نفهمهما نحن البشر. لا شيء يُمكنه فعل ذلك ما لم نتمكن من محاكاة الدماغ البشري بشكل كامل.

إذن، ما هي فائدته؟

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

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

خذ هذا الكود المكتوب بلغة بايثون كمثال:

دالة fib(n: int) -> int:

إذا كان n < 0:

رفع استثناء ("القيم السالبة غير مدعومة")

elif 0 <= n < 2:

إرجاع n

آخر:

أعد fib(n-1) + fib(n-2)

if __name__ == '__main__':

assert [fib(i) for i in range(10)] == [0, 1, 1, 2, 3, 5, 8, 13, 21, 34]

تحقق من أن fib(15) == 610

هنا، يمكنك التعبير عن نواياك بثلاث طرق مختلفة:

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

ضمنيًا، من خلال نظام النوع (الذي يحدد أن المدخلات والمخرجات والخطوات الوسيطة في الاستدعاء الذاتي كلها أعداد صحيحة)

من خلال طريقة "حزمة العينات": حالات الاختبار

سيؤدي تشغيل الملف إلى التحقق من صحة الصيغة ومقارنتها بالعينات. يمكن لمدقق الأنواع التحقق من توافق الأنواع: فجمع عددين صحيحين عملية متوافقة وستنتج عددًا صحيحًا آخر.

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

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

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

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

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

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

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

كيف أبدأ؟

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

/-- مساعد: نقطة ≤ عند مستوى الطي مع مُجمِّع. -/

نظرية خاصة foldl_acc_le (ds1 ds2 : List Nat) (w : Nat) (ab : Nat) (hAcc : a ≤ b)

(hLE : Forall₂ (· ≥ ·) ds1 ds2) :

List.foldl (λ acc d => acc * w + d) a ds1 ≤

List.foldl (λ acc d => acc * w + d) b ds2 := by

قم بمطابقة ds1 و ds2 و hLE مع

| [], [], .nil => دقة hAcc

| d1::ds1', d2::ds2', .cons hd htl =>

simp [List.foldl]

تحسين foldl_acc_le ds1' ds2' w (a * w + d1) (b * w + d2) ?_ htl

بالضبط Nat.add_le_add (Nat.mul_le_mul hAcc (Nat.le_refl _)) HD

(إذا كنت تتساءل، فهذه واحدة من العديد من المعضلات الفرعية في إثبات بيان أمني محدد لنوع مختلف من توقيعات SPHINCS).

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

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

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

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

الشيء الوحيد الذي عليك التحقق منه في النهاية هو ما إذا كانت البيانات التي تم إثباتها تلبي متطلباتك.

في حالة متغير توقيع SPHINCS، هذا هو البيان النهائي:

نظرية wots_fullDigits_incomparable

{dig1 dig2 : List Nat} {w l1 l2 : Nat}

(hw : 0 < w)

(hLen1 : dig1.length = l1) (hLen2 : dig2.length = l1)

(hBound1 : ∀ d ∈ dig1, d < w) (hBound2 : ∀ d ∈ dig2, d < w)

(hL2suff : l1 * (w - 1) < w ^ l2)

(hNeq : dig1 ≠ dig2) :

¬ لكل ٢ (· ≤ ·) (wotsFullDigits dig1 w l1 l2) (wotsFullDigits dig2 w l1 l2) ∧

¬ Forall₂ (· ≤ ·) (wotsFullDigits dig2 w l1 l2) (wotsFullDigits dig1 w l1 l2)

هذا في الواقع على وشك أن يكون بالكاد قابلاً للقراءة:

إذا كانت الأرقام الناتجة عن تجزئة واحدة (dig1) لا تساوي تلك الناتجة عن تجزئة أخرى (dig2).

إذن، لا يتحقق أي من الشرطين التاليين:

بالنسبة لجميع الأرقام، فإن الأرقام من dig1 ≤ الأرقام من dig2

بالنسبة لجميع الأرقام، فإن الأرقام من dig2 ≤ الأرقام من dig1

في "الأرقام الموسعة" (wotsFullDigits) الناتجة عن جمع مجاميع التحقق. أي أنه في امتداد الرقم 1، ستكون هناك حتماً أماكن تكون فيها الأرقام أعلى، بينما في أماكن أخرى، ستكون الأرقام في امتداد الرقم 2 أعلى.

فيما يتعلق باستخدام نماذج اللغة الكبيرة لكتابة البراهين، أجد أن كلاً من Claude و Deepseek 4 Pro مناسبان. أما Leanstral فهو نموذج أوزان مفتوح المصدر أصغر حجماً، تم ضبطه خصيصاً لكتابة Lean، وهو بديل واعد.

يحتوي على 119 مليار مُعامل، ويُفعّل 6 مليارات لكل رمز مميز، ويمكنك تشغيله محليًا، على الرغم من أنه أبطأ (حوالي 15 رمزًا مميزًا/ثانية على حاسوبي المحمول). وفقًا للاختبارات المعيارية، يتفوق Leanstral على نماذج عامة أكبر بكثير.

بناءً على تجربتي الشخصية الحالية، فهو أقل فعالية قليلاً من برنامج Deepseek 4 Pro ولكنه لا يزال فعالاً للغاية.

لا يمكن للتحقق الرسمي أن يحل جميع مشاكلنا.

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

لقد ساهم التحقق الرسمي المدعوم بالذكاء الاصطناعي في تحقيق خطوة قوية نحو تحقيق هذا الهدف.

ومثل تقنية البلوك تشين وتقنية ZK-SNARKs، فإن الذكاء الاصطناعي والتحقق الرسمي هما أيضاً تقنيات متكاملة للغاية.

تمنحك تقنية البلوك تشين إمكانية التحقق المفتوح ومقاومة الرقابة على حساب الخصوصية وقابلية التوسع، بينما تعيد لك تقنية ZK-SNARKs الخصوصية وقابلية التوسع (في الواقع، أكثر مما كان لديك من قبل).

يمنحك الذكاء الاصطناعي القدرة على كتابة كميات هائلة من التعليمات البرمجية على حساب الدقة، بينما يعيد لك التحقق الرسمي الدقة (في الواقع، أكثر مما كان لديك من قبل).

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

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

لكن هنا، يتمتع الأمن السيبراني بمستقبل متفائل: سيستمر البرنامج في الانقسام إلى "أجزاء طرفية غير آمنة" حول "نواة آمنة".

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

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

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

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

ستصبح نواة نظام التشغيل (أو جزء منها على الأقل) بمثابة نواة آمنة.

ستكون إيثيريوم مثالاً آخر.

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

ستكون الأنظمة المتعلقة بإنترنت الأشياء هي الرابعة.

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

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