بسیاری از برنامههای دنیای واقعی، فایلهای بسیار ساختاریافته (highly structured) و پیچیده را به عنوان ورودی دریافت میکنند. آزمون خودکار چنین برنامههایی، مسئلهای پیچیده و غیر بدیهی است. چنانچه ورودی آزمون با قالب فایل مشخص مطابقت نداشته باشد، برنامه یک خطای تجزیهگر (parser error) بازمیگرداند.
در فازینگ جعبه سفید مبتنی بر اجرای نمادین (symbolic execution-based whitebox fuzzing)، کدهای مربوط به مدیریت این خطاها میتوانند به یک عامل اتلاف زمان قابلتوجه تبدیل شوند. بخش زیادی از زمان تجزیهگر (parser)، صرف پیمایش و بررسی مسیرهای متعددی میگردد که همگی در نهایت منجر به خطاهای سادهی تجزیهگر (parser errors) میشوند. بدیهی است که این زمان بهتر است صرف بررسی بخشهای عملکردی (functional parts) برنامه شود؛ جایی که شکست در برابر ورودیهای معتبر میتواند باگهای (Bug) عمیق و واقعی را در برنامه آشکار کند.
ما در این مقاله، پیشنهاد میدهیم از اطلاعات مربوط به قالب فایل (file format) و قطعههای داده (data chunks) موجود در فایلهای معتبر و واقعی استفاده شود تا بتوان فرآیند کاوش (exploration) مسیرها را به سرعت از بخش تجزیهگر (parser) عبور داد. ما این رویکرد را فازینگ جعبه سفید مبتنی بر مدل (Model-based Whitebox Fuzzing – MoWF) نامگذاری میکنیم، زیرا مدل ورودیِ قالب فایل که در فازرهای جعبه سیاه (blackbox fuzzers) استفاده میشود، میتواند به عنوان یک محدودیت (constraint) بر فضای بسیار بزرگ ورودیها به کار گرفته شود تا در حین کاوش مسیرها (path exploration) در اجرای نمادین (symbolic execution)، اغلب ورودیهای نامعتبر حذف شوند.
ما این روش را روی ۱۳ آسیبپذیری در ۸ باینر برنامه بزرگ و با ۶ قالب فایل مجزا ارزیابی کردیم و دریافتیم که MoWF تمام این آسیبپذیریها را آشکار میکند، ر حالی که هر دو روش فازینگ جعبهسفید سنتی و فازینگ جعبهسیاه مبتنی بر مدل، هر کدام کمتر از نیمی از آنها را کشف میکنند. آزمایشهای ما همچنین نشان میدهند که MoWF بدون نیاز به هیچگونه دانه ورودی (seed) اولیه، ۷۰ درصد از آسیبپذیریها را کشف میکند.
۱. مقدمه (INTRODUCTION)
آزمون برنامههای پردازش فایل میتواند چالشبرانگیز باشد. اگرچه یک فایل ساختاریافته (structured file) به صورت یک بردار (vector) از بایتهای ورودی ذخیره میشود، اما اغلب به صورت یک درخت (tree) تجزیه (pars) میگردد؛ بهطوریکه قطعههای داده (data chunks) شامل فیلدها و همچنین سایر قطعههای داده هستند.
بینش کلیدی ما این است که برخی شاخهها (branches) در یک برنامهی پردازش فایل تنها تحت شرایط خاصی اجرا میشوند: (۱) وجود یک قطعههای داده (data chunk) مشخص، (۲) مقدار مشخصی از یک فیلد (field) درون یک قطعه داده و یا (۳) یکپارچگی (integrity) قطعههای داده.
از این رو، یک روش تولید آزمون (test generation) کارآمد نه تنها باید مقادیر مشخصی را برای فیلدها تعیین کند، بلکه باید بتواند کل قطعهها (chunk) را اضافه یا حذف کرده و یکپارچگی (integrity) آنها را برقرار کند (به عنوان مثال از طریق جمعآزما (checksum) یا اندازه (size)).
فازرها (Fuzzers) به تست چنین برنامههای پردازش فایل کمک میکنند. فازرهای جعبه سیاه مبتنی بر مدل (Model-based Blackbox Fuzzers – MoBF) [3, 5]، از مدلهای ورودی برای تولید فایلهای تصادفیِ معتبر استفاده میکنند. این مدل ورودی، قالب (format) قطعههای داده (data chunks) و محدودیتهای یکپارچگی (integrity constraints) را مشخص میکند. با این حال، اگرچه خروجیها معتبر میباشند، اما تغییرات همچنان ذاتاً تصادفی (random) باقی میمانند.
در مقابل، فازرهای جعبه سفید (Whitebox Fuzzers – WF) از اجرای نمادین (symbolic execution) برای کاوش نظاممندتر مسیرهای برنامه استفاده میکنند. با داشتن یک فایل معتبر، این روشها میتوانند مقادیر مشخص فیلدهای دادهای را بهخوبی تولید کنند. با این حال، زمانی که صحبت از حذف یا اضافه قطعههای داده(data chunks) یا اعمال محدودیتهای یکپارچگی (integrity constraints) به میان میآید، آنها با فضای جستجوی بزرگ ورودیهای نامعتبر مواجه میشوند [27].
فازرهای جعبه سفید مبتنی بر دستور زبان (Grammar-based Whitebox Fuzzers – GWF) قادر هستند فایلهایی تولید کنند که نسبت به یک دستور زبان مستقل از متن (context-free grammar) معتبر باشند [14]. این روشها (GWF)، مشابه فازرهای جعبه سفید (WF)، محدودیتهای مسیر (path constraints) را محاسبه میکنند؛ یعنی فرمولهای منطقی که فقط توسط فایلهای جدیدی که مسیرهای جایگزین (alternative paths) را اعمال میکنند، برآورده میشوند.
با این حال، برخلاف WF، این محدودیتها به عبارات منظم تبدیل میشوند، بهگونهای که یک حلکنندهی محدودیت مستقل از متن (context-free constraint solver) بتواند ورودی تولید کند که هم توسط دستور زبان و هم توسط این عبارت پذیرفته شود. با این حال، این عبارتها نسبت به محدودیتهای مسیر (path constraints) بسیار ضعیفتر هستند. فرض کنید اجرای نمادین (symbolic execution) به محدودیت مسیر ϕ ∧ (x < y) منجر شود.
پس از تبدیل، عبارت منظم دیگر قادر نیست آن محدودیت حسابی (arithmetic constraint) را شامل شود. علاوه بر این، GWF نمیتواند محدودیتهای مربوط به یکپارچگی (integrity constraints) مانند اندازه (size)، آفست (offset)، طول (length) و جمعآزما (checksum) را رمزگذاری کند. این بررسیهای یکپارچگی (integrity checks) در بسیاری از قالبهای فایل ساختاریافته مانند PNG ،PDF و WAV رایج میباشند.
در این کار، ما فازینگ جعبه سفید مبتنی بر مدل (Model-based Whitebox Fuzzing – MoWF) را ارائه میدهیم؛ یک تکنیک تست خودکار برای باینریهای برنامه در مقیاس صنعتی که ورودیهای ساختاریافته را پردازش میکنند. MoWF ترکیبی از فازینگ جعبه سیاه مبتنی بر مدل و فازینگ جعبه سفید است که به صورت کارآمد فایلهای معتبر تولید میکند و در عین حال، موقعیتهای هدف بحرانی (critical target locations) را به طور مؤثر اجرا میکنند.
این یک تکنیک کاوش مسیر هدایت شده (directed path exploration) است که مسیرهایی را که توسط ورودیهای نامعتبر و ناقص (invalid, malformed inputs) طی میشوند، از فضای جستجو حذف میکند.
(۱) MoWF از اطلاعات مربوط به قالب فایل (file format) برای کاوش آن دسته از شاخهها (branches) استفاده میکند که بسته به وجود قطعههای خاص (chunk) اعمال میشوند. برای این منظور، MoWF قطعه (chunk) مورد اشاره را حذف میکند یا یک قطعه معتبر جدید را با نمونهسازی از مدل ورودی اضافه میکند و یا از فرایندی که آن را « پیونددهی قطعه داده (data chunk transplantation)» مینامیم استفاده میکند. MoWF در این فرایند، مجموعه بایتهای ورودی متناظر با بخش مورد نیاز را در یک فایل اهداکننده (دهنده – donor file) شناسایی کرده و آنها را به محل مناسب در فایل گیرنده (receiving file) منتقل میکند.
(۲) MoWF از اجرای نمادین انتخابی (selective symbolic execution) [11] برای کاوش آن دسته از شاخهها استفاده میکند که وابسته به مقادیر خاصی از فیلدهای دادهای هستند.
(۳) در نهایت، MoWF یکپارچگی و صحت (integrity) فایلهای تولید شده را برقرار میکند و مقادیری مانند جمعآزما (checksum) و آفستها (offset) را اصلاح مینماید.
برخلاف MoBF، فازینگ جعبه سفید مبتنی بر مدل (MoWF)، هدایت شده (directed) است و مقادیر مشخص فیلدهای دادهای را به صورت نظاممندتر (systematic) شمارش میکند. MoWF برخلاف WF، درگیر فضای جستجوی بزرگ ورودیهای نامعتبر نمیشود و همچنین نیازی به دانه ورودی(seed inputs) ندارد (به [13، 16] مراجعه کنید).
MoWF برخلاف GWF، محدودیتهای مسیر کامل (full path constraints) را حفظ میکند، بنابراین هیچ تأثیری بر صحت (soundness) و کامل بودن (completeness) فازینگ جعبه سفید (WF) ندارد. علاوه بر این، MoWF از یک مدل ورودی (input model) رساتر اما سادهتر استفاده میکند تا بتواند محدودیتهای مربوط به یکپارچگی (integrity constraints) را نیز مدیریت کند.
مدل ورودی (input model) برای تولید کارآمد فایلهای معتبر، اعمال محدودیتهای مربوط به یکپارچگی (integrity constraints)، و تسهیل پیونددهی (transplantation) قطعه دادههای (data chunks) استفاده میشود. از آنجا که این مدل صرفاً فضای جستوجو را هرس (prune) میکند، نیازی نیست کامل (complete) باشد.
از یک سو، فازینگ جعبه سفید در نهایت با کاوش مسیرهایی که توسط مدل ورودی حذف نشدهاند، تمام فایلهای (نیمه)معتبر مرتبط را تولید میکند و از سوی دیگر، پیوند قطعههای داده از فایلهای اهدا کننده (دهنده – donor files) به حفظ محدودیتهای یکپارچگی ناقص یا کاملا تعیین نشده (underspecified integrity constraints) کمک میکند (به عنوان مثال، مشخص بودن الگوریتم فشردهسازی که دادهی تصویری در فایل PNG باید با آن کدگذاری شود). مدل ورودی یکبار ساخته میشود و میتواند در تمام جلسات تست آینده مورد استفاده قرار گیرد. همچنین نشان داده شده است که مدلهای ورودی میتوانند به صورت خودکار نیز استخراج شوند [19, 18, 17]. هر یک از مدلهای ورودی ما به صورت دستی در کمتر از یک روز ساخته شدهاند.
دو چالش اصلی فازینگ جعبه سفید سنتی (Traditional Whitebox Fuzzing – TWF) که ما به آنها میپردازیم عبارتاند از:
(۱) انفجار مسیر (Path Explosion). کد تجزیهگر (Parser code) اغلب بخش بزرگ و بسیار پیچیدهای از یک برنامه است. فازینگ جعبه سفید سنتی (TWF) در عمل، به دلیل تعداد نمایی (exponential) مسیرهایی که در تجزیهگر و توسط ورودیهای نامعتبر اجرا میشوند، درگیر فضای جستوجو میگردد [27].
(۲) وابستگی به دانه (Seed Dependence). اغلب رویکردهای فازینگ جعبه سفید سنتی (TWF) فرض میکنند که یک فایل دانه (seed file) وجود دارد که شامل تمام قطعه دادههای (data chunks) مورد نیاز است؛ در این حالت تنها کافی است مقادیر صحیح برای فیلدهای داده تنظیم شوند تا یک خطا آشکار گردد. با این حال، در عمل ممکن است اینگونه نباشد. ممکن است برخیاز قطعههای داده (data chunks) وجود نداشته باشند یا ترتیب آنها اشتباه باشد و یا در برخی موارد ممکن است اصلاً هیچگونه فایل دانهای (seed file) در دسترس نباشد.
مهمترین دستاوردهای MoWF به شرح زیر است:
- هرس کردن مسیرهای نامعتبر (Pruning Invalid Paths). مدل ورودی (input model) امکان حذف و هرس کردن (prune) اکثر مسیرهایی را فراهم میکند که توسط ورودیهای نامعتبر طی میشوند. MoWF برخلاف فازینگ جعبه سفید سنتی (TWF)، قادر است شاخههای کلیدی و حیاتی را که تنها در حضور برخی قطعههای داده (data chunks) خاص فعال میشوند، به صورت مستقیم حذف کند، بدون آنکه نیاز باشد این قطعههای داده به صورت تکرار شونده از طریق کاوش کد تجزیهگر (parser) ساخته شوند. تمام ورودیهای آزمایشی تولید شده معتبر هستند، به این معنا که با مدل ورودی (input model) سازگارند و محدودیتهای مربوط به یکپارچگی (integrity constraints) در آنها رعایت شده است. با در نظر گرفتن محدودیت زمانی ۲۴ ساعته، ابزار MoWF در آزمایشهای ما هر ۱۳ آسیبپذیری را کشف کرد، در حالی که ابزار TWF موفق به شناسایی تنها ۶ مورد از آنها شد.
- کاهش وابستگی به دانه (Reduced Seed Dependence). نمونهسازی (instantiation) از مدل ورودی (input model) این امکان را فراهم میکند که دانههای ورودی (seed inputs) از صفر (ابتدا) ساخته شوند. علاوه بر این، اگر یک دانه ورودی دارای یک قطعه داده (data chunk) باشد که برای رسیدن به یک موقعیت هدف (target location) کم است، MoWF میتواند از سایر فایلهای دانه (seed) به عنوان اهدا کننده (donor) استفاده کند، یک قطعه داده مفقود را پیوند دهد (transplant) و یک دانه ورودی جدید بسازد که به موقعیت هدف نزدیکتر باشد. در صورتی که هیچ اهدا کنندهای (donor) در دسترس نباشد، قطعه داده مفقود میتواند مستقیماً از مدل ورودی نمونهسازی شود. در میان ۱۳ آسیبپذیری موجود در موضوعات آزمایش ما، ابزار MoWF توانست ۹ مورد را بدون استفاده از هیچگونه دانه ورودی شناسایی کند.
- ابزار فازینگ (Fuzzing tool). ما ابزار MoWF خود را به عنوان یک توسعه از ابزار فازینگ جعبه سفید سنتی (TWF) به نام HERCULES [22] پیادهسازی کردهایم. ما ابزار MoWF را نه تنها با HERCULES (به عنوان TWF)، بلکه با فازر جعبه سیاه مبتنی بر مدل PEACH [3] نیز مقایسه میکنیم. با در نظر گرفتن یک بودجه زمانی ۲۴ ساعته، ابزار MoWF ما موفق شد هر ۱۳ آسیبپذیری موجود در موضوعات آزمایشی را کشف کند، در حالی که هر دو ابزار HERCULES و PEACH تنها ۶ مورد از آنها را شناسایی کردند.
بینشها (Insights). ما همچنین از طریق آزمایشهای خود، به بینشهایی درباره توانمندیهای نسبی تکنیک MoWF، فازینگ جعبه سفید سنتی مبتنی بر اجرای نمادین (symbolic execution-based TWF) و فازینگ جعبه سیاه مبتنی بر مدل (MoBF) مانند فازرهای Peach/Spike [3, 5] دست یافتیم. TWF تنها در صورتی عملکرد خوبی دارد که یک دانه ورودی(seed input) وجود داشته باشد که شامل تمام قطعههای داده (data chunks) ضروری بوده و صرفاً مقادیر مشخصی از فیلدهای داده تنظیم شوند.
MoBF زمانی عملکرد خوبی دارد که آسیبپذیری با قرار دادن مقادیر مرزی (boundary values) در برخی فیلدهای داده و یا با افزودن یا حذف قطعههای داده (data chunk) خالی آشکار شود. بهترین حالت کشف آسیبپذیریهای عمیق (deep vulnerabilities) که نیازمند مقادیر خاصی هستند، توسط رویکرد مبتنی بر اجرای نمادین (symbolic execution) انجام میشود. MoWF حتی در غیاب دانه ورودی نیز عملکرد خوبی دارد و میتواند به سرعت مقادیر مشخص مورد نیاز برای آشکارسازی آسیبپذیریهای عمیق را در حالی که همزمان توانایی افزودن و حذف قطعههای داده کامل را نیز مشابه MoBF حفظ میکند، تولید نماید.
۲. مرور کلی (Overview)
۲.۱ مثال انگیزشی (Motivating Example)
ما MoWF را بر اساس یک آسیبپذیری واقعی و جدی در یک کتابخانه (library) که همراه با چندین مرورگر و پخشکننده رسانه (media player) عرضه میشود، معرفی و انگیزهسازی میکنیم. LibPNG [24] کتابخانه رسمی مرجع برای قالب PNG است؛ این کتابخانه تقریباً از تمام قابلیتهای PNG پشتیبانی میکند و بیش از ۲۰ سال به طور گسترده مورد تست و ارزیابی قرار گرفته است. این کتابخانه در برنامههای محبوبی مانند پخشکننده VLC، مرورگر وب Google Chrome و Apple TV یکپارچهسازی و ادغام (integrated) شده است.
فایلهای PNG از چهار نوع قطعه داده (data chunk) اجباری و چهارده نوع قطعه داده اختیاری تشکیل میشوند. به منظور سهولت در تجزیه (parsing) و تشخیص خطا، قالب فایل علاوه بر دادهی اصلی، نیاز دارد که اندازه (size)، نوع (type) و جمعآزمای (checksum) هر قطعه داده نیز مشخص شود.
فایل PNG مشخص شده در شکل ۱، یک آسیبپذیری از نوع نقض دسترسی به حافظه (memory access violation) با شناسه OSVDB-95632 را در VLC 2.0.7 [25] که از LibPNG 1.5.14 استفاده میکند، آشکار میسازد. به منظور فعالسازی این باگ، عرض تصویر (image width) تعریف شده در قطعه IHDR باید مقدار مشخصی را در بازهی 0x7FFFFFF2 تا 0x7FFFFFFF بگیرد و همچنین باید قطعه اختیاری tRNS وجود داشته باشد. قطعه tRNS مقادیر آلفا (alpha values) را برای کنترل شفافیت (transparency) پیکسلهای تصویر مشخص میکند.
شکل ۱ ساختار بخشی از فایلی را نشان میدهد که این باگ را آشکار میکند. هشت بایت ابتدایی، فایل را به عنوان یک PNG شناسایی میکنند. چهار بایت بعدی اندازهی قطعه داده (data chunk) بعدی را مشخص میکنند (xD = hex(13) bytes0)، و پس از آن چهار بایت وجود دارد که نوع قطعه را که IHDR این است، تعیین میکند (بخش خاکستری روشن). ۱۳ بایت بعدی شامل فیلدهای داده هستند که عرض و ارتفاع تصویر را مشخص میکنند. پس از آن، چهار بایت جمعآزما (checksum) قرار دارد که صحت قطعه IHDR را تضمین میکند (بخش خاکستری تیره). بخشهای باقیمانده نیز به صورت مشابه ساختاریافته میباشند. دادهی تصویری موجود در قطعه IDAT با استفاده از الگوریتم فشردهسازی DEFLATE فشرده شده است [1] و پایان فایل PNG توسط قطعه IEND مشخص میشود.
لیست ۱، کد مربوطه در LibPNG را نشان میدهد. در هر تکرار، تابع png_read_info (خطوط ۲ تا ۲۷) اطلاعات مربوط به قطعه (chunk) فعلی از جمله اندازه (size) و نوع (type) آن را تجزیه میکند. بسته به نوع قطعه، تابع متناظر برای پردازش قطعه فعلی و اعتبارسنجی جمعآزما (checksum) فراخوانی میشود. این توابع handler، فیلدهای دادهای قطعه را تجزیه کرده و مقادیر آنها را برای مراحل بعدی تبدیل و پردازش تصویر (image transformation and processing) ذخیره میکنند.
قطعهها تا زمان رسیدن اولین قطعه از نوع IDAT (خطوط ۱۸ تا ۲۲)، تجزیه میشوند. فایلی که در شکل ۱ نشان داده شده است، تمام بررسیهای مربوط به تجزیهگر (parser) و کد مدیریت قطعهها (chunk-handling code) را با موفقیت پشت سر میگذارد و در نتیجه از دیدگاه سیستم معتبر (valid) محسوب میشود.
لیست ۱: کد ساده شدهی تجزیهگر (parser) برای قطعههای داده (data chunk). این کد به منظور تسهیل توضیح ارائه شده است؛ MoWF مستقیماً روی باینریهای برنامه (program binaries) کار میکند:
// read chunks’ info before first IDAT chunk
void png_read_info(png_structp ptr)
{
// read and check the PNG file signature
read_sig(f);
for (;;)
{
// get current chunk’s information
uint_32 length = read_chunk_header(ptr);
uint_32 chunk_name = ptr->chunk_name;
// mandatory chunks
if (chunk_name == png_IHDR)
handle_IHDR(ptr, length);
else if (chunk_name == png_IEND)
handle_IEND(ptr, length);
else if (chunk_name == png_PLTE)
handle_PLTE(ptr, length);
else if (chunk_name == png_IDAT)
{
ptr->idat_size = length;
break;
}
// optional chunks
else if ...
else if (chunk_name == png_tRNS)
handle_tRNS(ptr, length);
else if ...
}
}
// initialize row buffer for reading data from file
void png_read_start_row(png_structp ptr)
{
size_t buf_size;
...
buf_size = calculateBufSize(ptr);
ptr->row_buf = png_malloc(ptr, buf_size);
png_memset(ptr->row_buf, 0, ptr->rowbytes);
}
پس از آنکه تمام قطعههای دیگر تجزیه (parsed) شدند، LibPNG شروع به خواندن دادههای پیکسلی از قطعههای IDAT میکند. LibPNG برای هر سطر از تصویر، یک بافر تخصیص داده و مقداردهی اولیه میکند (خطوط ۳۱ تا ۳۸ در تابع png_read_start_row). این همان تابعی است که دارای خطا میباشد. به طور مشخص، وجود قطعه tRNS و اعتبارسنجی نادرستِ مقدارهای بزرگ برای عرض تصویر (image width) منجر به سرریز عدد صحیح (integer overflow) هنگام محاسبه اندازه بافر برای هر سطر میشود (به صورت ساده شده تابع calculateBufSize در خط ۳۵ نشان داده شده است). در نتیجه، بافری که تخصیص داده میشود بسیار کوچکتر از مقدار مورد نیاز است (خط ۳۶). سپس، یک سرریز بافر (buffer overflow) در تابع png_memset رخ میدهد که منجر به کرش کردن (Crash) برنامه میشود. توجه داشته باشید که آرگومان سوم در فراخوانی تابع memset (یعنی ptr→rowbytes) به مراتب بزرگتر از اندازه واقعی بافر تخصیصیافته است.
۲.۲ آشکارسازی آسیبپذیریها (Exposing Vulnerabilities)
۲.۲.۱ فازینگ جعبه سفید سنتی (Traditional Whitebox Fuzzing)
با داشتن یک فایل PNG سالم (benign) که شامل قطعه دادههای (data chunk) مورد نیاز در شکل ۱ باشد و همچنین داشتن موقعیت بحرانی و خطرناک (dangerous location) در تابع png_memset، یک ابزار فازینگ جعبه سفید (TWF) میتواند به صورت خودکار ورودی را تولید کند که منجر به کشف آسیبپذیری میشود.
با این حال، فرض کنید فایل سالم فاقد قطعه tRNS باشد؛ در این صورت، این موضوع به یک مانع برای TWF تبدیل میشود، زیرا بسیار بعید است که TWF بتواند این قطعه مفقود را به درستی تولید (synthesize) کند و در عین حال، اعتبار فایل را حفظ نماید. در واقع، چنانچه قطعه tRNS وجود نداشته باشد، شاخهی true در دستور شرطی (IF) خط ۲۵ در لیست ۱ طی نخواهد شد. اگرچه TWF میتواند این شاخه را نقض (negate) و قطعهای با نام «tRNS» ایجاد کند، اما اندازه (size) و محتوای (content) آن همچنان مطابق مشخصات یک قطعه دیگر باقی میماند.
در جایی که LibPNG انتظار دارد اندازه (size)، داده (data) و جمعآزمای (checksum) مربوط به قطعه جدید tRNS را دریافت کند، در عمل تنها دادههای تصادفی (random noise) را پیدا میکند. بنابراین، TWF دادههای تصویری که به درستی کدگذاری شدهاند را نادیده میگیرد (override) تا زمان قابلتوجهی را صرف ساخت یک قطعه tRNS معتبر در همان موقعیت کند.
از آنجا که قطعه IDAT اجباری است، TWF زمان بیشتری را صرف پیمایش فضای ورودیهای نامعتبر میکند تا بتواند یک قطعه IDAT دیگر بسازد و در نهایت به فایلی معتبری دست پیدا کند که شامل یک قطعه tRNS معتبر و تمام قطعههای اجباری باشد که تمامی محدودیتهای یکپارچگی (integrity constraints) در آن رعایت شدهاند.
۲.۲.۲ فازینگ جعبه سفید مبتنی بر مدل (Model-Based Whitebox Fuzzing)
ما فازینگ جعبه سفید مبتنی بر مدل (MoWF) را به عنوان ترکیبی از فازینگ جعبه سیاه مبتنی بر مدل و فازینگ جعبه سفید پیشنهاد میدهیم. رویکرد مبتنی بر مدل به MoWF این امکان را میدهد که فضای جستوجوی ورودیهای آزمایشی معتبر (valid test inputs) را به صورت کارآمد پوشش دهد، در حالی که رویکرد جعبه سفید، هر زیردامنه (subdomain) را با جزئیات و دقت بیشتری مورد پیمایش و کاوش قرار میدهد. این دو رویکرد در قالب یک حلقه بازخورد (feedback loop) با یکدیگر یکپارچه شدهاند که در شکل ۲ نشان داده شده است.
راهاندازی (Setup). در این مثال، کاربر باینری معیوب VLC، یک گزارش کرش (crash report)، مجموعهای از فایلهای PNG سالم موجود (در صورت وجود) و یک مدل PNG مطابق با لیست ۲ را ارائه میدهد. به منظور پیادهسازی MoWF، ما از یک فازر جعبه سیاه مبتنی بر مدل استفاده میکنیم. چارچوب Peach این امکان را فراهم میکند که قالب فایل به صورت Peach Pit [4] مشخص شود. این مدل، انواع (types) و روابط (مانند اندازه (size)، تعداد (count ) و آفست (offset)) بین قطعههای داده (data chunk) و فیلدها را توصیف و همچنین از مکانیزمهای اصلاح کننده (fixup) و تبدیل کننده (transformers) پشتیبانی میکند. مکانیزم اصلاح (fixup) به منظور تصحیح (repair) فیلدهای وابسته مانند جمعآزماها (checksum) استفاده میشوند. در حالی که مبدلها یا تبدیل کنندهها (transformers) برای کدگذاری (encoding)، رمزگشایی (decoding) و فشردهسازی (compression) به کار میروند.
PNG Peach Pit در لیست ۲، ابتدا یک قطعه داده (data chunk) عمومی را مشخص میکند (خطوط ۱ تا ۱۴). تمام قطعههای PNG حداقل شامل سه فیلد دادهای هستند که به ترتیب طول (length)، نوع (type) و جمعآزماهای (checksum) قطعه را تعیین میکنند. سایر قطعههای داده این ویژگیها را به ارث میبرند (خطوط ۱۵ تا ۳۱)، نوع قطعه را به صورت شمارشی (enumerable) تثبیت میکنند (مانند IHDR، PLTE، tRNS و …) و فیلدهای داده بیشتری را به آن اضافه مینمایند. در نهایت، کل فایل PNG تعریف میشود (خطوط ۳۲ تا ۴۲). این تعریف با یک عدد جادویی (magic number) مشخص (امضای فایلهای PNG) آغاز میشود، سپس یک قطعه هدر (IHDR) میآید و پس از آن تا ۳۰٬۰۰۰ قطعه (با ترتیبِ انعطافپذیر) قرار میگیرند، تا در نهایت با قطعه IEND خاتمه یابد.
لیست ۲: مدل ورودی PNG در قالب Peach Pit:
<DataModel name="Chunk">
<Number name="Length" size="32" >
<Relation type="size" of="Data" />
</Number>
<Block name="TypeData">
<Blob name="Type" length="4" />
<Blob name="Data" />
</Block>
<Number name="crc" size="32" >
<Fixup class="Crc32Fixup">
<Param name="ref" value="TypeData"/>
</Fixup>
</Number>
</DataModel>
<DataModel name="Chunk_IHDR" ref="Chunk">
<Block name="TypeData">
<String name="Type" value="IHDR" />
<Block name="Data">
<Number name="width" size="32" />
<Number name="height" size="32" />
...
</Block>
</Block>
</DataModel>
...
<DataModel name="Chunk_tRNS" ref="Chunk">
<Block name="TypeData">
<String name="Type" value="tRNS" />
<Blob name="Data" />
</Block>
</DataModel>
<DataModel name="PNG">
<Number name="Sig" value="89504e..." />
<Block name="IHDR" ref="Chunk_IHDR"/>
<Choice name="Chunks" maxOccurs="30000">
<Block name="PLTE" ref="Chunk_PLTE"/>
...
<Block name="tRNS" ref="Chunk_tRNS"/>
<Block name="IDAT" ref="Chunk_IDAT"/>
</Choice>
<Block name="IEND" ref="Chunk_IEND"/>
</DataModel>
با توجه به این پیکربندی، برای تولید ورودی که موجب کرش (Crash) در مثال انگیزشی میشود، MoWF موفق شده است: (۱) یک قطعه tRNS را در موقعیت مناسب در یک فایل PNG سالم (benign) درج کند، (۲) مسیرهای تحت تأثیر وجود tRNS به سمت موقعیت کرش (crash) را بررسی کند و (۳) مقدار مشخصی برای فیلد داده عرض تصویر (image width) در قطعه IHDR تولید کند. این فرآیند در چهار مرحله انجام میشود.
مرحله ۱: انتخاب دانه و شکستن فایل (Seed selection and file cracking). همانطور که در شکل ۲ نشان داده شده است، MoWF ابتدا فایلی را به عنوان ورودی اولیه (initial input) انتخاب میکند که از نظر شباهت، به یک موقعیت احتمالی کرش (potential crash location) نزدیکتر است. سایر فایلهای PNG که به عنوان فایلهای «اهدا کننده» (donor) در نظر گرفته میشوند توسط ماژول file cracker یا شکننده فایل، دیساسمبل (disassemble) شده و به مجموعهی قطعات (fragment pool) اضافه میگردند. این قطعات فایل میتوانند در صورت نیاز به داخل فایلهای ورودی منتقل (transplant) شوند.
چنانچه هیچ فایل اولیهای در دسترس نباشد، MoWF ورودی اولیه را مستقیماً از مدل ورودی (input model) نمونهسازی (instantiate) میکند. MoWF سپس تمام فیلدهای دادهای را که کاربر به عنوان «قابل تغییر» (modifiable) مشخص کرده است، به صورت نمادین (symbolic) علامتگذاری میکند. در فرآیند فازینگ، تنها همین فیلدهای قابل تغییر در نظر گرفته میشوند.
در این مثال، تمام فیلدهای داده (مانند عرض تصویر) به جز جمعآزما (checksum) و اندازه (size) قطعه، به عنوان قابل تغییر، علامتگذاری میشوند. در نتیجه، یک فایل PNG نمادین هیبریدی (hybrid symbolic PNG) به دست میآید؛ به این معنا که برخی بخشها دارای مقدار قطعی و واقعی (concrete) هستند و برخی دیگر نمادین. این فایل سپس به صورت کانکولیک (concolic) توسط یک فازر جعبه سفید سنتی اجرا میشود.
مرحله ۲: افزودن و حذف قطعههای داده (Adding and removing data chunks)
برخی شاخهها (branches) در یک برنامهی پردازش فایل تنها در صورتی اجرا میشوند که یک قطعه داده (data chunk) مشخص وجود داشته باشد یا بالعکس (وجود نداشته باشد). به منظور پیمایش این شاخهها در حین کاوش مسیر، MoWF آن قطعه مشخص را حذف و یا یک قطعه جدید به فایل اضافه میکند.
ابتدا، در هنگام اجرای یک فایل f داده شده، MoWF آن دسته از دستورات (گزارههای) شرطی مهم (crucial if-statements) را شناسایی میکند که وابسته به یک فیلد دادهای از نوع شمارشی (enumerable) در f هستند. شرطهای if در لیست ۱، در خطوط ۱۱ تا ۲۶ را میتوان مهم در نظر گرفت، در حالی که هیچیک از شرطهای داخل توابع handle_**** در این دسته قرار نمیگیرند.
در آزمایشهای ما مشاهده شده است که این نوع مقادیر شمارشی اغلب به صورت یکتا (uniquely)، نوع یک قطعه داده (data chunk) را مشخص میکنند. در ادامه، MoWF با استفاده از تحلیل آلودگی (taint analysis) کلاسیک، بایتهای ورودی در فایل f را که بر نتیجهی گزارههای شرطی شاخه (branch predicates) اثر میگذارند، شناسایی میکند. در مثال ما، MoWF رابطه بین بایتهای ورودی بالای جعبههای خاکستری در شکل ۱ وIFها در لیست ۱ را تعیین میکند، سپس MoWF نوع فیلد دادهای متناظر را با استفاده از مدل ورودی (input model) یاد میگیرد.
در نهایت، چنانچه فیلد دادهای از نوع شمارشی باشد و IF مربوطه قبلاً در هر دو جهت (true/false) اجرا نشده باشد، آن IF به عنوان یک شرط مهم در نظر گرفته میشود و MoWF یا قطعه داده (data chunk) متناظر را حذف میکند یا یک قطعه جدید را از طریق پیونددهی (transplantation) یا نمونهسازی (instantiation) از مدل ورودی اضافه میکند. هنگامی که MoWF نوع مربوط به قطعه دادهای که حذف یا اضافه میشود را شناسایی میکند، ماژول اتصال فایل (file stitcher)، پیونددهی قطعه داده را هماهنگ میکند.
نخست، ماژول اتصال فایل (file stitcher)، مجموعه (fragment pool) را جستوجو میکند تا قطعه دادههای (data chunk) کاندیدی را بیابد که مطابق با مدل ورودی (input model) مُجاز هستند در همان سطح با قطعه انتخاب شده در فایل دانه (seed) فعلی f قرار گیرند. در نهایت، ماژول اتصال فایل از مدل ورودی برای شناسایی مجموعه بایتهای ورودی مربوط به هر قطعه داده کاندید در مجموعه داده استفاده میکند و آنها را در مکان مناسب فایل گیرنده f پیوند میدهد تا تعدادی فایل اصلی جدید برای هر قطعه، تولید کند. به عنوان مثال، ما در ادامه فرض میکنیم که قطعه داده کاندید حاوی قطعه tRNS به عنوان انتخاب بعدی برگزیده میشود.
مرحله ۳: تغییر فیلدهای داده در قطعه داده درج شده (Changing data fields in inserted data chunk)
شاخههای دیگر در یک برنامه پردازش فایل تنها در صورتی اعمال میشوند که مقادیر خاصی در فیلدهای داده هر قطعه تنظیم شده باشند. در مثال ما، آسیبپذیری تنها زمانی آشکار میشود که عرض تصویر (image width) در بازهی مشخصی از مقادیر قرار گیرد. بهکارگیری این شاخهها با یافتن مقادیر خاص، نقطه قوت فازینگ جعبه سفید (whitebox fuzzing) محسوب میشود.
اجرای نمادین انتخابی (selective symbolic execution)، فضای جستوجوی محلی ورودیهای نیمهمعتبر (semi-valid inputs) را از نقطه آغاز شاخهی کلیدیِ نقض شده (negated crucial branch) کاوش میکند. این جستوجوی محلی در مقایسه با TWF کلاسیک، بسیار کارآمدتر است. هرگونه بررسی یکپارچگی (integrity check) در حین کاوش، شناسایی و نادیده گرفته میشود. فایلهایی که ممکن است در این مرحله نامعتبر شوند، بعداً در مرحلهی اصلاح فایل (file repair) تصحیح میگردند.
پس از رسیدن به موقعیت هدف (target location)، فازر جعبه سفید بررسی میکند که آیا همزمانی محدودیت مسیر (path constraint) و شرط کرش (crash condition) که از گزارش کرش استخراج شده یا به عنوان خروجی ابزار تحلیل ایستا (static analysis) ارائه شده است، رضایت بخش میباشد یا خیر. چنانچه این ترکیب رضایت بخش باشد، فازر یک ورودی منجر به کرش (crashing input) تولید میکند. در غیر این صورت، از هسته غیررضایت بخش (unsatisfiable core) برای هدایت پیمایش مسیر به سمت موقعیت کرش استفاده میکند و این بررسی را مجددا تکرار خواهد کرد.
مرحله ۴: تکرار (Repeat). در برخی قالبهای فایل (مانند WAV)، قطعههای داده (data chunk) میتوانند بهصورت تودرتو (nested) باشند. بنابراین، MoWF از فایلهای تولید شده به عنوان دانههای (seed) جدید استفاده میکند تا تکرار بعدی را از مرحله ۱ ادامه دهد. از میان دانههای (seed) گسترشیافته (شامل دانههای اولیه و جدید)، MoWF فایلی را انتخاب میکند که از نظر شباهت، به موقعیت کرش نزدیکتر باشد و سپس آن را به مراحل بعدی منتقل میکند. MoWF فایل انتخاب شده را اجرا میکند، گزارههای شرطی مهم (crucial if-statements) را شناسایی و قطعه دادهها (data chunk) را پیونددهی (transplant) میکند و به پیمایش مسیر (path exploration) ادامه میدهد.
خلاصه. MoWF در این مثال انگیزشی، این چهار مرحله را دنبال و در طول اجرای کانکولیک (concolic)، خط ۲۵ (لیست ۱) را به عنوان یک گزاره if مهم شناسایی میکند. ماژول اتصال فایل (file stitcher) از روی مدل ورودی (input model)، استنباط میکند که قطعه tRNS یک کاندید مناسب برای پیونددهی (transplantation) است و قرار گرفتن آن پس از قطعه PLTE و پیش از IDAT مُجاز میباشد. از این رو، ماژول اتصال فایل (file stitcher) یک قطعه tRNS را از مجموعه قطعات، منتقل کرده و یا مستقیماً یک قطعه tRNS حداقلی را از مدل ورودی نمونهسازی میکند و آن را درست پیش از قطعه IDAT قرار میدهد.
در نتیجه، شاخهی true از گزاره شرطی if در خط ۲۵ طی میشود و چانک tRNS پیش از ادامه پردازش، توسط برنامه تجزیه (parse) میگردد. پس از رسیدن به موقعیت کرش (Crash)، شرط کرش وابسته به عرض تصویر (image-width dependent crash condition) بررسی میشود و در نهایت یک فایل PNG تولید میگردد. فایل حاصل همچنان نامعتبر (invalid) است، زیرا مقدار جدید عرض تصویر باعث نامعتبر شدن مقدار جمعآزمای (checksum ) قطعه IHDR میشود. بنابراین، ابزار اصلاح فایل (file repair)، مقدار جمعآزما (checksum) را تصحیح میکند و آسیبپذیری آشکار میشود.
۳. فازینگ جعبه سفید مبتنی بر مدل (Model-Based Whitebox Fuzzing)
الگوریتم ۱ نمای کلی فرآیند فازینگ جعبهسفید مبتنی بر مدل به صورت هدایت شده (directed model-based whitebox fuzzing) را ارائه میدهد. این الگوریتم یک برنامه P، یک مدل ورودی M، مجموعهای از موقعیتهای هدف L در برنامه P و مجموعهای از ورودیهای اولیه (seed inputs) به نام T را دریافت میکند.
هدف الگوریتم ۱، تولید فایلهای معتبر (منجر به کرش) است که موقعیتهای L را اجرا میکنند. اگر هیچ هدفی (target) مشخص نشده باشد، MoWF از تحلیل ایستا (static analysis) برای شناسایی موقعیتهای خطرناک در برنامه مانند مکانهای بالقوه برای ارجاع به اشارهگرهای تهی (null pointer dereference) یا تقسیم بر صفر (divisions by zero) (خطوط ۱ تا ۳) استفاده میکند.
این الگوریتم از موارد آزمایشی ارائه شده در T به عنوان دانه (seed) برای تولید تست استفاده میکند. با این حال، اگر هیچ فایل اولیهای (seed file) ارائه نشده باشد، MoWF از مدل ورودی M برای نمونهسازی یک فایل دانه (seed file) استفاده میکند (خطوط ۴ تا ۷).
الگوریتم ۱: فازینگ جعبه سفید مبتنی بر مدل:
Input: Program P, Input Model M
Input: Initial Test Suite T , Targets L
Output: Augmented Test Suite T ′
if L = ∅ then
L ← IDENTIFYCRITICALLOCATIONS(P)
end if
if T = ∅ then
t ← INSTANTIATEASVALIDINPUT(M)
T ← {t}
end if
while timeout not exceeded do
Target location l ← CHOOSETARGET(L)
Input file t ← CHOOSEBEST(T, l)
Fragment Pool Φ ← FILECRACKER(T, M)
Crucial IFS Λ ← DETECTCRUCIALIFS(t, l, P, M)
for all λ ∈ Λ do
Valid files Tλ ← FILESTITCHER(t, λ, Φ, M)
for all tλ ∈ Tλ that negate λ do
Hybrid file ˆtλ ← MARKSYMBOLICVARS(tλ, M)
Files F ← PATHEXPLORATION(ˆtλ, λ, l, L, P)
for all f ∈ F do
Valid file f ′ ← FILEREPAIR(f, M)
T ← T ∪ f ′
end for
end for
end for
end while
T ′ ← T
حلقهی اصلی الگوریتم ۱ در خطوط ۸ تا ۲۴ نشان داده شده است. ابتدا، MoWF موقعیت هدف بعدی l را انتخاب میکند. اگر MoWF در حالت بازتولید کرش (crash reproduction mode) اجرا شود، آنگاه l همان موقعیت شناخته شدهی کرش است که از گزارش کرش استخراج شده است. در غیر این صورت، l بر اساس کمترین میانگین فاصلهاش نسبت به تمام دانههای (seed) موجود در T انتخاب میشود. فاصله بین یک ورودی t و یک موقعیت برنامه l در تعریف ۱ مشخص شده است.
در مرحله دوم، MoWF یک فایل دانه یا بذر (seed) بعدی t را بر اساس یک استراتژی جستوجو انتخاب میکند که هدف آن تولید ورودی بعدی با فاصله کمتر نسبت به l است (خط ۱۰). سایر فایلهای اولیه (seed) به ماژول شکستن فایل (file cracker) ارسال میشوند تا در خط ۱۱ مجموعه قطعات (fragment pool) Φ ساخته شود. این مجموعه قطعات، نقش اصلی در فرآیند پیونددهی قطعات داده (data chunk transplantation) را ایفا میکند.
تعریف ۱ (فاصله ورودی تا مکان):
با توجه به ورودی t، برنامه P و مکان برنامه l در P. فرض کنید Ω(t) مجموعه گرههایی (node) در نمودار جریان کنترل (CFG) از P باشد که توسط t اعمال میشوند. فاصله δ(t, l) از t تا l برابر با تعداد گرههای روی کوتاهترین مسیر از هر b ∈ Ω(t) تا l است. در ادامه، الگوریتم ۱ ورودی t را روی برنامه P اجرا میکند تا IFهای مهم (IFs Λ) را شناسایی کند (خط ۱۲). مطابق تعریف ۲، یک IF کلیدی تنها بر اساس نوع قطعه دادههای (data chunk) موجود در t در جهات مختلف ارزیابی میشود. پیادهسازی ما از مدل M استفاده میکند تا IFهای کلیدی را بر اساس وابستگی آنها به یک فیلد داده قابل شمارش (enumerable) در t شناسایی کند. مشاهده کردیم که این نوع مقادیر شمارشی اغلب به طور یکتا نوع یک قطعه داده (data chunk) را مشخص میکنند. توجه داشته باشید که IFهایی که نفی (negate) آنها باعث کاهش فاصله تا موقعیت هدف l نمیشود، در این فرآیند نادیده گرفته میشوند.
تعریف ۲ (گزاره شرطی مهم (Crucial IF-statement):
با توجه به ورودی t برای برنامه P و یک موقعیت هدف l در P، یک گزاره شرطی if به نام b در برنامه P زمانی مهم است که شرایط زیر برقرار باشد:
- دستور b توسط ورودی t در برنامه P اجرا شود.
- تنها یکی از دو جهت (directions) شاخه b پیمایش شده باشد.
- نفی شرط شاخه در b باعث کاهش فاصله تا موقعیت هدف l شود.
- اگر ϕ(b) را شرط شاخه در b در نظر بگیریم، نتیجهی ϕ(b) به فیلدی در t بستگی دارد که نوع (type) قطعه را مشخص میکند.
برای هر IF کلیدی λ که به این ترتیب شناسایی میشود، الگوریتم ۱ از ماژول اتصال فایل (file stitcher) برای نفی شرط شاخهی λ استفاده میکند (خطوط ۱۳–۱۴). برای هر فایل چسبیده شدهی tλ که بتواند با موفقیت شرط λ را نقض کند، الگوریتم، اجرای نمادین انتخابی و به دنبال آن اصلاح فایل را اجرا میکند تا مقادیر دقیق قطعههای داده را به دقت تنظیم کرده و فاصله تا موقعیت هدف l کاهش دهد (خطوط ۱۵-۲۰).
بهطور دقیقتر، تمام فیلدهای دادهای قابل تغییر (modifiable data fields) در فایل tλ به صورت نمادین (symbolic) علامتگذاری میشوند و پیمایش مسیر هدایت شده (directed path exploration) آغاز میگردد (خطوط ۱۶–۱۷). در طول پیمایش مسیر، MoWF بررسیهای مربوط به یکپارچگی (integrity checks) را به عنوان محدودیتهای شاخه (branch constraints) در نظر نمیگیرد. به عنوان مثال، یک بررسی جمعآزما (checksum) ممکن است اجازه تغییر یک فیلد داده را ندهد، در حالی که همان تغییر میتواند فاصله تا مجموعه اهداف L را کاهش دهد (مقایسه با TaintScope [26]). این محدودیت یکپارچگی در خط ۱۹ اصلاح میشوند.
هر زمان که یک موقعیت بالقوه خطرناک در L در دسترس قرار گیرد، MoWF بررسی میکند که آیا شرط کرش برقرار است یا خیر و بر اساس آن یک مورد آزمون (test case) منجر به کرش تولید میکند. بحث تفصیلی درباره رویههای الگوریتم ۱ در بخشهای بعدی ارائه شده است.
۳.۱ جستجوی مبتنی بر مدل هدایت شده (Directed Model-Based Search)
به منظور تولید ورودیهایی که آسیبپذیریها را آشکار کنند، MoWF از دانههای (seed) ورودی T برای کاهش فاصله تا موقعیت بحرانی ارائه شده یا شناسایی شدهی l استفاده میکند تا زمانی که آن موقعیت پیمایش شده و شرط کرش برآورده شود.
موقعیتهای بحرانی (Critical Locations). اگر هیچ هدف L به الگوریتم ارائه نشود، MoWF موقعیتهای بحرانی را در برنامه P شناسایی میکند. یک موقعیت بحرانی، موقعیتی از برنامه است که در صورت اعمال ورودی مناسب، ممکن است آسیبپذیری را آشکار کند. روشهای مختلفی برای شناسایی چنین موقعیتهای بحرانی وجود دارد [13، 26]. در پیادهسازی ما، از IDAPro [2] برای دیساسمبل کردن (disassemble) باینری برنامه P و انجام برخی تحلیلهای سبک (lightweight analysis) به منظور شناسایی دستورالعملهایی که با الگوهای نشان داده شده در لیست 3 مطابقت دارند، استفاده شده است.
این الگوها بخشی از دستورالعملهایی را پوشش میدهند که ممکن است منجر به آسیبپذیریهایی مانند تقسیم بر صفر (divide-by-zero) و ارجاع به اشارهگر تهی (null-pointer dereference) شوند. بهطور خاص، ما بر روی دستورالعملهای تقسیم (division) و جابهجایی حافظه (memory move) که از ثَباتها (register) یا آرگومانهای پشته (stack arguments) بهعنوان عملوند استفاده میکنند، تمرکز میکنیم. شرط کرش (crash condition) برای این دستورالعملها، بدیهی است. به این صورت که هر زمان در طی اجرای کانکولیک (concolic) به یک موقعیت بحرانی برسیم، بررسی میکنیم که آیا مقدار ثَبات (register) یا آرگومان پشته برابر صفر است (در حالت تعیین مقدار واقعی) یا میتواند صفر باشد (در حالت نمادین)؟
لیست ۳: قالب دستورالعملهای کرش (Crash instruction templates):
div register
div [ebp + argument_offset]
mov operand, [register]
mov operand, [ebp + argument_offset]
mov [register], operand
mov [ebp + argument_offset], operand
به منظور تولید ورودی که فاصله تا موقعیت هدف l را کاهش دهد، MoWF ابتدا آن دانه (seed) ورودی t را انتخاب میکند که کمترین فاصله را تا l دارد، و سپس IFهای کلیدی اجرا شده Λ را شناسایی میکند (خطوط ۱۰ و ۱۲ در الگوریتم ۱). هدف مرحلهی بعدی، یعنی پیونددهی (transplantation) و نمونهسازی قطعههای داده (data chunk)، تولید ورودیهای معتبری است که بتوانند شرایط شاخه (branch conditions) مربوط به Λ را نقض (negate) کنند.
در حالی که پیادهسازیهای دیگری نیز ممکن است، ما تصمیم گرفتیم از یک الگوریت تپه نوردی (hill climbing) استفاده کنیم. در پیادهسازی ما، تابع CHOOSEBEST، فایل ورودی t ∈ T را به گونهای انتخاب میکند که برای موقعیت انتخاب شده l ∈ L، کمترین فاصله را تا l داشته باشد. MoWF به منظور شناسایی شاخههای کلیدی Λ، ابتدا با استفاده از تحلیل آلودگی (taint analysis)، بایتهای ورودی در t را که ممکن است بر نتیجهی برخی از b ∈ Ω(t) تأثیر بگذارند، تعیین میکند. یادآوری میکنیم که Ω(t) مجموعهای از گرهها (node) در گراف جریان کنترل (CFG) برنامه P است که توسط t پیمایش میشوند. ما در پیادهسازی خود از تابع DETECTCRUCIALIFS، از قابلیتهای موجود در ابزار اجرای نمادین Hercules (هرکول) بهره گرفتهایم. در ادامه، MoWF از CFG استفاده میکند تا تعداد گرهها در کوتاهترین مسیر بین b و موقعیت l ∈ L را محاسبه کند.
نفی ϕ(b) تنها در صورتی میتواند فاصله تا l را کاهش دهد که b در بُرش رو به عقب ایستا (static backward slice) مربوط به l قرار داشته باشد و همچنین شاخهی ′b که بلافاصله پس از b میآید، مسیر کوتاهتری (از نظر تعداد گرهها) تا l نداشته باشد. در نهایت، MoWF از مدل ورودی M استفاده میکند تا فیلد دادهای متناظر با بایتهای ورودی شناسایی شده را تعیین و بررسی کند که آیا این فیلد داده، نوعِ قطعه (chunk) را مشخص میکند یا خیر. اگر تمام شرایط ذکر شده در تعریف ۲ برقرار باشند، آنگاه b به عنوان یک IF کلیدی علامتگذاری شده و به مجموعه Λ افزوده میشود.
اتصال فایل (File Stitcher). با داشتن یک فایل معتبر t و یک IF کلیدی λ، هدف تابع FILESTITCHER این است که شرط ϕ(λ) را نقض (negate) کرده و با حذف یا افزودن قطعهها (chunk) از t، فاصله تا موقعیت هدف l را کاهش دهد. در گام نخست، اتصال دهنده میبایست قطعه c در فایل t را تعیین کند که یا بایستی حذف گردد و یا یک قطعه دیگر باید قبل از آن درج شود تا ϕ(λ) نقض شود. این قطعه c قبلاً در مرحلهای که مشخص شد نتیجهی λ به فیلدی وابسته است که نوع c را تعیین میکند، شناسایی و ذخیره شده بود. در گام دوم، اگر طبق مدل ورودی، M مجاز باشد، stitcher با حذف c از t یک فایل جدید تولید میکند. در گام سوم، برای هر نوع قطعه C که قرار گرفتن آن قبل از c در t مجاز است:
(۱) پیونددهی (Transplantation). اگر در مخزن Φ یک قطعه c′ از نوع C وجود داشته باشد، بایتهای ورودی متناظر با c′ از فایل اهدا کننده (donor file) کپی شده و در موقعیت قبل از c در فایل گیرنده t قرار داده میشوند.
(۲) نمونهسازی (Instantiation). در غیر این صورت، از مشخصات نوع C در مدل ورودی M به عنوان یک قالب (template) استفاده میشود تا بایتهای مربوط به قطعه c′ تولید شده و قبل از c در فایل t قرار داده شوند. تمام فایلهایی که به این روش تولید شدهاند و واقعاً شرط λ را نقض (negate) میکنند، در مرحله بعدی یعنی اجرای نمادین انتخابی (selective symbolic execution) مورد استفاده قرار خواهند گرفت.
اصلاح فایل (File Repair). با داشتن یک فایل f و مدل ورودی M، ابزار file repair یکپارچگی (integrity) فایل را مجدداً برقرار میکند. در پیادهسازی ما، از سازوکارهای اصلاح (fixup) و تبدیل کننده (transformer) که میتوانند در مدل M چارچوب Peach Fuzzer تعریف شوند، استفاده میشود.
۳.۳ اجرای نمادین انتخابی و هدفمند (Selective and Targeted Symbolic Execution)
ما از استراتژی جستوجوی هدفمند برای کاوش نمادین (symbolic exploration) که در ابزار Hercules پیادهسازی شده است، مجدداً استفاده میکنیم. بهطور کلی، به منظور کاهش مشکل انفجار مسیر (path explosion)، این رویکرد تنها در برخی ماژولهای انتخاب شده و مهم (interest modules) امکان استدلال کاملاً نمادین (fully symbolic reasoning) را فراهم میکند؛ یعنی ماژولهایی مانند فایلهای اجرایی (exe.) و کتابخانههای پویا (dll.).
لیست این ماژولهای انتخاب شده از طریق ماژول هدف TM استخراج میشود؛ این ماژول شامل موقعیت هدف انتخاب شده است و همچنین از طریق یک گراف وابستگی ماژولها (Module Dependency Graph – MDG) تعیین میگردد. MDG با اجرای برنامهی تحت آزمون روی ورودیهای سالم (benign inputs) و جمعآوری پیونددهی کنترل (control transfer) بین ماژولهای برنامه ساخته میشود. ماژول هدف TM و تمام ماژولهایی که در مسیر از ماژول ورودی (entry module / main program) تا TM قرار دارند، با استفاده از MDG ساخته شده برای حالت اجرای نمادین کامل (fully symbolic execution mode) انتخاب میشوند.
استراتژی جستوجوی Hercules (هرکول) [22] به صورت هدفمند (targeted) است، به این معنا که مسیرهای برنامه را به سمت یک موقعیت هدف (target location) مانند موقعیتهای بحرانی از جمله محلهای منجر به کرش کاوش میکند و در عین حال مسیرهای نامرتبط (irrelevant paths) را هرس (prune) میکند. علاوه بر این، Hercules از از هسته صدق پذیر (unsatisfiable core) که توسط یک حلکننده نظریه (theory prover) مانند Z3 تولید میشود [12]، برای هدایت (guide) فرآیند کاوش استفاده میکند.
۳.۴ مدیریت مدلسازی ناقص حافظه (Handling Incomplete Memory Modeling)
مدلهای حافظه در موتورهای اجرای نمادین (symbolic execution engines) مانند Hercules، KLEE یا [22, 10, 11] S2E از تخصیص حافظه با اندازه نمادین (symbolic size) پشتیبانی نمیکنند. چنانچه یک اندازه نمادین (symbolic size) داده شود، پیش از تخصیص حافظه هیپ (heap)، مقدار واقی آن تعیین میشود (concretized). این مکانیزمِ تعیین مقدار واقعی (concretization) ممکن است مانع از آشکارسازی آسیبپذیریهای سرریز بافر هیپ (heap buffer overflow) شود. برای مثال، در مثال انگیزشی، فرض کنید عرض تصویر (image width) در فایل PNG سالم مقدار بسیار کوچکی مانند ۱ داشته باشد و بهصورت نمادین علامتگذاری شده باشد.
در کد پردازش، LibPNG باید یک بافر هیپ (heap) با اندازه نمادین تخصیص دهد که به عرض تصویر (و سایر متغیرهای نمادین) وابسته است. هنگامی که بافر تخصیص داده میشود، مقدار عرض تصویر در P C توسط قید روی مقدار مشخص شده برای اندازه بافر تخصیص داده شده محدود میشود.
پس از رسیدن به موقعیت کرش (برای مثال، دستورالعملی که به بافر heap تخصیص یافته دسترسی دارد)، Hercules قابلیت صدق پذیری (satisfiability) پیوستگی میان محدودیت مسیر فعلی (path constraint – PC) و شرط کرش (crash condition – CC) را بررسی میکند. فرض کنید یه منظور برآورده ساختن (صدق پذیری) شرط کرش، عرض تصویر (image width) باید به اندازه کافی بزرگ باشد. در فایل فعلی که دارای عرض تصویر کوچک است، ممکن است شرط کرش CC با محدودیت مسیر PC در تضاد باشند؛ بهطوریکه ترکیب PC ∧ CC صدق ناپذیر (unsatisfiable) باشد.
Hercules غالبا، بر اساس هسته صدقناپذیر (unsatisfiable core) مربوط به PC ∧ CC، مجموعهای از شاخهها را پیدا میکند که میتوان آنها را نقض (negate) نمود تا مسیرهای همسایهای که در آنها احتمال برآورده ساختن شرط کرش CC وجود دارد، بررسی شوند. با این حال، از آنجا که مقدار width قبلاً به یک مقدار مشخص مقید شده است، هیچ مسیر جایگزینی (alternative path) وجود ندارد که در آن شرط کرش CC صدق ناپذیر باشد.
ما در توسعهی Hercules، از پیشرفتهای اخیر در بیشینهسازی صدق پذیری (Maximally Satisfiable / MaxSMT) با Z3 [8, 12] استفاده میکنیم. با استفاده از یک لیست سفید (whitelist)، ابزار ما به صورت خودکار برخی از شروط (clauses) را به عنوان شروط آسان (soft clauses) علامتگذاری میکند. حل کننده صدق پذیری بر اساس نظریه ها (SMT) یعنی Z3 امکان ایجاد یک انتساب (assignment) به متغیرهای نمادین را به عنوان راه حلی فراهم میکند که شرط محدودیت تمام شروط -اما نه لزوماً شروط آسان- را برآورده میکند.
به طور مشخص، در رویکرد ما تمام محدودیتهای موجود در شرط کرش (CC) به عنوان شروط سخت (hard clauses) در نظر گرفته میشوند، در حالی که مثلاً محدودیتهای مربوط به تخصیص حافظه در محدودیت مسیر (PC) به عنوان شروط آسان (soft clauses) مشخص میگردند.
برای تعیین اینکه کدام محدودیتها در PC میتوانند آسان باشند، ابتدا بررسی میکنیم که آیا ترکیب PC ∧ CC صدق ناپذیر (unsatisfiable) است یا خیر. اگر چنین باشد، تمام متغیرهای نمادین موجود در CC استخراج میشوند. سپس تمام محدودیتهای موجود در PC شده و هر محدودیتی که شامل یکی از متغیرهای نمادین CC باشد، به عنوان محدودیت آسان در نظر گرفته میشود.
پس از انجام این مراحل، یک PC به روز شده (′PC) به دست میآید و آن را به حلکننده MaxSMT ارسال میکنیم تا بیشینه صدقپذیری PC′ ∧ CC بررسی شود. چنانچه P C′ ∧ CC صدقپذیر باشد (حتی با این امکان که یک یا چند شرط آسان در ′PC نادیده گرفته شوند)، در این صورت یک فایل ورودی به عنوان راهحل تولید میشود. در نهایت، به عنوان یک تأیید اضافی، فایل تولید شده را با ارسال آن به باینری برنامه اعتبارسنجی میکنیم و بررسی میکنیم که آیا منجر به کرش برنامه میشود یا خیر.
۴. پیادهسازی (IMPLEMENTATION)
ابزار MoWF ما بر پایه چندین ابزار و کتابخانهی شخص ثالث ساخته شده است. ما این تکنیک را در موتور اجرای نمادین هدایت شده Hercules پیادهسازی کردیم که خود از S2E و حل کننده صدق پذیری بر اساس نظریه ها (SMT) یعنی Z3 استفاده میکند. همچنین دقت تحلیل آلودگی (taint analysis) پیادهسازی شده در Hercules را بهبود دادیم. به منظور تحلیل ایستا (static analysis) و شناسایی موقعیتهای خطرناک در کد برنامه (موقعیتهایی که اجرای آنها ممکن است باعث کرش شود، مطابق بخش 3.1)، از IDA Pro و ابزار ابزارگذاری باینری پویای اینتل (Intel Dynamic Binary Instrumentation Tool) (برای ابزار PIN) استفاده کردیم.
ابزار PIN همچنین به منظور تحقق دو هدف به کار گرفته شد:
(۱) پروفایلسازی دستورالعملها (instruction profiling) برای تولید ردگیری اجرای برنامه (execution trace) و محاسبه فاصله ورودی دانه (seed) فعلی تا موقعیتهای بحرانی و خطرناک،
(۲) پروفایلسازی شاخهها (branch profiling) به منظور تعیین اینکه کدام شاخههای کلیدی (crucial branches) کاوش شدهاند.
چارچوب مربوط به فازر جعبه سیاه مبتنی بر مدل Peach (Peach model-based blackbox fuzzer) امکان پیادهسازی اجزای مبتنی بر مدل ورودی از جمله File Cracker ،File Stitcher و File Repair را فراهم میکند. در واقع، مورد اول (File Cracker) برای اهداف ما اصلاح شد و دو مورد آخر (File Stitcher و File Repair)، به عنوان مثال برای پشتیبانی از پیوند قطعههای داده (data chunk transplantation)، از ابتدا پیادهسازی شدند.
۵. ارزیابی تجربی (Experimental Evaluation)
ما تکنیک MoWF را به صورت تجربی ارزیابی کردیم تا به سؤالات پژوهشی زیر پاسخ دهیم:
- پرسش پژوهشی اول: MoWF در مقایسه با فازینگ جعبه سفید سنتی (Traditional Whitebox Fuzzing – TWF)، چه تعداد آسیبپذیری را آشکار میکند؟
- پرسش پژوهشی دوم: MoWF در مقایسه با فازینگ جعبه سیاه مبتنی بر مدل (Model-based Blackbox Fuzzing – MoBF)، چه تعداد آسیبپذیری را آشکار میکند؟
- پرسش پژوهشی سوم: اگر هیچ ورودی دانه اولیه (initial seed inputs) در دسترس نباشد، MoWF چه تعداد آسیبپذیری را میتواند آشکار کند؟
هر یک از این تکنیکها با یک بازه زمانی ۲۴ ساعته مورد ارزیابی قرار گرفتند.
۵.۱ تنظیمات آزمایش (Experimental Setup)
۵.۱.۱ موضوعات آزمایش (Subjects)
ما موضوعات آزمایش را از میان مجموعهای از باینریهای برنامه شناخته شده و پرکاربرد مانند پخشکنندههای ویدئو (video players)، برنامههای خواندن اسناد (document readers)، پخشکنندههای موسیقی (music players) و ویرایشگرهای تصویر (image editors) انتخاب کردیم. برنامههایی که با انواع مختلف و پیچیدهای از قالبهای فایل (file formats) کار میکنند.
از آنجا که Hercules به عنوان تکنیک پایه (baseline) استفاده میشود، ما همچنین هر پنج موضوعی را که در ارزیابی اولیه Hercules استفاده شده بودند نیز به مجموعه اضافه کردیم [22] (در جدول با پسزمینه خاکستری مشخص شدهاند). ما همچنین دستهبندی انواع آسیبپذیریها را نیز مدنظر قرار دادیم. همانطور که در جدول ۱ نشان داده شده است، ما هشت برنامه واقعی متفاوت (برخی با نسخههای مختلف) را انتخاب کردیم: Adobe Reader، VLC media player، Windows Media Player ،RealPlayer، Music Animation Machine MIDI Player (MP) ،XnView ،LibPNG و Orbital Viewer.
جدول ۱: برنامههای موضوعی
دول ۱ نه تنها موضوعات آزمایش و نسخههای آنها را نشان میدهد، بلکه ماژولهای دارای باگ (buggy modules) و اندازههای مربوط به آنها را نیز ارائه میکند. علاوه بر این، این جدول شامل تعداد آسیبپذیریهای شناختهشدهای است که هدف ما بازتولید (reproduce) آنها بوده است. ما در یک مورد (XnView)، کار را بدون هیچ آسیبپذیری شناختهشدهای آغاز کردیم و به دنبال آسیبپذیریهای ناشناخته گشتیم. در موارد دیگر، با وجود اینکه هدف ما بازتولید آسیبپذیریهای شناخته شده بود، موفق شدیم آسیبپذیریهای جدیدی را کشف کنیم. در واقع، ابزار MoWF ما با موفقیت تمام ۹ خطای شناخته شده را بازتولید کرد و علاوه بر آن ۴ خطای ناشناخته را نیز کشف نمود ( ۳ مورد در XnView و ۱ مورد در Windows Media Player ) – به بخش ۵.۲ مراجعه کنید.
۵.۱.۲ مدلسازی ورودی (Input Modeling)
به منظور تعریف مدلهای ورودی پنج قالب فایل (PDF، PNG، MIDI، FLV و ORB) از ابتدا، از زبان مدلسازی فازر جعبه سیاه مبتنی بر مدل Peach Fuzzer استفاده کردیم. همچنین مدل ورودی مربوط به فایلهای WAV را که بهصورت آزاد توسط Peach Fuzzer ارائه شده بود، بهبود بخشیدیم (augment). بهطور مشخص، ما یک قالب تصویری رایج (PNG)، سه قالب صوتی و ویدئویی (MIDI، WAV و FLV)، یک قالب سند قابل حمل (PDF) و یک قالب فایل هندسی (ORB) را مدلسازی کردیم. در جدول ۲، اندازه مدلهای ورودی گزارش شده است که نسبتاً کوچک هستند و از ۴ کیلوبایت تا ۱۴ کیلوبایت متغیر میباشند. برای نوشتن هر مدل مربوط به یک فرمت فایل، کمتر از یک روز زمان صرف شد.
جدول ۲: اطلاعات مربوط به مدلهای ورودی
۵.۱.۳ انتخاب فایلهای دانه اولیه (Initial Seed Files Selection)
برای انتخاب فایلهای دانه اولیه، به طور تصادفی ۱۰ فایل با قالب مربوطه را از اینترنت بارگیری کردیم، به جز فایلهای دانه اولیه با قالبهای ORB و PNG. فایلهای ORB از وبسایت فروشنده بارگیری و فایلهای PNG از مجموعه تست آنلاین Schaik بارگیری شدند. اندازه متوسط فایلهای دانه در هر مجموعه تست در ستون پنجم جدول ۲ نشان داده شده است.
۵.۱.۴ زیرساخت (Infrastructure)
ما سه ابزار را مورد ارزیابی قرار دادیم: ابزار MoWF خود، فازر جعبه سفید سنتی Hercules (TWF) و فازر جعبهسیاه مبتنی بر مدل Peach Fuzzer (MoBF). به منظور انجام آزمایشها، از نسخه عمومی (community version) فازر Peach که همراه با کد منبع آن ارائه میشود استفاده کردیم. هر دو روش مبتنی بر مدل (model-based) از یک مدل ورودی یکسان استفاده کردند. تمام برنامههای مورد آزمایش روی سیستمعامل Windows XP نسخه ۳۲ بیتی SP3 اجرا شدند. برای هر برنامه، هر ابزار بهگونهای تنظیم شد که پس از ۲۴ ساعت اجرا به صورت خودکار متوقف گردید (timeout). تمام آزمایشها روی یک رایانه با پردازنده 3.6GHz Intel Core i7-4790 و ۱۶ گیگابایت حافظه RAM انجام شدند.
۵.۲ نتایج و تحلیل (Results and Analysis)
جدول ۳ نتایج مربوط به بازتولید آسیبپذیریهای شناخته شده و کشف آسیبپذیریهای ناشناخته را برای سه تکنیک مورد مقایسه نشان میدهد. بهطور کلی، در این آزمایشها ابزار MoWF ما عملکرد بهتری نسبت به دو ابزار Hercules و Peach داشته است.
در حالی که ابزار MoWF ما با موفقیت، ۱۳ ورودی منجر به کرش تولید کرده است، نه Hercules و نه Peach هیچکدام قادر به تولید حتی نیمی از آنها نبودند. علاوه بر این، ابزار MoWF ما موفق به کشف آسیبپذیریهای ناشناخته احتمالی در Windows Media Player و XnView نیز شده است. این آسیبپذیریها پیشتر در پایگاههای MITRE ،OSVDB یا Exploit-DB گزارش نشده بودند.
همچنین قدرت ابزار MoWF ما با توانایی آن در آشکارسازی انواع مختلف آسیبپذیریها نیز نشان داده میشود، از جمله سرریز عدد صحیح (integer overflow)، سرریز بافر (buffer overflow)، ارجاع به اشارهگر تهی (null pointer dereference) و تقسیم بر صفر (divide-by-zero). در بخشهای بعدی، تحلیل عمیقتری ارائه میدهیم تا به سه سؤال پژوهشی در خصوص اثربخشی و حساسیت رویکرد خود پاسخ دهیم.
پرسش پژوهشی ۱: مقایسه با فازینگ جعبه سفید سنتی (Traditional Whitebox Fuzzing)
آزمایشهای ما تأیید میکنند که فازر جعبه سفید سنتی (TWF) به احتمال زیاد قادر به تولید (synthesize) قطعه دادههای (data chunk) ترکیبی مفقود (missing composite data chunks) نیست. همانطور که در مواردی مانندOSVDB-95632، CVE-2012-5470، CVE-2011-3328 و موارد ناشناخته ۱ تا ۴ مشاهده شد، Hercules قادر به تولید ورودیهایی که منجر به کرش میشوند برای آشکارسازی این آسیبپذیریها نیست، زیرا این موارد به وجود قطعه دادههای ترکیبی اختیاری (optional composite data chunks) وابسته هستند.
در آزمایشهای ما، Hercules در فرآیند ساخت این قطعه داده موردنیاز دچار بنبست (stuck) میشود. به طور خاص، به منظور آشکارسازی ۷ آسیبپذیری که در بنچمارک Hercules وجود ندارند، میبایست شرایط زیر برقرار باشد:
OSVDB-95632 (سرریز بافر – Buffer Overflow):
این آسیبپذیری نیازمند یک فایل PNG است که شامل یک قطعه داده (data chunk) اختیاری به نام tRNS میباشد؛ این قطعه داده میتواند یا مقادیر آلفا (alpha values) را که به ورودیهای پالت (palette entries) در تصاویر رنگبندی شده (indexed-color images) مرتبط هستند مشخص کند، یا یک رنگ شفاف واحد را برای تصاویر خاکستری (greyscale) و رنگی واقعی (truecolor) تعریف کند. علاوه بر این، مقدار یک فیلد داده در قطعه IHDR (قطعه هدر فایل PNG) یعنی عرض تصویر (image width) باید به گونهای باشد که بتواند یک سرریز عدد صحیح (integer overflow) را در پلاگین LibPNG مورد استفاده در VLC 2.0.7 ایجاد کند.
CVE-2012-5470 (سرریز بافر – Buffer Overflow):
این آسیبپذیری نیازمند یک فایل PNG است که شامل یک قطعه داده (data chunk) اختیاری به نام tEXt باشد؛ این قطعه برای ذخیره رشتههای متنی مرتبط با تصویر استفاده میشود، مانند توضیح تصویر (image description) یا اطلاعات حق نشر (copyright notice). علاوه بر این، طول (length) این قطعه داده (data chunk) باید به اندازهای بزرگ باشد که از ظرفیت بافر هیپ (heap) تخصیصیافته برای نگهداری دادههای تصویر فراتر برود و باعث سرریز بافر (buffer overflow) شود. با این حال، این مقدار نباید آنقدر بزرگ باشد که مانع از موفقیت LibPNG در تخصیص بافر هیپ (heap) موردنیاز برای ذخیره دادههای موجود در قطعه tEXt شود.
CVE-2011-3328 (تقسیم بر صفر – Divide-by-Zero):
این آسیبپذیری نیازمند یک فایل PNG است که شامل یک قطعه داده (data chunk) اختیاری به نام cHRM باشد. این قطعه، مختصات رنگی (chromaticities) مربوط به رنگهای پایه قرمز، سبز و آبی (red, green, blue primaries) در نمایش تصویر و همچنین نقطه سفید مرجع (white point) را مشخص میکند. در مرحله دوم، برخی از فیلدهای دادهای در قطعه cHRM باید دارای مقادیر خاصی باشند تا بتوانند یک خطای تقسیم بر صفر (divide-by-zero) را در کتابخانه LibPNG ایجاد کنند.
آسیب پذیریهای ناشناخته ۱-۳ (نقض دسترسی خواندن حافظه – Memory Read Access Violation):
این موارد نیازمند فایلهای PNG هستند که شامل قطعه دادههای (data chunk) اختیاری مانند iTXt، zTXt یا iCCP (بسته به مورد) بود و فاقد محتوا باشند. به عبارت دیگر، این قطعهها دارای اندازهای (size) برابر با صفر هستند و تنها شامل نام قطعه (chunk) و جمعآزما (checksum) میباشند، بدون آن که هیچ دادهای در بخش محتوایی آنها وجود داشته باشد.
آسیب پذیری ناشناخته ۴ (تقسیم بر صفر – Divide-by-Zero):
این مورد نیازمند یک فایل WAV است که در آن، قطعه قالب (format chunk) شامل یک فیلد دادهای مرکب (composite data field) اختیاری باشد. علاوه بر این، یک بایت مشخص در داخل این فیلد باید مقدار صفر داشته باشد تا خطای تقسیم بر صفر (divide-by-zero) در برنامه ایجاد شود.
برخلاف Hercules، ابزار MoWF ما از مدلهای ورودی (input models) برای پیوند(transplant) قطعههای داده مورد نیاز از سایر فایلها در مجموعه تست اولیه یا تولید خودکار قطعهها از روی مدل ورودی استفاده میکند. به همین علت، ابزار MoWF ما میتواند با موفقیت ورودیهای منجر به کرش را به عنوان شاهد (witness) برای هفت آسیبپذیری ذکرشده تولید کند.
از آنجا که MoWF توسعهای (extension) از Hercules است، میتواند هر شش آسیبپذیری موجود در بنچمارک Hercules را نیز با موفقیت بازتولید کند. همانطور که در پاسخ بهپرش پژوهشی سوم خواهیم دید، ابزار MoWF ما برای بازتولید سه مورد از این شش آسیبپذیری (CVE-2010-0718، CVE-2011-0502 و CVE-2010-0688) حتی به دانه ورودی (seed input) نیز نیاز ندارد، زیرا قادر است فایلهای (نیمه)معتبر را مستقیماً از مدلهای ورودی تولید کند.
پرسش پژوهشی ۲. مقایسه با فازینگ جعبه سیاه مبتنی بر مدل (Model-Based Blackbox Fuzzing)
فازر جعبه سیاه مبتنی بر مدل Peach قادر نیست حتی نیمی از آسیبپذیریهایی را که ابزار MoWF ما آنها را شناسایی میکند، کشف کند (به جدول ۳ مراجعه کنید). لازم به ذکر است که ما به صورت محافظهکارانه فرض کردهایم که قابلیتهای پیونددهی (transplantation) و نمونهسازی (instantiation) قطعههای داده (data chunk) در Peach وجود دارند، در حالی که واقعا این چنین نیست. همچنین باید توجه داشت که افزودن این قابلیتها به Peach میتواند چالشبرانگیز باشد. در واقع، یافتن قطعه مناسب برای پیونددهی و قرار دادن آن در موقعیت صحیح در دانه ورودی (seed input)، در یک تکنیک فازینگ بدون جهت (undirected) مانند Peach، با مشکل انفجار ترکیبی (combinatorial explosion) مواجه است. در مقابل، MoWF با استفاده از اطلاعات مربوط به IFهای کلیدی، فرآیند پیونددهی قطعههای داده را به صورت هدایت شده (directed) انجام میدهد.
ما در آزمایشها، توانایی Peach در انجام پیونددهی (transplantation) و نمونهسازی (instantiation) قطعههای داده را به صورت شبیهسازی شده پیادهسازی کردیم. به این صورت که مجموعهی ۱۰ دانه ورودی که هیچکدام شامل قطعههای داده مفقود نبودند را با حداقل یک دانه ورودی تکمیل کردیم که در آن، قطعههای داده مورد نظر را به صورت دستی پیونددهی (transplant) کرده بودیم.
در جدول ۳ نشان میدهیم که فازر Peach (با این قابلیت شبیهسازی شده) میتواند سه آسیبپذیری ناشناخته ۱-۳ را آشکار کند، زیرا این موارد تنها به وجود قطعههای داده اختیاری با دادهی خالی (empty-data optional chunks) نیازمند است.
با این حال، برای ۱۰ آسیبپذیری باقیمانده، ابزار MoBF یعنی فازر Peach حتی با وجود اینکه ورودیهایی شامل قطعه دادههای (data chunk) اختیاری مورد نیاز در اختیارش قرار دادهایم، نمیتواند ۷ مورد از این ۱۰ آسیبپذیری را با موفقیت آشکار کند. دلیل این موضوع، محدودیت این رویکرد در تولید مقادیر خاص (specific values) است. بهطور کلی، فازینگ جعبه سیاه قادر نیست مقادیر دقیقی را برای فیلدهای دادهای تولید کند که برای آشکارسازی آسیبپذیریهای عمیق (deep vulnerabilities) لازم هستند. به عنوان مثال، اگر یک فیلد دادهای از نوع عدد صحیح ۴ بایتی (4-byte integer) داشته باشیم، احتمال اینکه یک فازر جعبه سیاه از طریق جهش تصادفی (randomly mutate) به یک مقدار خاص X برسد، بسیار ناچیز است (فقط ۱ در 2³²). در مقابل، فازینگ جعبه سفید مبتنی بر اجرای نمادین (symbolic execution) در یافتن چنین مقادیر دقیقی بسیار توانمند است.
در همین حال، ابزار MoWF ما (با بهرهگیری از مدلهای ورودی) نسخه بهبود یافته TWF است و میتواند هم مشکل قطعه داده مفقود (missing data chunk) و هم محدودیت در تولید مقادیر ورودی خاص را برطرف کند. در نتیجه، میتواند با موفقیت موارد آزمایشی را برای افشای هر ۱۳ آسیبپذیری تولید کند.
پرسش پژوهشی ۳. حساسیت نسبت به مجموعه آزمون اولیه (Sensitivity to the Initial Test Suite)
جدول ۴: آسیبپذیریهایی که توسط ابزار MoWF ما در شرایطی که هیچ فایل دانه اولیهای (initial seed files) ارائه نشده است، آشکار شدهاند.
در این آزمایش، ابزار MoWF را بدون هیچگونه دانه ورودی اولیه (initial seed inputs) اجرا کردیم (مطابق جدول ۴). با بهرهگیری از مدلهای ورودی مربوط به قالبهای PNG ،MIDI و ORB، ابزار MoWF برای هر قالب فایل به صورت خودکار یک فایل دانه حداقلی (minimal seed file) تولید میکند. بهطور خاص یک فایل PNG حداقلی، یک تصویر ۱×۱ است که شامل چهار قطعه اجباریIHDR ، PLTE، IDAT و IEND میباشد. در مورد MIDI، این فایل یک فایل صوتی تک آهنگ (single track) است که شامل یک قطعه هدر MThd و یک قطعه آهنگ MTrk است. یک فایل ORB حداقلی شامل تمام ویژگیهای لازم برای رندر کردن یک شیء مداری (orbital object) است. پس از تولید این فایلها، ابزار MoWF را روی تمام برنامههای مورد آزمایش که در جدول ۴ فهرست شدهاند اجرا میکنیم.
نتایج آزمایشها نشان میدهند که با استفاده از فایلهای حداقلی (minimal files)، ابزار MoWF ما قادر است ۹ مورد از ۱۳ آسیبپذیری (آنهایی که از طریق فایلهای PNG، MIDI و ORB قابل شناسایی هستند) را همانگونه که در جدول ۳ گزارش شده است، کشف کند.
این بدان معناست که ابزار MoWF میتواند ۷۰٪ از آسیبپذیریها را بدون هیچگونه دانه ورودی اولیهای آشکار کند. این نتیجه نشان میدهد که تکنیک MoWF وابستگی فازینگ جعبه سفید سنتی (TWF) به دانههای اولیه انتخاب شده را به طور قابل توجهی کاهش میدهد.
ابزار MoWF در ۴ مورد از ۱۳ آسیبپذیری موفق به کشف آنها نشد، زیرا این موارد به فایلهایی با قالبهای WAV، FLV و PDF نیاز دارند. با این حال، مدلهای ما برای این فرمتها هنوز نسبتاً ناقص و خام (coarse) هستند. اگرچه این مدلها برای کار کردن MoWF با مجموعههای تست موجود کافی هستند، اما برای تولید مستقیم فایلهای (نیمه)معتبر باید کاملتر شوند.
از آنجا که این قالبهای فایل پیچیده هستند، از یک سو میتوان زمان بیشتری صرف مطالعه و درک کامل مشخصات (specifications) آنها کرد تا مدلهای ورودی را بهبود بخشید. از سوی دیگر، میتوان از مدلهای جامعتری که توسط شرکتهای نرمافزاری یا مالکان این قالبها توسعه داده شدهاند استفاده مجدد کرد.
به عنوان مثال، طبق مطلبی در وبلاگ رسمی Adobe Systems، توسعهدهندگان این شرکت مدل مربوط به فایل PDF (که تا سال ۲۰۰۸ یک قالب اختصاصی تحت کنترل Adobe بود) را پیادهسازی کرده و از فازر Peach به منظور فازینگ نرمافزار محبوب خود یعنی Adobe Reader استفاده نمودند. با در اختیار داشتن چنین مدلهای ورودی کامل یا نسبتاً کامل، رویکرد MoWF ما میتواند بهعنوان مکملی برای ابزارهای MoBF مانند فازر Peach عمل کند، تا بهرهبرداری از این مدلها را به حداکثر رسانده و در نتیجه آسیبپذیریهای بیشتری را آشکار سازد.
۶. تهدیدهای اعتبار (Threats to Validity)
مهمترین تهدید برای اعتبار بیرونی (external validity)، میزان تعمیمپذیری (generality) نتایج ما است. MoWF برای باینریهای برنامههایی که با ورودیهای پیچیده کار میکنند توسعه داده شده است. ما مجموعه متنوعی از برنامههای شناخته شده از حوزههای مختلف را انتخاب کردیم که مشخصات (specifications) قالب ورودی آنها در دسترس بود.
در حالی که برای نرمافزارهای اختصاصی (proprietary)، ممکن است این مشخصات قالب در دسترس نباشد، ما معتقدیم که تکنیکهای استنتاج دستور زبان (grammar inference) میتوانند ابزار قدرتمندی برای استخراج خودکار مدلهای ورودی باشند. نیمی از آسیبپذیریها از کارهای پیشین [22] انتخاب شدهاند. برای نشان دادن اثربخشی MoWF، نیمه دیگر بهگونهای انتخاب شدند که وجود یک قطعه داده (data chunk) اختیاری برای آشکارسازی آنها ضروری باشد.
مهمترین تهدید برای اعتبار داخلی (internal validity)، سوگیری انتخاب در تعیین دانه (seed) است (به جدول ۲ مراجعه کنید). ما ورودیهای دانه را یا به صورت تصادفی از یک بنچمارک انتخاب کردیم یا از اینترنت به دست آوردیم. با این حال، نتایج آزمایشهای ما نشان میدهد که وابستگی به دانههای موجود در رویکرد ما کاهش یافته است.
مهمترین تهدید برای اعتبار سازه (construct validity)، صحت پیادهسازی ابزار ما است. با این وجود، از آنجا که ابزار ما توسعهای از Hercules و Peach Fuzzer – دو مبنای اصلی ارزیابی ما – محسوب میشود، هرگونه خطا یا نادرستی موجود در این ابزارهای پایه میتواند به ابزار ما نیز منتقل شود.
۷. کارهای مرتبط (Related Work)
اولین تکنیک آزمون خودکار برای برنامههای پردازش فایل با نام FUZZ در سال ۱۹۹۰ توسط Miller و همکاران [21] برای بررسی میزان قابلیت اطمینان ابزارهای UNIX پیادهسازی شد. از آن زمان تاکنون، فازینگ (fuzzing) به میزان قابل توجهی توسعه یافته، به طور گسترده مورد استفاده قرار گرفته و آسیبپذیریهای جدی در بسیاری از نرمافزارهای مهم را آشکار کرده است.
یک فازر به سرعت حجم زیادی از ورودیهای برنامه را به منظور کرش کردن آن برنامه تولید میکند. امروزه، اکثر کامپایلرها از تزریق به اصطلاح سنیتایزرها (sanitizerها) هنگام کامپایل برنامه تحت آزمون پشتیبانی میکنند. یک سنیتایزر یک اوراکل خودکار (automated oracle) است که میتواند باگهای پیچیدهتر و جدیتر نرمافزاری مانند سرریز بافر (buffer overflow)، رقابت داده (data race) و خطاهای حافظه (memory errors) را شناسایی کند.
فازرها و سنیتایزرها در کنار هم، امکان تست خودکار و آشکارسازی باگهای عمیق و پیچیده در برنامههایی با هر مقیاس را فراهم میکنند. برنامههای حساس از نظر امنیتی در یک حلقه بازخوردی (feedback loop) سختسازی (hardened) میشوند؛ به این صورت که ابتدا برنامه با سنیتایزر تجهیز میشود، سپس فاز میگردد، خطاهای کشف شده اصلاح میشوند، نسخه اصلاح شده مجددا فاز میگردد و این چرخه ادامه پیدا میکند.
میتوان بین دو دسته تکنیک تمایز قائل شد: تکنیکهای جعبه سیاه (blackbox) که کارآمدتر هستند و بدون تحلیل کد منبع برنامه، ورودیهای تست را تولید میکنند، و تکنیکهای جعبه سفید (whitebox) که مؤثرتر هستند و از تحلیل برنامه استفاده میکنند تا باگهایی را آشکار کنند که در لایههای عمیقتر کد پنهان شدهاند.
فازینگ جعبهسیاه (Blackbox Fuzzing) [3, 5, 6, 7, 21]. برنامههایی که ورودیهای متنی ساده و با ساختار کمتر پیچیده را پردازش میکنند، میتوانند با مولدهای ورودی تصادفی مانندFUZZ [21] ، فاز شوند. در واقع، تولید تصادفی آزمون میتواند یک تکنیک بسیار کارآمد برای تولید آزمون باشد [9].
با این حال، برای برنامههایی که فایلهای ورودی با ساختار بسیار پیچیده را پردازش میکنند (مانند یک PDF Reader )، اغلب فایلهای تصادفی به عنوان ورودی نامعتبر رد میشوند. به همین دلیل، ابزارهای فازینگ جعبه سیاه مبتنی بر مدل (Model-based Blackbox Fuzzing – MoBF) از یک مدل ورودی ارائه شده توسط کاربر استفاده میکنند تا فایلهای تصادفی اما معتبر تولید کنند [3, 5, 6, 7]. با این وجود، به دلیل انتخاب تصادفی مقادیر برای فیلدهای داده، MoBF ممکن است همچنان در آشکارسازی خطاهای عمیقتر در عملکرد برنامه ناکارآمد باشد. در مقابل، بررسی سیستماتیک مسیرها (systematic path exploration) برای شمارش و بررسی مقادیر خاص یک فیلد داده، بهمراتب مؤثرتر است.
فازینگ جعبه سفید سنتی (Traditional Whitebox Fuzzing) [15, 22, 13, 26]. این نوع فازینگ با جایگزینی بایتهای ورودی در یک فایل مشخص با مقادیر دیگر، به دنبال کشف مسیرهای جایگزین در برنامه است. فازینگ جعبه سفید مبتنی بر آلودگی (taint-based whitebox fuzzing) [13, 26] آن دسته از «بایتهای حساس» (hot bytes) را در فایل ورودی شناسایی میکند که بر مقدار یک موقعیت خطرناک (dangerous location) مانند مقسومعلیه (divisor) یا فراخوانی سیستم (system call) تأثیر میگذارند. فازینگ این بایتهای حساس میتواند خطاها را سریعتر آشکار کند.
فازرهای جعبه سفید مبتنی بر اجرای نمادین (symbolic execution-based whitebox fuzzers) پیشرفتهتر، بایتهای ورودی مؤثر بر نتیجه یک شاخه (branch) را با متغیرهای نمادین (symbolic variables) جایگزین کرده و از اجرای نمادین [15, 22] برای نقض (negate) آن شاخهها استفاده میکنند.
فازینگ جعبه سفید آگاه از جمعآزما (checksum) [26] تلاش میکند بررسیهای جمعآزما را شناسایی کرده و در حین فازینگ، آنها را دور بزند. این بررسی معمولاً به صورت اولین گزاره شرطی (if-statement) s شناسایی میشود که به تعداد زیادی از بایتهای ورودی وابسته است. سپس این شرط با حذف s از برنامه دور زده میشود. برای تعمیر فایلهای ناقص تولید شده، شرط شاخهای s برحسب بایتهای ورودی نمادین محاسبه میشود.
با این حال، فازینگ جعبه سفید آگاه از جمعآزما (checksum) نمیتواند سایر محدودیتهای یکپارچگی (integrity constraints) مانند اندازه قطعه (chunk size) یا آفست (offset) را حل کند. ما در سراسر مقاله، محدودیتهای فازینگ جعبه سفید سنتی از جمله گرفتار شدن در فضای جستجوی بسیار بزرگ ورودیهای نامعتبر و وابستگی به فایلهای دانه (seed files) را نشان دادهایم.
در مقابل، فازینگ جعبه سفید مبتنی بر دستور زبان (Grammar-based Whitebox Fuzzing – GWF) [14] ورودیهایی تولید میکند که نسبت به یک گرامر مستقل از متن (context-free grammar) به نام G معتبر هستند. برای توضیح، از مثال موجود در لیست ۴ استفاده میکنیم.
لیست ۴: تابع ()isSorted در صورتی مقدار true بازمیگرداند که ورودی آن یک لیست مرتب از اعداد تکرقمی باشد:
int i;
char* input;
char getNextToken() {
return input[i++];
}
bool isSorted() {
int prev_digit = 0;
if (’{’ == getNextToken()) {
do {
char token = getNextToken();
if (’,’ == token) continue;
if (’}’ == token) return true;
int digit = asInt(token);
if (prev_digit > digit) return false;
prev_digit = digit;
} while (true);
}
return false;
}
دستور زبان مستقل از متن (G) را میتوان به صورت زیر نوشت:
این گرامر بیان میکند که ورودیهای معتبر با یک آکولاد باز آغاز میشوند و به دنبال آن لیستی از (حداقل یک) رقم جدا شده با ویرگول و یک براکت آکولاد قرار میگیرد. فازینگ جعبه سفید مبتنی بر دستور زبان (GWF) یک شرط مسیر (path condition) را به صورت یک عبارت منظم کدگذاری میکند. GWF برای ورودی {1,2}، محدودیت زیر را تولید میکند تا شاخهی جایگزین (alternative branch) را بررسی کند؛ یعنی حالتی که ورودی با آکولاد بسته تمام نمیشود:
که در آن Digit یک متغیر نمادین (symbolic variable) است. با استفاده از یک حلکننده محدودیت مستقل از متن (context-free constraint solver)، میتوان یک آرایه شامل سه رقم به دست آورد که هم توسط گرامر (G) و هم توسط محدودیت (R) پذیرفته میشود (برای مثال {0,0,0}).
با این حال، از آنجا که عبارت منظم نمیتواند رابطه حسابی بین token2 و token4 را بیان کند (یعنی شرطهایی مانند 1<2)، ممکن است یک مسیر کاملاً متفاوت در برنامه طی شود. این موضوع باعث میشود GWF هم نادرست (unsound) و هم ناقص (incomplete) باشد. در مقابل، MoWF شرایط مسیر (path conditions) را به صورت فرمولهای SMT نگه میدارد و تنها مسیرهایی را هرس (prune) میکند که توسط ورودیهای نامعتبر نسبت به مدل ورودی طی میشوند.
علاوه بر این، زبان مستقل از متن که قالب فایل را توصیف میکند، قادر به بیان محدودیتهای یکپارچگی (integrity constraints) مانند جمعآزما (checksum) یا اندازهء (size) یک قطعه داده (data chunk) نیست. همچنین توابعی که روی دادههای داخل فیلدها اعمال میشوند، مانند الگوریتمهای فشردهسازی، نیز قابل بیان نیستند. مدلهای ورودی ما این امکان را فراهم میکنند که قیود یکپارچگی و الگوریتمهای فشردهسازی از طریق مفاهیمی مانند اصلاح (Fixup) و تبدیلکننده (Transformer) مشخص شوند.
فازینگ هیبریدی (Hybrid Fuzzing). Driller [23]، کارایی فازینگ جعبه سفید و بهرهوری فازینگ جعبه سیاه را با هم ترکیب میکند. در این روش، ابتدا فازر جعبه سیاه برای مدتی اجرا میشود و سپس فازر جعبه سفید روی «مؤثرترین» یا امیدوارکنندهترین دانههایی (seed) که توسط فازر جعبه سیاه تولید شدهاند اعمال میگردد. Driller برخلاف MoWF، از اطلاعات یک مدل ورودی (input model) برای تولید فایلهای معتبرتر استفاده نمیکند. همچنین Driller به طور خاص برای برنامههایی که ورودیهای بسیار ساختیافته (highly structured inputs) را پردازش میکنند طراحی نشده است. از این نظر، رویکرد ما نسبت به Driller متعامد (orthogonal) محسوب میشود. در واقع، Driller میتواند هنگام آزمایش برنامههایی که ورودیهای بسیار ساختیافته (structured inputs) را پردازش میکنند، از MoWF بهرهمند شود.
۸. بحث (Discussion)
ما تکنیک فازینگ جعبه سفید مبتنی بر مدل (Model-based Whitebox Fuzzing – MoWF) را به عنوان یک روش تست خودکار برای باینریهای برنامههایی معرفی کردیم که با ورودیهای بسیار ساختیافته (highly structured inputs) کار میکنند. مشاهده کردهایم که برخی شاخهها (branches) در یک برنامه پردازش فایل تنها در شرایط خاصی اجرا میشوند؛ از جمله: (۱) وجود یک قطعه داده (data chunk) خاص،
(۲) مقدار مشخصی از یک فیلد داده در یک قطعه داده (data chunk)،
(۳) یا صحت و یکپارچگی (integrity) قطعه دادهها.
از این رو، ما ابزار Hercules را که یک تکنیک فازینگ جعبه سفید سنتی موجود است توسعه دادهایم، بهگونهای که نهتنها بتواند مقادیر خاص فیلدها را تنظیم کند، بلکه بتواند یک قطعه دادههای کامل را اضافه یا حذف کند و در عین حال یکپارچگی آنها را در حین فازینگ مجددا برقرار سازد.
هرس کردن مسیرهای نامعتبر (Pruning Invalid Paths). ما چندین رویکرد را برای هرس کردن فضای جستجوی بسیار بزرگ ورودیهای نامعتبر بررسی کردیم، از جمله اعمال محدودیتهای یکپارچگی (integrity enforcement) و همچنین پیونددهی (transplantation) و ایجاد (instantiation) قطعههای داده (data chunk). برخلاف فازینگ جعبه سفید سنتی (TWF)، ابزار MoWF قادر است شاخههایی را که تنها در حضور قطعه دادههای خاص فعال میشوند، نفی (negate) کند، بدون اینکه نیاز باشد بهصورت تکراری با کاوش کد تجزیهگر (parser)، آن قطعه داده را از ابتدا بسازد. تمام ورودیهای تولید شده معتبر هستند، به این معنا که با مدل ورودی (input model) سازگارند و محدودیتهای یکپارچگی نیز در آنها رعایت میشود. ابزار MoWF ما با در نظر گرفتن محدودیت زمانی ۲۴ ساعته، موفق گردید هر ۱۳ آسیبپذیری موجود در برنامههای آزمایشی را کشف کند، در حالی که ابزار TWF تنها ۶ مورد از آنها را شناسایی کرد.
کاهش وابستگی به دانه (Reduced Seed Dependence). ما همچنین وابستگی MoWF به فایلهای دانه اولیه (initial seed files) را بررسی کردیم. ابزار MoWF میتواند فایلهای دانه اولیه را مستقیماً از مدل ورودی ارائه شده (input model) نمونهسازی کند. علاوه بر این، اگر یک دانه ورودی برای رسیدن به یک هدف مشخص (target location) فاقد یک قطعه داده (data chunk) باشد، MoWF میتواند از سایر فایلهای دانه به عنوان اهدا کننده (donor) استفاده کند، قطعه داده مفقود را از آنها منتقل (transplant) کند و یک دانه جدید بسازد که به موقعیت هدف نزدیکتر است. در صورتی که هیچ اهدا کنندهای در دسترس نباشد، قطعه داده مورد نیاز مستقیماً از مدل ورودی نمونهسازی و تولید میشود. در مجموع، از ۱۳ آسیبپذیری موجود در موضوعات آزمایشی ما، ابزار MoWF موفق شد ۹ مورد را بدون استفاده از هیچگونه دانه اولیهای کشف کند.
بطور خلاصه، MoWF یک تکنیک فازینگ امیدوارکننده برای باینریهای برنامهای است که ورودیهای بسیار ساختیافته را پردازش میکنند. این روش خصوصا زمانی مفید است که هیچ فایل دانه اولیهای در دسترس نباشد که شامل قطعههای داده اختیاری موردنیاز باشد. MoWF با داشتن همان بودجه زمانی، میتواند تعداد بیشتری ورودی معتبر تولید کند؛ و این موضوع به آشکارسازی آسیبپذیریهایی کمک میکند که در غیر این صورت قابل کشف نبودند.
۹. قدردانی (Acknowledgments)
از کمکهای لاو ون یونگ (Law Wen Yong) در پیادهسازی این پروژه سپاسگزاریم. این پژوهش تا حدودی توسط کمک مالی آزمایشگاههای ملی DSO سنگاپور و بنیاد ملی تحقیقات دفتر نخستوزیری سنگاپور، تحت برنامه ملی تحقیق و توسعه امنیت سایبری (پروژه TSUNAMi، شماره جایزه NRF2014NCR-NCR001-21) پشتیبانی شده و توسط اداره ملی تحقیق و توسعه امنیت سایبری اداره میشود.
منابع
[1] Specification of the DEFLATE Compression Algorithm. https://tools.ietf.org/html/rfc1951. Accessed: 2016-02-13.
[2] Tool: IDA multi-processor disassembler and debugger. https://www.hex-rays.com/products/ida/. Accessed: 2016-04-04.
[3] Tool: Peach Fuzzer Platform. http://www.peachfuzzer.com/products/peach-platform/.Accessed: 2016-01-23.
[4] Tool: Peach Fuzzer Platform (Input Model). http://community.peachfuzzer.com/v3/DataModeling.html. Accessed: 2016-01-23.
[5] Tool: SPIKE Fuzzer Platform. http://www.immunitysec.com. Accessed: 2016-01-23.
[6] Tool: Suley Fuzzer. https://github.com/OpenRCE/sulley. Accessed: 2016-01-23.
[7] G. Banks, M. Cova, V. Felmetsger, K. Almeroth, R. Kemmerer, and G. Vigna. Snooze: Toward a stateful network protocol fuzzer. In Proceedings of the 9th International Conference on Information Security, ISC’06, pages 343–358, 2006.
[8] N. Bjorner and A.-D. Phan. vz - maximal satisfaction with z3. In T. Kutsia and A. Voronkov, editors, SCSS 2014. 6th International Symposium on Symbolic Computation in Software Science, volume 30 of EPiC Series in Computing, pages 1–9, 2014.
[9] M. Böhme and S. Paul. On the efficiency of automated testing. In Proceedings of the 22Nd ACM SIGSOFT International Symposium on Foundations of Software Engineering, FSE 2014, pages 632–642, 2014.
[10] C. Cadar, D. Dunbar, and D. Engler. Klee: Unassisted and automatic generation of high-coverage tests for complex systems programs. In Proceedings of the 8th USENIX Conference on Operating Systems Design and Implementation, OSDI’08, pages 209–224, 2008.
[11] V. Chipounov, V. Kuznetsov, and G. Candea. S2e: A platform for in-vivo multi-path analysis of software systems. In Proceedings of the Sixteenth International Conference on Architectural Support for Programming Languages and Operating Systems, ASPLOS XVI, pages 265–278, 2011.
[12] L. De Moura and N. Bjørner. Z3: An efficient smt solver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’08/ETAPS’08, pages 337–340, 2008.
[13] V. Ganesh, T. Leek, and M. Rinard. Taint-based directed whitebox fuzzing. In Proceedings of the 31st International Conference on Software Engineering, ICSE ’09, pages 474–484, 2009.
[14] P. Godefroid, A. Kiezun, and M. Y. Levin. Grammar-based whitebox fuzzing. In Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’08, pages 206–215, 2008.
