قسمت سی و چهارم بافر اورفلو

Symbolic Execution

از ورودی واقعی تا ورودی نماد ها

تا اینجا یاد گرفتیم چطور داده رو داخل برنامه دنبال کنیم و بفهمیم چطور به یک Crash میرسه

حالا میخوایم یک قدم جلوتر بریم
فرض کنید یک برنامه شرطی داره که فقط وقتی ورودی مقدار خاصی داشته باشه وارد یک مسیر مشخص میشه
میتونیم هزاران ورودی مختلف امتحان کنیم تا بالاخره به اون مسیر برسیم
ولی راه بهتری هم وجود داره
به جای اینکه فقط مقدارهای واقعی رو امتحان کنیم میتونیم از Symbolic Execution استفاده کنیم تا بفهمیم چه شرط‌ هایی باید برقرار باشن تا برنامه وارد مسیر موردنظر بشه

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

ایده اصلی چیه

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

int check(int x)
{
if (x == 1337)
return 1;

return 0;
}

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

x = 10

برنامه شرط رو بررسی میکنه

10 == 1337

نتیجه غلطه و برنامه وارد مسیر دوم میشه
حالا فرض کن به جای مقدار واقعی از یک مقدار نمادین استفاده کنیم

x = X

در این حالت شرط برنامه میشه

X == 1337

حل‌ کننده می‌تونه نتیجه بگیره که برای ورود به مسیر اول باید مقدار X برابر 1337 باشه
پس به جای امتحان کردن مقدارهای مختلف می‌تونیم شرط لازم برای رسیدن به مسیر رو به دست بیاریم

Path Constraint
فرض کنید این کد رو داریم
C

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

return 0;
}

برای رسیدن به return 1 باید هر دو شرط برقرار باشن


x > 10
AND
x < 20

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

Path Constraint
پس محدودیت مسیر موردنظر اینه

10 < x < 20

چون x از نوع int هست جواب‌های ممکن شامل این مقدارها میشن

11, 12, 13, 14, 15, 16, 17, 18, 19

حل‌ کننده میتونه یکی از جواب‌های معتبر رو پیدا کنه

مثلا:

x = 15

نکته مهم اینه که Symbolic Execution فقط شرط فعلی رو در نظر نمیگیره
بلکه شرط‌های قبلی مسیر رو هم نگه میداره
چون برای رسیدن به یک نقطه از برنامه باید تمام شرط‌های لازم در مسیر برقرار باشن

وقتی مسیرها چند شاخه میشن

این برنامه رو ببینید
C

int process(int x)
{
if (x > 10)
return 1;

if (x == 5)
return 2;

return 0;
}

از دید Symbolic Execution میتونیم مسیرهای مختلف برنامه رو بررسی کنیم


x = X
|
x > 10 ?
/ \
Yes No
| |
return 1 x == 5 ?
/ \
Yes No
| |
return 2 return 0

حالا فرض کنید میخوایم به return 2 برسیم

اول باید شرط اول برقرار نباشه

X <= 10

بعد باید شرط دوم برقرار باشه

X == 5

پس Path Constraint ما میشه

X <= 10
AND
X == 5

در نتیجه

X = 5

یک ورودی معتبر برای رسیدن به این مسیر محسوب میشه
این همون ایده اصلی Symbolic Execution هست

برنامه رو دنبال میکنیم و برای هر مسیر شرط‌های لازم رو جمع می‌کنیم

نقش SMT Solver

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

اینجا از ابزاری به اسم
SMT Solver
استفاده میکنیم

یکی از ابزارهای شناخته‌شده در این زمینه

Z3
هست که توسط Microsoft Research توسعه داده شده

فرض کنید شرط‌های ما اینا باشن

X > 10
X < 20
X != 15

حل‌ کننده باید مقداری پیدا کنه که تموم شرط‌ ها رو همزمان برقرار کنه

مثلا:

X = 11


این مقدار معتبره چون هر سه شرط رو برقرار میکنه

ولی اگر شرطها این باشن


X > 20
X < 10

هیچ مقدار حقیقی نمی‌تونه هر دو شرط رو همزمان برقرار کنه

در نتیجه مسئله
Unsatisfiable
هست
یعنی جواب معتبری وجود نداره
در مقابل اگر حداقل یک جواب وجود داشته باشه مسئله

Satisfiable
محسوب میشه
البته SMT Solver فقط برای شرطهای ساده عددی نیست

بسته به منطق و قابلیت‌ های حل‌ کننده میتونه محدودیت‌های مربوط به Bit Vectorها و عملیات بیتی رو هم بررسی کنه

این موضوع برای تحلیل باینری‌ ها خیلی مهمه چون پردازنده با مقدارهایی با اندازه مشخص مثل 8 و 32 و 64 بیت کار میکنه و رفتار اون‌ها همیشه مثل اعداد صحیح ریاضی نیست

ارتباط Symbolic Execution با Reverse Engineering

فرض کنید یک باینری دارید و داخلش چنین منطقی وجود داره

C++

int validate(int value)
{
if (value < 100)
return 0;

if (value > 200)
return 0;

if (value == 150)
return 1;