قسمت سی و پنجم بافر اورفلو

Concolic Execution

ترکیب اجرای واقعی و نمادین برای کشف مسیرهای جدید



Concolic Execution
ترکیبی از دو روشه:

Concrete Execution:
اجرای برنامه با ورودی واقعی

Symbolic Execution:
بررسی نمادین داده‌ ها و شرط‌ های مسیر اجرا

هدف اینه که از یک اجرای واقعی شروع کنیم شرط‌ هایی رو که برنامه طی کرده استخراج کنیم و ورودی‌ های جدیدی بسازیم تا مسیر های دیگه هم بررسی بشن

یک مثال ساده

فرض کنید برنامه اینه:

int check(int x)
{
if (x > 10)
{
if (x < 20)
return 1;
}

return 0;
}

برنامه رو با این ورودی اجرا میکنیم:

x = 5

چون شرط "x > 10" برقرار نیست برنامه مستقیما به "return 0" میرسه

مسیر اجرا:

x = 5
|
x > 10 ?
|
False
|
return 0

تا اینجا فقط یک مسیر رو بررسی کردیم

اما Concolic Execution میتونه از همین اجرا برای پیدا کردن ورودی جدید استفاده کنه

استخراج شرط مسیر

در اجرای بالا شرط زیر بررسی شده:

if (x > 10)

مقدار واقعی "x" برابر 5 بوده پس شرط غلط شده

محدودیت نمادین مسیر طی‌ شده اینه:

x <= 10

حالا برای بررسی شاخه‌ی مخالف این شرط رو در نظر میگیریم:

x > 10

حل‌کننده‌ی محدودیت‌ها مثل SMT Solver میتونه یک مقدار مناسب پیشنهاد بده:

x = 15

با اجرای مجدد برنامه:

x = 15
|
x > 10 ?
|
True
|
x < 20 ?

این بار به شرط دوم رسیدیم مسیری که اجرای قبلی بهش نرسیده بودیم

ساخت ورودی جدید برای مسیر بعدی

شرط دوم اینه:

if (x < 20)

برای ورودی 15 این شرط هم برقرار میشه و برنامه به این بخش میرسه:

return 1;

محدودیت‌های مسیر موفق این برنامه عبارت‌اند از:

x > 10
AND
x < 20

یعنی:

10 < x < 20

پس "x = 15" یک ورودی معتبر برای رسیدن به این مسیر محسوب میشه

نکته‌ی مهم اینه که ورودی جدید صرفا تصادفی انتخاب نشده بلکه با استفاده از شرط‌ های مسیر ساخته شده

در عمل ابزار میتونه مسیرهای اجراشده رو ثبت کنه و با تغییر یکی از شرط‌ها ورودی جدیدی برای رسیدن به شاخه‌ ی متفاوت بسازه

الگوریتم کلی Concolic Execution

اجرای برنامه

برنامه با یک ورودی واقعی اجرا میشه

ثبت شرط‌های مسیر

ابزار شرط‌ های شاخه‌ هایی رو که برنامه ازشون عبور کرده ثبت میکنه به این شرط‌ ها "Path Constraints" گفته میشه.
تغییر یک شرط مسیر

یکی از شرط‌ ها رو برای بررسی شاخه‌ی مخالف تغییر میده در حالی که شرط‌ های قبلی مسیر رو هم در نظر میگیره

حل محدودیت‌ها

یک "SMT Solver" تلاش میکنه ورودی‌ ای پیدا کنه که شرط‌ های جدید رو برآورده کنه

اجرای مجدد با ورودی جدید

برنامه با ورودی به‌دست‌ اومده دوباره اجرا میشه تا مسیر متفاوتی بررسی بشه

این چرخه میتونه بارها تکرار بشه تا مسیرهای بیشتری پوشش داده بشن

ارتباط Concolic Execution با Fuzzing

در Fuzzing معمولی ورودی‌ ها اغلب با جهش یا تغییر ورودی‌ های قبلی ساخته میشن

مثلا:

Input A
↓
Mutation
↓
Input B
↓
New Execution

اما بعضی وقتا برنامه شرطی داره که رسیدن به شاخه‌ی موردنظر رو دشوار میکنه

مثلا:

if (input[0] == 'R' &&
input[1] == 'E' &&
input[2] == 'V')
{
process_special_case();
}

Fuzzer
باید ورودی‌ ای پیدا کنه که هر سه شرط رو برقرار کنه

Concolic Execution
میتونه شرط‌ های بررسی‌ شده رو تحلیل کنه و برای عبور از شاخه‌ ها ورودی مناسب پیشنهاد بده

Input
↓
Execution
↓
Path Constraints
↓
Solver
↓
New Input
↓
New Path

این ایده در Concolic Testing و بعضی روش‌های هدایت هوشمند ورودی در تست نرم‌افزار کاربرد داره

البته Fuzzer های مدرن هم میتونن از تکنیک‌هایی مثل "Coverage-Guided Fuzzing" استفاده کنن و بدون حل نمادین شرط‌ ها با جهش‌ های هدفمند به مسیرهای جدید برسن

محدودیت‌ های این روش

Concolic Execution
جادو نیست هرچند اسمش طوریه که انگار قراره برنامه خودش رو برای ما توضیح بده

چند مشکل مهم داره:

Path Explosion:
تعداد مسیرهای ممکن میتونه به‌سرعت زیاد بشه

محدودیت حل‌ کننده:
بعضی شرط‌ ها مخصوصا محاسبات پیچیده یا عملیات پشتیبانی‌ نشده ممکنه سخت حل بشن

وابستگی به اجرا:
تحلیل معمولا از مسیر هایی شروع میشه که با ورودی‌ های اولیه اجرا شدن برای رسیدن به مسیرهای دیگه باید ورودی‌های مناسبی تولید بشن

محیط اجرا:
تعامل با فایل شبکه سیستم‌ عامل یا کد خارجی میتونه تحلیل رو پیچیده‌تر کنه

به همین دلیل این روش معمولا در کنار Fuzzing و Static Analysis استفاده میشه نه به‌عنوان جایگزین کامل اون‌ها

تفاوت سه روش