https://virgool.ir/feed/@hadis.malek8حدیث ملک زنگنهfa2026-11-11 21:07:35https://virgool.ir/images/default-avatar.jpghttps://virgool.ir/@hadis.malek8https://virgool.ir/@hadis.malek8/یک-رویکرد-اجرای-concolic-در-embedded-device-ها-by4xyq3oxmviچکیده مقاله:با استفاده گسترده از embeded device ها، مشکلات امنیتی آنها باعث می شود که توجه زیادی بدان صورت پذیرد. بعنوان یکی از تکنیک های محبوب تست برنامه، اجرای نمادین یک برنامه بعنوان یک روش تست مورد استقبال عموم واقع شده است. به دلیل محیط پیچیده و کمبود منابع محاسباتی، هیچ روش اجرای نمادین با کارآیی موثر برای تجزیه و تحلیل firmware های در حال اجرا بر روی دستگاه ها وجود ندارد. در این مقاله ، ما یک رویکرد اجرای concolic جدید برای برنامه های firmware ارائه می دهیم. این رویکرد یک طرح تولید پویای تست برای انجام اجرای concolic در معماری های مختلف دستگاه های فیزیکی است. به منظور اینکه اطلاعات پیچیده محیط را بدست آوریم، اجرای concolic با استفاده از روش اشکال زدایی gdb میتواند به جمع آوری trace های برنامه و اطلاعات زمان اجرا بپردازد. برای غلبه بر کمبود منابع محاسباتی ، اجرای نمادین constraint های مربوطه را استخراج می کند و constraint های جمع آوری شده را برای تولید test case های جدید استفاده می کند. ما رویکرد را روی معماری های مختلف پیاده سازی می کنیم.تعریف مسئله و ورودی و خروجی مسئله:از آنجا که embedded device ها بیشتر در اینترنت استفاده می شوند ،تحقیقات در مورد امنیت این دستگاه ها بیشتر می شود. اما به دلیل تفاوت بین این دستگاه ها با کامپیوتر شخصی ، آنالیز سنتی نرم افزار را نمی توان مستقیماً روی firmware (برای مدیریت هر سخت افزاری یا بهتر بگوییم برای استفاده بهینه از امکانات سخت افزاری، نیازمند یک سیستم مدیریتی هستیم که توانایی مدیریت و زمانبندی اجرا و کنترل فرآیندها و پردازش ها را داشته باشد. در مدل های پیشرفته نام این سیستم مدیریتی سیستم عامل و در مدل های ساده تر نام آن Firmware یا به فارسی میان افزار است.) دستگاه اعمال کرد. در مقایسه با تحلیل نرم افزار های معمولی، تجزیه و تحلیل برنامه های Firmwareاین وسیله ها با مشکلات بیشتری روبرو است: اول ، نرم افزار روی رایانه ای با معماری x86-64 اجرا می شود ، و معماری دستگاه embedded که firmwareرا اجرا می کند متنوع است . دوم اینکه ایجاد محیطی برای تجزیه و تحلیل نرم افزارهای رایج آسان است، در حالی که embedded deviceها نسبتا بسته هستند ، که این باعث می شود ما محدودیت های بیشتری را در تحلیل برنامه های firmware نیاز داشته باشیم. ه منظور اخذ اطلاعات بیشتر در زمینه تجزیه و تحلیل برنامه firmware ، استفاده از روشی دقیق تر و قابل اعتمادتر ضروری است. تجزیه و تحلیل پویا می تواند اطلاعات بسیار مفیدی را بما ارائه دهد. در این راستا Symbolic execution که روشی برای تجزیه و تحلیل پویا است می تواند test case های موثری تولید کند، نقص نرم افزار را پیدا کند و آسیب پذیری های امنیتی را کشف کند. به طور خودکار ساخت یک فرمول منطقی، مسیر اجرای برنامه را توصیف می کند که باعث کاهش مشکل درک استدلال در منطق بکار رفته در برنامه می شود. با توسعه مداوم منابع محاسباتی، به طور مداوم قابلیت استفاده از اجرای نمادین بهبود یافته است. از طرفی نحوه تجزیه و تحلیل source codeدر اجرای نمادین نیز گسترش یافته است که به تولید constraintها در اجرای نمادین منجر می شود.ما می توانیم از تحقیقات قبلی برای انجام بهتر اجرای نمادین روی برنامه firmware بهره ببریم. در این راستا مشکلات زیر باید برطرف شوند:اول ، محدودیت منابع محاسباتی در embedded device ها نمی تواند نیازهای اجرای نمادین را برآورده سازند.دوم ، فقدان اطلاعات زمان اجرا در pure symbolic execution که موجب سختی تجزیه و تحلیل برنامه ها می شود؛سوم ، راه حل های پویا موجود فقط برای دستگاههای خاصی قابل استفاده هستند.با توجه به مشخصات کلی در دستگاه های embedded، مبنای مطالعاتی بر اساس concolic executionاست. ما رویکردی را بمنظور تجزیه و تحلیل برنامه firmware پیشنهاد می کنیم. این رویکرد به اجرای concrete در دستگاه های embeddedمنجر می شود و اجازه برگرداندن عملکردی صحیح را در state برنامه میدهد و می تواند دقت تحلیل را بهبود بخشد. همچنین اجرای نمادین را روی debugging hostانجام می دهد و به جمع آوری constraintهای مسیر برای تولید test case های جدید می پردازد. ما از ابزارها و پروژه های موجود برای پیاده سازی رویکرد خود استفاده می کنیم. برنامه firmware اجرای concreteرا روی یک دستگاه فیزیکی انجام می دهد که این خود، می تواند اطلاعات دقیق زمان اجرا و عملیات مربوط به سخت افزار مانند خواندن پیکربندی سخت افزار و غیره را بدست آورد، این اطلاعات برای تجزیه و تحلیل برنامه واقعی مفید است. روی debugging host ، ما میتوانیم کد باینری را به vexک ه یک زبان میانی (IR) است تبدیل می کنیم و اجرای نمادین را روی IRآن کد انجام دهیم که این کار محدودیت منابع محاسباتی را در دستگاه های embedded حل می کند. همچنین موتور اجرای نمادین برای ایجاد test case ها به حل constrain های جمع آوری شده میپردازد. test case های تولید شده دوباره توسط اجراهای concrete\symbolicبعدی استفاده می گردند. برای تأیید این رویکرد، ما روی سطوح توسعه ای مختلف و دستگاه های مختلف آزمایش انجام دادیم. دراین محیط ها ما برخی از برنامه های کوچک و بخشی از هسته های اصلی gnu (یک هسته سیستم‌ عامل است که به عنوان هسته سیستم عامل گنو و جایگزینی برای هسته یونیکس. گنو هرد از سال ۱۹۹۰ به وسیله پروژه گنو از بنیاد نرم‌افزار آزاد در حال توسعه است.) را آزمایش می کنیم و رویکرد ما می تواند این برنامه را در سطح بالایی پوشش دهد.معیارهای بررسی موضوع:در دسترس بودن واثربخشی رویکرد ما با ارزیابی توسط برخی برنامه های binutil در چارچوب این رویکرد تأیید می شود.نوآوری مقاله:دلایل اصلی که ما سعی می کنیم اشکالات firmware را با اجرای concolic کشف کنیم عبارتند از:اول ، نقش دستگاه های embedded در شبکه مهم است و امنیت دستگاه های embedded نسبت به کامپیوترهای شخصی کمتر نگران کننده است. در حالی که امنیت نرم افزار رایانه ای را میتوان با کاهش راه های مختلف حمله افزایش داد ، اما برنامه firmware بیشتر در شرایط محافظت ضعیف باقی مانده است. آسیب پذیری مانند CVE-2019-1579 انواع اساسی آسیب پذیری هایی از این دست با تأثیر بسیار زیادی است. به ناچار تعداد زیادی آسیب پذیری در انواع مختلف دستگاه های embedded وجود دارد.دوماً ، در حال حاضر ، اجرای نمادین توانسته است به طور موثر برنامه های باینری کوچک را تحلیل کند. در مقایسه با مدل فازی ، اجرای نمادین ممکن است هنوز شکاف خاصی درروند کار داشته باشد که باعث آسیب پذیری آن می شود و در تجزیه و تحلیل برنامه های بزرگ کارآمد نیست. اما به عنوان یک روش تست دقیق ، اجرای نمادین می تواند به پوشش کد نسبتاً بالایی دست یابد. با این حال، اندازه برنامه های firmware معمولی بسیار کوچکتر از برنامه نرم افزار رایانه ایست. ما معتقدیم که اجرای نمادین می تواند اثربخشی خود را در تجزیه و تحلیل برنامه firmware پس از حل مشکلات محیطی رایج در دستگاه های embeddedبه طور کامل نشان دهد . در حال حاضر پروژه های بسیاری وجود دارد که می توانند از رویکرد ما پشتیبانی کنند، اشکال زدایی از راه دور روی نرم افزارهای embeddedداشته باشند و به تجزیه و تحلیل برنامه ها در معماری با پردازنده های متعدد بپردازند. در هنگام طراحی رویکرد اصلی ما با اصول زیر مواجهیم:راه حل کارای اجرای concolic :در حالی که به همان اندازه حفظ اطلاعات مربوط به اجرای برنامه مهم است به همان اندازه ، کارآیی تجزیه و تحلیل برنامه هم باید قابل قبول باشد.تطبیق پذیری خاص: انواع مختلفی از فروشندگان دستگاه های embedded وجود دارد و تعداد انواع این دستگاه ها قابل شمارش نیست. طراحی یک راه حل برای هر دستگاه هزینه بر است. ما امیدواریم که بتوانیم رویکردی تهیه کنیم که بتواند به راحتی با چند تغییر ساده پیکربندی، برای انواع معماری ها جوابگو باشد.برای دستیابی به اهداف فوق ، ما رویکرد را به صورت زیرطراحی می کنیم:ما برای استخراج state برنامه هدف از تکنیک instrumentation استفاده می کنیم. به منظور پشتیبانی از معماری اصلی x86-64 مانند ARM ، PPC ،و MIPSکه در دستگاه embeded استفاده شده است ، یک اقدام اساسی این است که یک instrumentation مناسب را انتخاب کنید که بتواند برای برنامه های firmware تحت معماری های مختلف قابل استفاده باشد .مورد دیگر تبدیل اطلاعات state و کد هدف برنامه ها تحت معماری های مختلف و به شکلی واحد و یکپارچه است به طوری که اجرای نمادین backend نیازی به مقابله با constrains ها در معماری های مختلف نداشته باشد.ما روش تولید دینامیک تست را برای رویکرد اجرای concolic انتخاب می کنیم ، جایی که دستگاه فیزیکی اجرای concolic را انجام می دهد ، runtime state را روی برنامه هدف و از طریق طرح instrumentation انتخاب شده جمع آوری می کند ، وdebugging host اضافی برای اجرای نمادین معرفی می کند تا کمی و نقصان تجزیه و تحلیل ناشی از کمبود منابع محاسباتی با پشتیبانی اضافی با تجهیزات اشکال زدایی بیشتر جبران می شود .Test case مورد نیاز برای اکتشاف مسیر بطور خودکار تولید شده است. Test case های جدید می توانند برای مرحله بعدی اجرا استفاده شوند. مسیر کد برنامه firmware می تواند بر اساس استراتژی هایی مانند پوشش بلوک ها و گرایش هدف کشف شود.بررسی معیارها که چه معیاری را بهبود داده:چهار مرحله لازم در روند اجرای نمادین وجود دارد: ردیابی دستورالعمل ، اعمال دستورالعمل ، استخراج constraint، و حل constraint. ما روش این پروژه را بر مبنای این چهار مرحله توضیح خواهیم داد. کل اجرای concolicتوسط کاشف هدایت می شود. در حین اجرای concolic، دستورالعمل ردیابی توسط Block-Level Instrumentorموجود دردستگاه فیزیکی پیاده سازی شده است. اجرای concreteمسئولیت ضبط وضعیت اجرای برنامه هدف را بر عهده دارد. هر زمان که اجرای concreteبه ورودی بلوک اصلی برنامه می رسد ، Block-Level Instrumentor همه محتوای بلوک اصلی را برای اجرا بسمت موتور SE رهنمون می سازد. دستورالعمل ارتقاء برای اولین بار در موتور SE تکمیل می شود. کد مونتاژ بلوک اصلی به نوعی مناسب برای فهم زبان میانی واسطه ای تبدیل می شود. پس از تبدیل ، Symbolic Storage ساخت symbolic state شامل register، حافظه و دیگر اطلاعات لازم برای اجرای نمادین را آغاز می کند. هنگام ساخت Symbolic Storage ، ما اطلاعات stateرا با استفاده از Storage Backer یا همان پشتیبان ذخیره سازی، برای استخراج از دستگاه فیزیکی تا زمان احتیاج به اجرای نمادین اخذ می کنیم. وقتی موتور SEهنگام اجرای نمادین با آنها دیدار می کند ،شرطی که بلوک اساسی بعدی به آن نیاز داشته باشد در قالب یک بیان نمادین استخراج می شود. مدل constraint برای هر شاخه توسط یک بیان نمادین بازگشتی استخراج می شود. برای هر اجرای concrete ممکن است چندین شاخه متفاوت وجود داشته باشد، بنابراین ممکن است چندین نتیجه حین استخراج constraintوجود داشته باشد. پس از اتمام اجرای concrete ، موتور SE همه constraintهای جمع آوری شده را حل می کند و test caseرا مطابق با استراتژی اکتشاف می سازد. پس از آن ، کاشف اجازه اجرای concreteجدید را با استفاده از test case های تولید شده جدید می دهد.خلاصه ای از متدولوژی کار:در این بخش ، ما به طور عمده روش اجرای خود را توصیف می کنیم. چارچوب ما در python3 پیاده سازی شده است. به جز کاشف بعنوان واحد کنترل ، سایر ماژولهای چارچوب ما به عنوان پلاگ این های gdb وجود دارند.Block-Level Instrumentorاین ابزار مسئولیت کسب اطلاعات از statementبرنامه هدف را بر عهده دارد. در حال حاضر ، بیشتر تجزیه و تحلیل باینری توسط instrumentationانجام می شود ، اما همه اینها از معماری های متعدد دستگاه های embeddedحمایت نمی کنند. به منظور عبور ازفرم استاندارد اطلاعات state برنامه به اجرای symbolic ، ما از ابزار gdb-gdbserverبرای instrument برنامه هدف استفاده می کنیم .موتور SEموتور اجرای نمادین عمدتاً مسئولیت انجام این کارها را دارد:تبدیل کد باینری به زبان واسطه ، اجرای نمادین روی زبان واسطه ای ، جمع آوری constraint ها و حل آن constraintهای جمع آوری شده. با توجه به اینکه کد مونتاژ توسط Block-Level Instrumentor شامل معماری های مختلف است، ما کد باینری را به زبان واسطه ای برای کاهش فشار روی اجرای نمادین تبدیل می کنیم. ما vex را به عنوان زبان واسطه انتخاب میکنیم. ما موتور اجرایی وکس به نام ارزشیاب VEX-IRرا ساختیم که گزاره vex را ازکد اسمبلی ایجاد می کند و یک state نمادین را ایجاد می کند. مثل register نمادین و حافظه نمادین و محل ذخیره نمادین . سپس هنگام تجزیه و تحلیل ، می توانیم منبع مسیر های نمادین را به صورت دستی مشخص کنیم ، مانند ورودی خط فرمان استاندارد ، یا داده های دریافت شده توسط توابع کتابخانه ای مانند Scanf و read. در حین اجرای نمادین مبتنی بر Vex ،اجرای شبیه سازی تابع کتابخانه ای باید باشد که به طور مستقیم با موتور اجرای نمادین در ارتباط است. پس از اتمام کار constraintهای متعددی وجود خواهند داشت. برای حل این constraint ها از constraint solverاستفاده می شود. در رویکرد خود ، ما Claripy را به عنوان constraint solver انتخاب می کنیم که توسط تیم Angr و در پایتون ایجاد شده است. نتایج تولید شده توسط constraint solver درمجموعه test case های ایجاد شده نگهداری می شوند و از این test case ها برای اجرای concrete با توجه به استراتژی مندرج درکاشف استفاده بعمل می آید.محل ذخیره سازی نمادینوقتی برنامه به صورت نمادین اجرا می شود ، stateبرنامه نمادین است که به ساختار مربوطه برای پشتیبانی نیاز دارد. اطلاعات کلیدی هنگام اجرای یک برنامه شامل حافظه و ثبات ها ، داده های برنامه و وضعیت در حال اجرا هستند که در این ساختار ذخیره می شود. بنابراین state نمادین نیز به اینها احتیاج دارد و اطلاعات را در حافظه و ثبات به شکلی مناسب ثبت می کند. از آنجا که اطلاعات ذخیره شده ممکن است مقادیر نمادین باشد این باعث می شود که محتویات ذخیره شده در حافظه نمادین بسیار پیچیده شوند. ما از SymbolicStorage ، StorageSpaceو ساختارسه سطحی بجای state نمادین استفاده می کنیم. در میان آنها ،SymbolicStorageبه دو نوع تقسیم می شود: حافظه نمادین وثبات نمادین ، که به صورت نمادین ترکیب شده اند. SymbolicStorage در داخل حاوی یک شی StorageSpace برای ذخیره مقادیر نمادین ، و همچنین یک سری عملگر برای دسترسی به مقادیرنمادین است. شیء StorageSpaceحاوی صفحات بسیاری است که اندازه آنها برابر با اندازه صفحه حافظه در معماری برنامه هدف است. فضای ذخیره سازی مربوط به حافظه نمادین بوسیله یک روش تخصیص حافظه مشخص می شود. محتوای صفحه شی در هر صف بعنوان واحد ذخیره سازی سازماندهی می شود که هر عنصر یک واحد حافظه را نشان می دهد. واحد آغازین حافظه به یک شیء بنام Storage Object یا SOاشاره می کند، در حالی که باقی واحد های حافظه به شیء Noneاشاره می کنند. Storage Object واحد اصلی ذخیره سازی برای storage نمادین است.پشتیبان ذخیره سازیبه ویژگی های gdbمتکی است و بیشترین عملکرد آن خواندن محتوای حافظه و ثبات در دستگاه فیزیکی است. وقتی محتوا در Symbolic Storage موجود نباشد، از پشتیبان ذخیره سازی خواسته شده است تا حافظه را از دستگاه فیزیکی بر اساس هر صفحه بخواند و مقدار خوانده شده را به یک شیء SOذخیره شده درحافظه نمادین تبدیل کند.کاشفاین ماژول مسئول کنترل عملکرد کل چارچوب است. هنگام انجام هر اجرای concrete ، برنامه هدف را در دستگاه فیزیکی شروع کرده و ارتباط بین دستگاه فیزیکی و میزبان اشکال زدایی ایجاد می شود. پس از اجرای concrete کاشف از test case ها برای تولید test case های جدید و مطابق با استراتژی جستجوی مسیر استفاده می کند. بعبارتی از آنها برای اجرای concrete بعدی استفاده می کند. سرانجام ، برنامه هدف با توجه به اقدامات صورت گرفته بررسی می شود. بعد از دورهای بسیاری از این فرآیند، ما می توانیم به یک پوشش خاص از برنامه هدف برسیم.این مقاله تمرین درس اشکال زدایی دانشگاه شهید بهشتی است و جهت انتشار محتوای فارسی بیشتر است.hadis.malek8hadis.malek8Wed, 17 Jun 2020 15:30:21 +0430