💻 computer science

Cargo Sherlock: An SMT-Based Checker for Software Trust Costs

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

المؤلفون الأصليون: Muhammad Hassnain, Anirudh Basu, Ethan Ng, Caleb Stanford

نُشر 2026-02-04

📖 4 دقيقة قراءة☕ قراءة في استراحة قهوة

CC BY 4.0

المؤلفون الأصليون: Muhammad Hassnain, Anirudh Basu, Ethan Ng, Caleb Stanford

البحث الأصلي مرخَّص بموجب CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ هذا شرح مولَّده بالذكاء الاصطناعي للبحث أدناه. لم يكتبه المؤلفون ولم يصادقوا عليه. وللتحقق من الدقة التقنية، يرجى الرجوع إلى البحث الأصلي. اقرأ إخلاء المسؤولية الكامل

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

يقدم البحث أداة تسمى Cargo Sherlock تساعدك في تحديد ما إذا كانت هذه "اللبنات" آمنة قبل استخدامها. بدلاً من مجرد التخمين، تعمل الأداة كـ "محقق" منظم للغاية يقوم بحساب "تكلفة الثقة" (Trust Cost) لكل قطعة برمجية تريد استخدامها.

إليك كيف تعمل، مقسمة إلى مفاهيم بسيية:

1. تشبيه "تكلفة الثقة"

فكر في الوثوق بقطعة برمجية مثل الحصول على قرض.

تكلفة ثقة منخفضة: أنت تثق في البرمجيات بسهولة. ربما لأنها من بناء مشهور (مؤلف معروف)، أو تم فحصها من قبل مفتش معتمد (تدقيق/Audit). أنت مستعد لـ "دفع" تكلفة منخفضة لتصدق أنها آمنة.
تكلفة ثقة مرتفعة: عليك أن تبذل جهداً كبيراً لتتخيل أنها آمنة. ربم يكون المؤلف غريباً، أو لم يتم تدقيق البرمجية أبداً، أو لديها عدد قليل جداً من التنزيلات. لكي تصدق أنها آمنة، عليك القيام بـ "قفزة إيمان" كبيرة. هذه "القفزة" تكلف الكثير.

مهمة Cargo Sherlock هي إيجاد أرخص طريقة لإقناع نفسك بأن قطعة برمجية ما آمنة. إذا كانت أرخص طريقة لتصديق أنها آمنة لا تزال تكلف ثروة (رقماً عالياً)، فإن الأداة تخبرك: "مهلاً، هذا أمر خطير. لا تستخدمه".

2. كيف يحل المحقق اللغز

تستخدم الأداة محرك منطق رياضي (يسمى SMT) لحل لغز. تخيل أن لديك قائمة من الأدلة (الافتراضات) التي يمكنك استخدامها لإثبات أن المكتبة آمنة:

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

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

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

3. "العامل البشري"

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

هي تتيح لك وضع القواعد. يمكنك القول: "أنا أثق في عمليات التدقيق من الشركة (س) أكثر من الشركة (ص)"، أو "أنا لا أثق في الكود الذي يحتوي على الكثير من التنزيلات لأنها قد تكون مزارع بوتات (Bot Farms)".
هي تجعل هذه المشاعر البشرية قابلة للتدقيق. بدلاً من "صندوق أسود" يقول "مستوى الثقة: 85%"، تقول الأداة: "نحن نثق في هذا لأنه اجتاز تدقيقاً من جوجل (التكلفة: 5) ولديه الكثير من التنزيلات (التكلفة: 10)".

4. ما وجدته الأداة (النتائج)

اختبر المؤلفون Cargo Sherlock في سيناريوهات حقيقية وزائفة:

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

5. السرعة والنطاق

تمتلك الأداة طريقتين لحل اللغز:

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

الملخص

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

ملاحظة: يذكر البحث صراحة أن هذه الأداة مخصصة لنظام لغة البرمجة Rust (المكتبات التي تسمى crates).

ملخص تقني: Cargo Sherlock

بيان المشكلة

تشكل هجمات سلاسل التوريد البرمجية، مثل حادثة SolarWinds، وثغرة XZ Utils، والمكتبات الخبيثة في لغة Rust مثل rustdecimal و faster_log تهديدات كبيرة للأنظمة البيئية مفتوحة المصدر. تندرج طرق الكشف الحالية ضمن فئتين:

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

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

المنهجية

يقترح البحث أداة Cargo Sherlock لقياس الثقة في سلاسل توريد مكتبات Rust (التي تسمى crates) باستخدام نظرية النماذج الملبيّة (Satisfiability Modulo Theories - SMT). يعتمد النهج على مشكلة الحد الأدنى من الثقة (Minimum Trust Problem).

مشكلة الحد الأدنى من الثقة

صاغ المؤلفون الثقة كمسألة تحسين منطقية:

المدخلات: مجموعة من الافتراضات المرشحة ( $\Gamma$ ) حول تبعية برمجية ما (على سبيل المثال: "إذا كان للـ crate عدد كبير من التنزيلات، فهو آمن")، واستنتاج ( $c$ ، مثل: "الـ crate آمن")، ودالة تكلفة ( $C$ ) تخصص تكلفة لكل افتراض.
الهدف: إيجاد مجموعة فرعية من الافتراضات $\Delta \subseteq \Gamma$ بحيث تستلزم $\Delta$ منطقياً الاستنتاج $c$ ( $\Delta \models c$ )، مع تقليل مجموع التكاليف في $\Delta$ .
التفسير: تشير "تكلفة الثقة" الأقل إلى حجة أقوى وأكثر تبريراً للسلامة بناءً على افتراضات المستخدم. وتشير التكاليف الأعلى إلى وجود كود أكثر خطورة يتطلب "إيماناً" أكبر للوثوق به.

الخوارزميات

تم اقتراح خوارزميتين لحل مشكلة الحد الأدنى من الثقة:

الخوارزمية الساذجة (الخوارزمية 1): تقوم بتشفير المشكلة باستخدام المكمّمات (Quantifiers) على المتغيرات القضائية والحساب الصحي الخطي. وهي تبني صيغة تمثل شجرة التبعيات بشكل متكرر وتستخدم مُحلل SMT لإيجاد الحد الأدنى من التكلفة. هذا النهج صحيح ولكنه مكلف حاسوبياً بسبب المكمّمات المتداخلة.
خوارزمية جمل هورن (الخوارزمية 2): تقيد الافتراضات لتكون جمل هورن محددة غير حلقية (Acyclic definite Horn clauses). وتستخدم إجراء فك (Unfolding) (مشابه لـ SLD resolution) لتحويل المشكلة إلى صيغة بالشكل الطبيعي المشتت (Disjunctive Normal Form - DNF). ثم تستخدم البحث الثنائي عبر مساحة التكلفة باستخدام استعلامات SMT خالية من المكمّمات. وبينما يمكن أن تكون الصيغة المولدة أسية في أسوأ الحالات، إلا أن هذا النهج أكثر كفاءة بشكل ملحوظ في الممارسة العملية.

التعقيد: ثبت أن مشكلة الحد الأدنى من الثقة العامة هي من فئة $\Sigma^P_2$ -hard. أما تقييدها بجمل هورن (HORN-MINTRUST) فقد ثبت أنه NP-complete، مما يبرر استخدام مُحللات SMT.

التنفيذ والتصميم

Cargo Sherlock هي أداة تعتمد على لغة Python وتتكامل مع:

جمع البيانات: تجمع البيانات الوصفية من crates.io (التنزيلات، النجوم، المؤلفون)، وGitHub، وRustSec (الثغرات الأمنية)، وCargo Vet (تقارير التدقيق)، وأدوات التحليل الساكن (Miri، Cargo Scan).
النموذج العلاقي: ينظم البيانات في كيانات (Crates، المؤلفون، عمليات التدقيق، التبعيات، نتائج الأدوات).
أنواع الافتراضات:
- الإيجابية: مبررات السلامة (مثل: مؤلف موثوق، اجتاز التدقيق، لا توجد آثار جانبية).
- السلبية: مبررات عدم الثقة (مثل: الوجود في RustSec، تم رصده بواسطة Miri).
- المعلمية (Parameterized): تكاليف تتغير باستمرار بناءً على البيانات الوصفية (مثل: عدد التنزيلات).
المخرجات: تحسب تكلفة الثقة (Trust Cost) وتكلفة عدم الثقة (Distrust Cost) (على مقياس 0–100). ويتم دمجهما لإنتاج تسمية شدة (آمن، شدة منخفضة/متوسطة/عالية، حرجة).

المساهمات الرئيسية

النموذج الشكلي: صياغة رسمية لمشكلة الثقة في سلسلة التوريد كمسألة حد أدنى من الثقة قابلة للحل عبر SMT، مما يحقق متطلبات التحديد، والقدرة على التدقيق، والقابلية للضبط، والتركيب.
الخوارزميات: خوارزميتان لحل المشكلة، بما في ذلك النهج المحسن القائم على جمل هورن الذي يتعامل مع أشجار التبعيات الكبيرة بشكل أكثر فعالية من الطريقة الساذجة القائمة على المكمّمات.
تنفيذ الأداة: نموذج أولي يعمل لـ Cargo Sherlock مخصص لـ Rust، يدمج البيانات الوصفية الحقيقية ونتائج تحليل البرامج لحساب تكاليف الثقة.
التقييم: دراسة تجريبية توضح قدرة الأداة على اكتشاف هجمات سلاسل التوريد الاصطناعية والواقعية.

نتائج التقييم

قيم المؤلفون Cargo Sherlock بناءً على أربعة أسئلة بحثية:

RQ1 (Typosquatting الاصطناعي): عند الاختبار على متغيرات Typosquatting اصطناعية لأفضل 100 crate في Rust، سجلت الأداة تكاليف ثقة وسمات شدة أعلى بكثير (غالباً "حرجة") مقارنة بالـ crates الأصلية الآمنة. تم تصنيف معظم الـ crates الأصلية على أنها "آمنة"، بينما تم وسم الـ typosquats بأنها خطرة بسبب انخفاض عدد التنزيلات والمؤلفين غير الموثوقين.
RQ2 (الحوادث الواقعية):
- faster_log: نسخة typosquat خبيثة من fast_log. أعطت Cargo Sherlock تسمية "حرجة" (ثقة: 75، عدم ثقة: 80) مقارنة بالأصل الذي حصل على "شدة متوسطة" (ثقة: 37، عدم ثقة: 73)، مدفوعة بالمؤلف غير الموثوق والآثار الجانبية.
- serde_yml: نسخة مستضافة من قِبل ذكاء اصطناعي (AI-maintained fork) لـ serde_yaml. أعطت الأداة تسمية "شدة منخفضة" للنسخة (مقابل "آمن" للأصل)، ويرجع ذلك أساساً لتغيير المؤلفية، رغم تشابه تكاليف عدم الثقة.
RQ3 (الثغرات المعروفة): عند الاختبار ضد 592 crate مدرجة في قاعدة بيانات RustSec (مع تعطيل الافتراضات الخاصة بـ RustSec)، تم تصنيف العديد منها كـ "آمنة" أو "شدة منخفضة". يشير هذا إلى أن الشعبية (عدد التنزيلات العالي) يمكن أن تخفي الثغرات المعروفة في نموذج الثقة، مما يوحي بأن المستخدمين قد يعتبرون الـ crates المصابة بثغرات آمنة إذا اعتمدوا فقط على مقاييس الشعبية.
RQ4 (القابلية للتوسع):
- الخوارزمية 1: فشلت في التوسع، حيث انتهى وقت التنفيذ أو تعطلت عند التعامل مع crates تحتوي على أكثر من ~10 تبعيات.
- الخوارزمية 2: نجحت في تقييم crates تصل تبعياتها إلى 150 خلال نافذة زمنية قدرها 10 دقائق، مما أظهر قابلية توسع عملية لمعظم السيناريوهات الواقعية.

الأهمية والادعاءات

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

التحديد (Specificity): على عكس نهج التعلم الآلي "الصندوق الأسود"، تنتج Cargo Sherlock مجموعة محددة من الافتراضات (مثل: "موثوق من قبل أليس"، "تنزيلات عالية") التي تبرر تكلفة الثقة، مما يجعل المنطق قابلاً للتدقيق.
القابلية للضبط (Configurability): يمكن للمستخدمين تعديل تكاليف الافتراضات (مثل: معاقبة الكود الذي يديره الذكاء الاصطناعي أو مكافأة مدققين محددين) لتتماشى مع مستوى تحملهم للمخاطر.
القابلية للتركيب (Composability): يسمح النموذج بتركيب تكاليف الثقة عبر أشجار التبعيات، مما يتيح رؤية شاملة لمخاطر سلسلة التوريد.

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