Frama-C ابزار تحلیل کد

a.hadadi — Wed, 12 Feb 2020 19:44:26 +0330

ابزار Frama-C برای تحلیل کد برنامه به زبان c استفاده می شود. اینجا با نصب ابزار Frama-C در ubuntu بطور عملی آشنا شده و چند ویژگی کد نمونه c را بررسی می کنیم.اگر سیستم عامل ubuntu را داشته باشید از این مرحله بگذرید و وارد مرحله نصب Frama-C شوید. چون سیستم عامل من windows10 هست و ابزارهایی مختص این سیستم عامل دارم ترجیح دادم vmware نصب کنم و ubuntu را بصورت vm اجرا کنم. البته Frama-C را می توانید مستقیما در ویندوز نصب کنید و برای این کار باید از PowerShell ویندوز استفاده کنید اما در نهایت محیط گرافیکی ubuntu را نخواهید داشت و برای داشتن gui آن باید یک سری ابزار اضافی نیز نصب کنید که پیچیدگی نصب را افزایش خواهد داد. بنابر این vmware نسخه 15 و ubuntu نسخه Ubuntu 18.04.4 LTS برای نصب انتخاب و vm آن نصب شد.اجرای سیستم عامل ubuntu از طریق vmنصب Frama-Cراهنمای نصب در لینک زیر قرار دارد اما بطور خلاصه دستورات نصب نیز ارائه شده است:https://frama-c.com/install-aluminium-20160501.html#installing-frama-c-on-windows-via-cygwin--opamsudo apt install opamopam install depextopam initopam depext frama-cبرای بررسی برنامه fibonacci انتخاب شد که در فایل fibo.c قرار دارد و در انتهای این گزارش کد آن آورده شده است. در سیستم عامل ubuntu فولدری با اسم c ایجاد کرده و سورس کد برنامه c که fibo.c است را در آن قرار داده ایم. داخل فولدر یک ترمینال برای خط فرمان باز کرده و در آن با دستور زیر برنامه frama-c را اجرا می کنیم.frama-c-guiسپس در برنامه frama-c از منوی project گزینه new project را انتخاب می کنیم. و فایل fibo.c را باز می کنیم.باز کردن فایل منبع Cمحیط برنامه بعد از باز کردن کد منبع cنحوه اجرای دستوراتقابلیت های Frama-c از دو طریق در دسترس است، از طریق GUI (واسط کاربری) و از طریق Batch Mode (اجرای دستورات در خط فرمان) . تمام دستوراتی که از طریق GUI قابلیت اجرا دارند حتما دستور معادل Batch دارند اما لزوما برای تمام فرمان های Batch معادل GUI وجود ندارد.بررسی CallGraph از منوی analysis گزینه callgraph انتخاب شودگزینه های callgraphcallgraph با نحوه نمایش درختیcallgraph با نحوه نمایش عمومیcallgraph هردو نحوه نمایش در کنار هم بررسی ویژگی Inoutبرای بررسی ورودی ها و خروجی های توابع از منوی analysis انتخاب گزینه Inout شودگزینه های مربوط به Inoutبعد از اجرای Inout خطوط برنامه که مربوط به ورودی و خروجی هستند مشخص می شونددر کنسول به تفصیل خروجی و ورودی ها آورده شده استبررسی Metricsاین گزینه را از CLI ادامه می دهیمفرمان زیر را در یک ترمینال نوشته و اجرا می کنیم:frama-c fibo.c -metricsدستور متریک و خروجی آن در خط فرمانبرای اینکه خروجی در یک فایل ذخیره شود می توانید دستور زیر را اجرا کنیدframa-c fibo.c -metrics > fibo_metrics.txtدستور متریک با ایجاد فایل خروجی و مشاهده متریک های برنامه در فایلگراف pdgاین دستور را نیز از طریق CLI انجام می دهیم. خروجی فایلی با پسوند dot می باشد که اطلاعات نودها و یال های یک گراف را در خود دارد.frama-c -pdg -pdg-dot graph -pdg-print fibo.c > pdg.dotخروجی pdg در فایلی با پسوند dot ذخیره می شودجهت مشاهده تصویری گراف بایستی با دستور زیر فایل dot به pdf تبدیل شود و گراف بصورت تصویری ساخته شود.dot -Tpdf graph.main.dot > pdg.pdfخروجی pdg ذخیره شده در فایل dot به گراف با پسوند pdf تبدیل می شودخروجی نهایی pdg بشکل گراف در فایل pdf ذخیره شده است بررسی Postdominatorاین قسمت نیز از طریق CLIانجام می شود و دستور زیر باید اجرا شود:frama-c fibo.c -dot-postdom mainخروجی دستور postdom در فایل main.main.dot و main.printfibo.dot ذخیره می شودبا اجرای دستور زیر خروجی dot مرحله قبلی به pdf تبدیل می شود و گراف مربوطه در آن رسم می شودخروجی گراف Postdominator بررسی Slicing جهت بررسی Slicing نسبت به متغیر n باید دستور زیر را در خط فرمان اجرا کرد:frama-c slice-wr n fibo.c -slice-print > slice.txtاسلایس نسبت به متغیر n محاسبه و در فایل ذخیره می شودمحتوای فایل اسلایس نسبت به nدر حالت واسط کاربر نیز با کلیک راست روی متغیر مورد نظر، گزینه های slicing مختلفی وجود داردگزینه های Slice در حالت GUIبررسی Usersاین گزینه از منوی analysis قابل انتخاب استمنوی usersخروجی تحلیل users در قسمت کنسول برنامه قابل مشاهده استبررسی wpبا اجرای دستور زیر در خط فرمان می توان wp را بررسی کردframa-c -wp fibo.cاجرای Wp و نتیجه آنبررسی Obfuscatorبرای به هم ریختن syntax کد و ناخوانا کردن و مخفی کردن منطق کد با حفظ کارکرد قبلی و semantic کد استفاده می شود. کاربرد عموما برای کد های امنیتی هنگامی که در محیطی با اعتماد کم اقدام به استقرار می شود جهت جلوگیری از آشکار شدن یا جلوگیری از دیکامپایل شدن کد استفاده می شود.برنامه اصلی خوانا و مشخصگزینه Obfuscate از منوی analysisبرنامه obfuscate شدهبررسی خصوصیت loopنامتغیرهای مربوط به حلقه های تکرار را مشخص شود. این ویژگي با یک برنامه دیگر که ضرب ماتریس انجام می دهد و لوپ های زیادی دارد تست شد.گزینه loop در analysisخروجی در قسمت console مشخص است. بررسی occurrenceدفعات استفاده هر متغیر توسط occurrence مشخص می شود.گزینه occurrence در منوی analysisنتیجه اجرا در کنسول برنامه قابل مشاهده است.ضمن آنکه با کلیک راست روی متغیر مورد نظر گزینه occurrence برای متغیر مورد نظر در دسترس استگزینه occurrence از طریق کلیک راستکد برنامه c تست شده که با نام fibo.c ذخیره شده است:#include//Arash_Hadadi_97443088//Program to print Fibonacci Series using Recursion// declaring the functionvoid printFibo(int ); int main(){ printf("\n\n\t\tStudytonight - Best place to learn\n\n\n"); int k, n; long int i = 0, j = 1; printf("Enter the length of the Fibonacci series: "); scanf("%d", &n); printf("\n\nfirst %d terms of Fibonacci series are:\n\n\n",n); printf("%d ", 1); printFibo(n); printf("\n\n\t\t\tCoding is Fun !\n\n\n"); return 0;} void printFibo(int aj){ static long int first = 0, second = 1, sum; if(aj > 1) { sum = first + second; first = second; second = sum; printf("%ld ", sum); printFibo(aj-1); // recursive call } else { // after the elements, for line break printf("\n\n\n"); }}

نوشته های a.hadadi

Frama-C ابزار تحلیل کد