checkedc
Version 1.0 of the Checked C specification
تمدد C تمتد C مع حدود فحص وتحسين سلامة النوع. يساعد المبرمجين على تعديل رمز C الحالي ليكون أكثر أمانًا. يحتوي هذا الريبو على مواصفات C التي تم فحصها ، رمز العينة ، ورمز الاختبار.
مؤشرات سمين لسلامة الذاكرة الزمنية لـ C بواسطة Jie Zhou و John Criswell و Michael Hicks. ظهر هذا في OOPSLA 2023. يصف امتدادًا لفحص C الذي يضيف مؤشرات جديدة توفر سلامة الذاكرة الزمنية.
C لفحص C بواسطة 3C ، من قبل Aravind Machiry ، John Kastner ، Matt McCutchen ، Aaron Eline ، Kyle Headley ، و Michael Hicks. تصف هذه الورقة أداة 3C شبه الآلية لتحويل C إلى فحص C. فازت بجائزة Sigplan الورقية المتميزة في OOPSLA 2022.
نموذج رسمي لفحص C ، بقلم Liyi Li و Deena Postol و Leonida Lampropoulos و David Van Horn و Michael Hicks. تم نشر هذا في نماذج أسس أمان الكمبيوتر 35 IEEE 35th. يصف نموذجًا رسميًا لفحص C. تم إضفاء الطابع الرسمي على النموذج باستخدام PROVER نظرية COQ.
تحقيق السلامة بشكل تدريجي مع Compled C. تم تقديم هذا في مؤتمر مبادئ الأمن والثقة 2019 :. تصف هذه الورقة إصدارًا مبكرًا من 3C يحول رمز C الموجود لاستخدام أنواع PTR. كما أنه يثبت خاصية إلقاء اللوم حول المناطق التي تم فحصها والتي تُظهر أن المناطق التي تم فحصها لا تلوم لأي فساد للذاكرة. يتم إضفاء الطابع الرسمي على هذا الدليل لمجموعة فرعية أساسية من تمديد اللغة.
تم فحص C: جعل C آمنًا بالتمديد من قبل David Tarditi و Samuel Elliott و Andrew Ruef و Michael Hicks. ظهر هذا في مؤتمر تنمية الأمن السيبراني 2018 IEEE 2018. يصف الأفكار الرئيسية لحدود C التي تم فحصها في 8 صفحات. لقد أضفنا ميزات لفحص C منذ ذلك الحين. توفر الويكي والمواصفات أوصافًا محدثة لفحص C.
تم تقديم ملصق في اجتماع LLVM DEV 2019: "تختفي الفائض: تم فحص C لسلامة الذاكرة". يوفر الملصق مقدمة لفحص C ، ويحدد تنفيذ برنامج التحويل البرمجي ويقدم تقييمًا تجريبيًا لفحص C.
كان هناك حديث (شرائح) في اجتماع DEV الظاهري 2020 LLVM: "تم التحقق من C: إضافة دعم سلامة الذاكرة إلى LLVM". يصف الحديث تصميم التعليقات التوضيحية الحدودية للمؤشرات التي تم فحصها ومؤشرات الصفيف وكذلك إطار الفحص الثابت لسلامة الحدود. يصف الحديث أيضًا باختصار خوارزميات جديدة لتوسيع الحدود تلقائيًا للمصفوفات المنتهية الخالية ومقارنة التعبيرات عن التكافؤ.
يسعدنا الحصول على المساعدة. يمكنك المساهمة من خلال تجربة Checked C ، والإبلاغ عن الأخطاء ، وإعطائنا ملاحظات. هناك طرق أخرى للمساهمة أيضًا.
يتم تغطية البرنامج في هذا المستودع بترخيص معهد ماساتشوستس للتكنولوجيا. انظر الملف ترخيص. txt للترخيص. يتم توفير مواصفات Cheded C من قبل Microsoft بموجب اتفاقية المواصفات النهائية لمؤسسة OpenWeb ، الإصدار 1.0. تخضع مساهمات التعليمات البرمجية في LLVM/Clang Repos لشروط ترخيص LLVM/CLANG.
Check C هو مشروع مستقل مفتوح المصدر. بدأ الأمر كمشروع بحث في Microsoft في عام 2015. على غرار Checked C. كنا نبحث عن طريقة لتحسين أمان برامج الأنظمة الحالية والتخلص من فئات الأخطاء.
تتمثل إحدى الطرق في إعادة كتابة البرنامج بلغة أحدث مثل Rust. ومع ذلك ، فإن إعادة كتابة رمز التحديات لعدة أسباب: إنها مكلفة ، وهناك اختلافات خفية في ميزات اللغة الأساسية مثل الحساب عبر اللغات ، وقد يستغرق الأمر وقتًا طويلاً قبل أن يكون لديك نظام عمل. مجتمعة ، وهذا يجعل إعادة كتابة مشروع تطوير البرمجيات عالية الخطورة. من غير المرجح أن يتم القيام بهذه الأنواع من إعادة الكتابة فقط لتحسين الأمن. قررنا اتباع نهج تدريجي يسمح بتحسين رمز C الحالي تدريجياً وبتكلفة أقل بكثير.
ساهم باحثون من العديد من الجامعات والشركات في فحص الباحثين C. في جامعة ماريلاند ، وجامعة روتشستر ، وجامعة واشنطن ، وجامعة سامسونج ، وجامعة روتجرز ، وجامعة بنسلفانيا ، وقد اقترحت على C. Apple تمديدًا مشابهًا للتحقق من التدقيق الديناميكي.
اعتمد هذا المشروع مدونة قواعد السلوك.
