فراما-سی

Frama-C

توسعه‌دهنده(ها)	Commissariat à l'Énergie Atomique (CEA-List) and Inria
مخزن	git.frama-c.com/pub/frama-c
نوشته‌شده با	اکمل
سیستم‌عامل	مایکروسافت ویندوز, فری‌بی‌اس‌دی, اوپن‌بی‌اس‌دی, لینوکس, مک‌اواس
در دسترس به	English
نوع	درستی‌یابی صوری, آنالیز ایستای برنامه
مجوز	mostly گنو ال‌جی‌پی‌ال, some parts under پروانه‌های بی‌اس‌دی
وبگاه	frama-c.com

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 زبان اضافه کنند . در میان اغلب استفاده می شود افزونه های عبارتند از:

تجزیه و تحلیل ارزش(Value analysis) - یک مقدار یا مجموعه ای از مقادیر ممکن را برای هر متغیر در یک برنامه محاسبه می کند. این افزونه از تکنیک های تفسیر انتزاعی استفاده می کند و بسیاری از افزونه های دیگر از نتایج آن استفاده می کنند.
جسی(Jessie) - خواص را به صورت قیاسی تأیید می کند. جسی برای اطمینان از ارسال تعهدات اثبات شده به پیش پرده های قضیه اتوماتیک مانند Z3 ، Simplify ، Alt-Ergo یا قضیه تعاملی مانند Coq یا چرا ، به پشتیبان چرا ^[۴] یا Why3 تکیه می کند. با استفاده از جسی ، اجرای حباب مرتب سازی یا سیستم رای گیری الکترونیکی اسباب بازی می تواند ثابت شود که مشخصات مربوط به آنها را برآورده می کند. از یک الگوی حافظه جدایی با الهام از منطق جدایی استفاده می کند .
WP (ضعیف ترین پیش شرط) - مشابه جسی ، خواص را به صورت قیاسی تأیید می کند. بر خلاف جسی ، بر پارامتر کردن با توجه به مدل حافظه تمرکز دارد. WP طوری طراحی شده است که برخلاف جسی که برنامه C را مستقیماً به زبان Why وارد می کند ، با سایر افزونه های Frama-C مانند افزونه تجزیه و تحلیل ارزش همکاری می کند. WP می تواند به صورت اختیاری از پلت فرم Why3 برای استناد به بسیاری از پیش بینی های خودکار و تعاملی دیگر استفاده کند.
آنالیز تاثیرات(Impact analysis) - تأثیرات تغییر در کد منبع C را برجسته می کند.
برش(Slicing) - برش برنامه را قادر می سازد. این برنامه تولید یک برنامه جدید C کوچکتر است که برخی از ویژگی های داده شده را حفظ می کند. ^[۵]
کد یدکی(Spare code) - کد بی فایده را از یک برنامه C حذف می کند.

سایر افزونه ها عبارتند از:

سلطه گرها(Dominators) - سلطه گران و پیشفرض اظهارات را محاسبه می کند.
از تحلیل(From analysis) - وابستگی های عملکردی را محاسبه می کند.

امکانات

Frama-C برای اهداف زیر قابل استفاده است:

برای درک کد C که شما ننوشتید. به طور خاص ، Frama-C به شما امکان می دهد مجموعه ای از مقادیر را مشاهده کند ، برنامه را به برنامه های کوتاه تر تقسیم کند و در برنامه حرکت کند.
برای اثبات خصوصیات رسمی روی کد. با استفاده از مشخصات نوشته شده در زبان مشخصات ANSI / ISO C ، آن را قادر می سازد تا از خواص کد برای هرگونه رفتار احتمالی اطمینان حاصل کند. Frama-C شماره های شناور را کنترل می کند. ^[۶]
برای اجرای استانداردهای کدگذاری یا قراردادهای کد در کد منبع C ، با استفاده از افزونه های سفارشی ^[۷]
برای تهیه کد C در برابر برخی نقص های امنیتی ^[۸]

نحوه ی نصب frama-c

ubuntu

جهت نصب بر روی ubuntu می توان مانند زیر عمل نمایید ابتدا terminal را باز می کنیم و با استفاده از دستور زیر نصب انجام می شود

sudo apt-get update -y

sudo apt-get install -y frama-c

نصب با استفاده از opam برای نصب frama-c به روش opam به شکل زیر است. Opam یک Package Manager برای OCamle است. برای نصب opam از دستور زیر استفاده میشود:

sudo apt-get install opam

Frama-c یک سری dependency های غیر OCamle ای از جمله Gtk و GMP دارد. در بسیاری از سیستم ها opam میتواند این وابستگی های خارجی را با پلاگین depext فراهم کند. برای استفاده از depext اینگونه عمل میکنیم:

opam install depext
opam depext frama-c

اگر سیستم توسط depext پشتیبانی نشود باید Gtk, GtkSourceView, GnomeCanvas و GMP جداگانه نصب شوند.

opam install frama-c

Fedora

۱- برای نصب Frama-C نیاز به مخزن RPM Fusion داریم در صورتی که این مخزن نصب نیست از طریق مراحل زیر اقدام به نصب نمایید.

۱-۱- باید ابتدا به سایت rpm fusion رفته به آدرس rpmfusion.org رفته و بر اساس معماری Fedora خود مخزن را دانلود نمایید.

۲-۱- پس از دانلود در ترمینال سیستم عامل با دستور rpm -ivh مخزن را نصب نمایید.

۲- سپس باید مخزن را آپدیت نمایید از طریق دستور dnf update میتوانید به جدید ترین پکیج ها دسترسی داشته باشید.

۳- سپس باید پکیج های مختلف شامل jcc و glibc و ++G را نصب نماییم برای نصب هر یک کافیست از دستور

dnf install [package name]

مثال :

dnf install jcc

dnf install glibc

dnf install g++

۴- در ادامه پس از نصب تمام پکیج های مورد نیاز بالا باید پکیج xkit را نصب کنید که مشابه دستورهای بالا قابل انجام خواهد بود.

۵- سپس به سایت frama-c رفته به آدرس frama-c.com و نسخه frama-c را بر اساس نوع سیستم عامل و معماری آن دانلود نمایید.

۶- سپس باید فایل tar را uncompress کنید ( توضیحات بیشتر برای استفاده از دستور tar )

۷- برای بهبود GUI برنامه Frama-c باید از پکیج Bladez از طریق دستور dnf install bladez نصب کنید.

۸- داخل پوشه extract شده frama-c رفته و ترمینال را باز کرده و با دستور install/. برنامه را نصب کنید.

محیط frama-c

جهت مشاهده محیط گرافیکی frama-c کافیست در ترمینال دستور زیر را وارد نمایید

frama-c-gui

منابع

↑ "Frama-C". frama-c.com. Retrieved 2016-11-05.
↑ CEA LIST. "CEA LIST, Smart digital systems". Retrieved 2016-11-05.
↑ Pascal Cuoq; et al. (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.
↑ "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.

PROFILBARU.COM