فراما-سی: تفاوت میان نسخه‌ها
ایجاد شده توسط ترجمهٔ صفحهٔ «Frama-C» |
(بدون تفاوت)
|
نسخهٔ ۱۵ فوریهٔ ۲۰۲۰، ساعت ۰۵:۲۷
 | |
| توسعه‌دهنده(ها) | Commissariat à l'Énergie Atomique (CEA-List) and Inria |
|---|---|
| مخزن | |
| نوشته‌شده با | OCaml |
| سیستم‌عامل | Microsoft Windows, FreeBSD, OpenBSD, Linux, Mac OS X |
| در دسترس به | English |
| نوع | Formal verification, Static code analysis |
| مجوز | mostly LGPL, some parts under BSD licenses |
| وبگاه | frama-c |
Frama-C [۱] مخفف (Framework for Modular Analysis of C programs) یا (چارچوب برای تجزیه و تحلیل مدولار برنامه های C) که جهت تجزیه و تحلیل مدولار برنامه های C است . Frama-C مجموعه ای از آنالایزرهای برنامه قابل تعامل برای برنامه های C است . Frama-C توسط کمیساریای فرانسوی l’Énergie Atomique et aux Énergies Alternatives ( لیست CEA ) [۲] و Inria توسعه یافته است . همچنین از ابتکار عمل زیرساخت های هسته ای بودجه دریافت کرده است. Frama-C ، به عنوان آنالایزر استاتیک ، برنامه ها را بدون اجرای آنها بازرسی می کند. با وجود نام آن ، این نرم افزار مربوط به پروژه فرانسوی Framasoft نیست .
این ابزار برای سیستم عامل های Mac و لینوکس ارائه شده و از طریق ماشین های مجازی همچون VM،Cygwin و یا WIndows Subsystem for Linux در ویندوز نیز قابل استفاده می باشد.
معماری
Frama-C دارای یک معماری پلاگین مدولار [۳] قابل مقایسه با Eclipse (نرم افزار) یا GIMP است .
Frama-C برای تولید یک درخت نحو انتزاعی به CIL ( C Intermediate Language ) متکی است . درخت نحوی انتزاعی از یادداشتهای نوشته شده در زبان خصوصیات ANSI / ISO C ((ACSL پشتیبانی می کند.
چندین ماژول می توانند درخت ترکیبی انتزاعی را برای افزودن حاشیه نویسی (ANSI / ISO C (ACSL زبان اضافه کنند . در میان اغلب استفاده می شود افزونه های عبارتند از:
- تجزیه و تحلیل ارزش – یک مقدار یا مجموعه ای از مقادیر ممکن را برای هر متغیر در یک برنامه محاسبه می کند. این افزونه از تکنیک های تفسیر انتزاعی استفاده می کند و بسیاری از افزونه های دیگر از نتایج آن استفاده می کنند.
- جسی – خواص را به صورت قیاسی تأیید می کند. جسی برای اطمینان از ارسال تعهدات اثبات شده به پیش پرده های قضیه اتوماتیک مانند Z3 ، Simplify ، Alt-Ergo یا قضیه تعاملی مانند Coq یا چرا ، به پشتیبان چرا [۴] یا Why3 تکیه می کند. با استفاده از جسی ، اجرای حباب مرتب سازی یا سیستم رای گیری الکترونیکی اسباب بازی می تواند ثابت شود که مشخصات مربوط به آنها را برآورده می کند. از یک الگوی حافظه جدایی با الهام از منطق جدایی استفاده می کند .
- WP (ضعیف ترین پیش شرط) – مشابه جسی ، خواص را به صورت قیاسی تأیید می کند. بر خلاف جسی ، بر پارامتر کردن با توجه به مدل حافظه تمرکز دارد. WP طوری طراحی شده است که برخلاف جسی که برنامه C را مستقیماً به زبان Why وارد می کند ، با سایر افزونه های Frama-C مانند افزونه تجزیه و تحلیل ارزش همکاری می کند. WP می تواند به صورت اختیاری از پلت فرم Why3 برای استناد به بسیاری از پیش بینی های خودکار و تعاملی دیگر استفاده کند.
- آنالیز تاثیرات – تأثیرات تغییر در کد منبع C را برجسته می کند.
- برش – برش برنامه را قادر می سازد. این برنامه تولید یک برنامه جدید C کوچکتر است که برخی از ویژگی های داده شده را حفظ می کند. [۵]
- کد یدکی – کد بی فایده را از یک برنامه C حذف می کند.
سایر افزونه ها عبارتند از:
- سلطه گرها – سلطه گران و پیشفرض اظهارات را محاسبه می کند.
- از تحلیل – وابستگی های عملکردی را محاسبه می کند.
امکانات
Frama-C برای اهداف زیر قابل استفاده است:
- برای درک کد C که شما ننوشتید. به طور خاص ، Frama-C به شما امکان می دهد مجموعه ای از مقادیر را مشاهده کند ، برنامه را به برنامه های کوتاه تر تقسیم کند و در برنامه حرکت کند.
- برای اثبات خصوصیات رسمی روی کد. با استفاده از مشخصات نوشته شده در زبان مشخصات ANSI / ISO C ، آن را قادر می سازد تا از خواص کد برای هرگونه رفتار احتمالی اطمینان حاصل کند. Frama-C شماره های شناور را کنترل می کند. [۶]
- برای اجرای استانداردهای کدگذاری یا قراردادهای کد در کد منبع C ، با استفاده از افزونه های سفارشی [۷]
- برای تهیه کد C در برابر برخی نقص های امنیتی [۸]
همچنین ببینید
- SPARK (زبان برنامه نویسی)
منابع
- ↑ "Frama-C". frama-c.com. Retrieved 2016-11-05.
- ↑ CEA LIST. "CEA LIST, Smart digital systems". Retrieved 2016-11-05.
- ↑ Pascal Cuoq (August 2009). "Experience report: OCaml for an industrial-strength static analysis framework". Proceedings of the 14th ACM SIGPLAN International Conference on Functional Programming. 44 (9): 281–286. doi:10.1145/1631687.1596591.
{{cite journal}}: Unknown parameter|displayauthors=ignored (|display-authors=suggested) (help) - ↑ "Why homepage".
- ↑ Benjamin Monate; Julien Signoles (2008). "Slicing for Security of Code". Trusted Computing - Challenges and Applications. Lecture Notes in Computer Science. Vol. 4968/2008. ISBN 978-3-540-68978-2.
- ↑ Sylvie Boldo; Thi Minh Tuyen Nguyen (2010). "Hardware-independent proofs of numerical programs" (PDF). Proceedings of NFM 2010.
- ↑ David Delmas; Stéphane Duprat; Victoria Moya Lamiel; Julien Signoles. "Taster, a Frama-C plug-in to enforce Coding Standards" (PDF). Embedded Real Time Software and Systems 2010, Toulouse, France.
- ↑ Jonathan-Christofer Demay; Éric Totel; Frédéric Tronel (2009). "Automatic Software Instrumentation for the Detection of Non-control-data Attacks". Recent Advances in Intrusion Detection. Lecture Notes in Computer Science. Vol. 5758/2009. pp. 348–349. doi:10.1007/978-3-642-04342-0_19. ISBN 978-3-642-04341-3.