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

ابزار 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 آن نصب شد.

• نصب Frama-C

راهنمای نصب در لینک زیر قرار دارد اما بطور خلاصه دستورات نصب نیز ارائه شده است:

https://frama-c.com/install-aluminium-20160501.html#installing-frama-c-on-windows-via-cygwin--opam

sudo apt install opam

opam install depext

opam init

opam depext frama-c

برای بررسی برنامه fibonacci انتخاب شد که در فایل fibo.c قرار دارد و در انتهای این گزارش کد آن آورده شده است.

در سیستم عامل ubuntu فولدری با اسم c ایجاد کرده و سورس کد برنامه c که fibo.c است را در آن قرار داده ایم. داخل فولدر یک ترمینال برای خط فرمان باز کرده و در آن با دستور زیر برنامه frama-c را اجرا می کنیم.

frama-c-gui

سپس در برنامه frama-c از منوی project گزینه new project را انتخاب می کنیم. و فایل fibo.c را باز می کنیم.

• نحوه اجرای دستورات

قابلیت های Frama-c از دو طریق در دسترس است، از طریق GUI (واسط کاربری) و از طریق Batch Mode (اجرای دستورات در خط فرمان) . تمام دستوراتی که از طریق GUI قابلیت اجرا دارند حتما دستور معادل Batch دارند اما لزوما برای تمام فرمان های Batch معادل GUI وجود ندارد.

• بررسی CallGraph

از منوی analysis گزینه callgraph انتخاب شود

• بررسی ویژگی Inout

برای بررسی ورودی ها و خروجی های توابع از منوی analysis انتخاب گزینه 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

جهت مشاهده تصویری گراف بایستی با دستور زیر فایل dot به pdf تبدیل شود و گراف بصورت تصویری ساخته شود.

dot -Tpdf graph.main.dot > pdg.pdf

• بررسی Postdominator

این قسمت نیز از طریق CLIانجام می شود و دستور زیر باید اجرا شود:

frama-c fibo.c -dot-postdom main

با اجرای دستور زیر خروجی dot مرحله قبلی به pdf تبدیل می شود و گراف مربوطه در آن رسم می شود

• بررسی Slicing

جهت بررسی Slicing نسبت به متغیر n باید دستور زیر را در خط فرمان اجرا کرد:

frama-c slice-wr n fibo.c -slice-print > slice.txt

در حالت واسط کاربر نیز با کلیک راست روی متغیر مورد نظر، گزینه های slicing مختلفی وجود دارد

بررسی Users

این گزینه از منوی analysis قابل انتخاب است

• بررسی wp

با اجرای دستور زیر در خط فرمان می توان wp را بررسی کرد

frama-c -wp fibo.c

• بررسی Obfuscator

برای به هم ریختن syntax کد و ناخوانا کردن و مخفی کردن منطق کد با حفظ کارکرد قبلی و semantic کد استفاده می شود. کاربرد عموما برای کد های امنیتی هنگامی که در محیطی با اعتماد کم اقدام به استقرار می شود جهت جلوگیری از آشکار شدن یا جلوگیری از دیکامپایل شدن کد استفاده می شود.

• بررسی خصوصیت loop

نامتغیرهای مربوط به حلقه های تکرار را مشخص شود. این ویژگي با یک برنامه دیگر که ضرب ماتریس انجام می دهد و لوپ های زیادی دارد تست شد.

• بررسی occurrence

دفعات استفاده هر متغیر توسط occurrence مشخص می شود.

ضمن آنکه با کلیک راست روی متغیر مورد نظر گزینه occurrence برای متغیر مورد نظر در دسترس است

کد برنامه c تست شده که با نام fibo.c ذخیره شده است:

#include<stdio.h>

//Arash_Hadadi_97443088

//Program to print Fibonacci Series using Recursion

// declaring the function

void printFibo(int );

int main()

{

    printf(&quot\n\n\t\tStudytonight - Best place to learn\n\n\n&quot);

    int k, n;

    long int i = 0, j = 1;

    printf(&quotEnter the length of the Fibonacci series: &quot);

    scanf(&quot%d&quot, &n);

    printf(&quot\n\nfirst %d terms of Fibonacci series are:\n\n\n&quot,n);

    printf(&quot%d &quot, 1);

    printFibo(n);

    printf(&quot\n\n\t\t\tCoding is Fun !\n\n\n&quot);

    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(&quot%ld &quot, sum);

        printFibo(aj-1);    // recursive call

    }

    else

    {

        // after the elements, for line break

        printf(&quot\n\n\n&quot);

    }

}