return 0;
}
با تحلیل معمولی میفهمیم برنامه چند شرط داره
ولی Symbolic Execution میتونه شرطهای لازم برای رسیدن به مسیر موفق رو استخراج کنه
value >= 100
AND
value <= 200
AND
value == 150
در نتیجه
value = 150
یک جواب معتبره
این قابلیت در Reverse Engineering کاربردهای مهمی داره
تحلیل منطق اعتبارسنجی
پیدا کردن ورودی های لازم برای رسیدن به یک مسیر مشخص
بررسی شرطهای پیچیده داخل باینری
تحلیل مسیر های منتهی به Crash
و بررسی اینکه چه محدودیت هایی باعث میشن یک مسیر قابل دسترسی یا غیرقابل دسترسی باشه
البته در باینری واقعی ممکنه شرط‌ها به چند تابع مختلف وابسته باشن یا تحت تأثیر حافظه و وضعیت Runtime قرار بگیرن
در این شرایط ساختن مدل دقیق برنامه سخت‌تر میشه
تفاوت Symbolic و Concrete Execution
این تفاوت رو خوب یاد بگیرید
Concrete Execution
برنامه با مقدار واقعی اجرا میشه
x = 15
در این حالت پردازش برنامه بر اساس مقدار واقعی
15 انجام میشهSymbolic Execution
به جای مقدار واقعی از یک مقدار نمادین استفاده میکنیم
x = X
وقت رسیدن به شرط ها محدودیت هایی روی
X ساخته میشنمقایسه ساده
یک نکته مهم
Symbolic Execution
تضمین نمیکنه تمام مسیرهای برنامه رو بررسی کنه
حلقه‌ها و تعداد زیاد شاخه ها میتونن باعث ترکیدن مسیرها بشن😁
محاسبات پیچیده و تعامل با سیستم عامل یا کتابخونه های خارجی هم ممکنه تحلیل رو دشوار کنن
پس حتی Symbolic Execution هم محدودیت‌های خودش رو داره
ارتباط با Fuzzing
اینجا Symbolic Execution به یکی از کاربردهای جذابش میرسه
فرض کنید Fuzzer یک ورودی تولید کرده و برنامه رو اجرا کرده
Input
↓
Program
↓
Branch A
↓
Branch B
↓
Crash
حالا میخوایم مسیر جدیدی رو بررسی کنیم که به خاطر برقرار نشدن یک شرط بهش نرسیدیم
مثلا برنامه چنین شرطی داره
Javascript
if (x == 1337)
dangerous_function();
اگر ورودی فعلی ما این باشه
x = 10
برنامه وارد
dangerous_function نمیشهSymbolic Execution
میتونه شرط شاخه رو استخراج کنه
X == 1337
بعد حل کننده یک مقدار معتبر پیشنهاد میده
X = 1337
این مقدار رو میشه به عنوان ورودی جدید در فرآیند تست استفاده کرد
پس ارتباط کلی میشه
Fuzzer
↓
Input
↓
Program Execution
↓
Uncovered Branch
↓
Path Constraint
↓
SMT Solver
↓
New Input
↓
Fuzzing Again
این ایده در روش‌هایی مثل Concolic Execution هم استفاده میشه
در Concolic Execution برنامه با ورودی های واقعی اجرا میشه ولی همزمان مقادیر و شرط‌ها به شکل نمادین هم دنبال میشن به این ترتیب اجرای واقعی و تحلیل نمادین در کنار هم قرار میگیرن
ابزارهای کاربردی
برای آشنایی عملی با این مبحث چند ابزار ارزش بررسی دارن
angr
یک Framework برای تحلیل باینری که قابلیت‌هایی مثل Symbolic Execution و تحلیل مسیر داره
مخزن رسمی:
https://github.com/angr/angr
Triton
یک Framework برای Dynamic Binary Analysis که قابلیت‌هایی مثل Taint Analysis و Symbolic Execution ارائه میده
مخزن رسمی:
https://github.com/JonathanSalwan/Triton
Z3
یک SMT Solver که میتونه محدودیت‌های نمادین رو حل کنه
مخزن رسمی:
https://github.com/Z3Prover/z3
این ابزارها دقیقا یک کار رو انجام نمیدن
angr
بیشتر برای ساختن و تحلیل مسیرهای نمادین در باینری کاربرد داره
Triton
قابلیت‌های تحلیل پویای باینری و محاسبات نمادین رو فراهم میکنه
Z3
هم حل کننده محدودیت هاست و به تنهایی یک ابزار کامل برای تحلیل مسیرهای اجرایی باینری محسوب نمیشه
مسیر کلی
Symbolic Execution این شکلیه
Symbolic Input
↓
Program Analysis
↓
Branch Conditions
↓
Path Constraints
↓
SMT Solver
↓
Possible Input
در قسمت‌های قبلی یاد گرفتیم داده از کجا وارد برنامه میشه و چطور در Register ها و Memory حرکت میکنه
حالا یاد گرفتیم چطور شرطهای اجرای برنامه رو تحلیل کنیم تا بفهمیم چه ورودی هایی میتونن به یک مسیر خاص برسن
وقتی این مفاهیم رو کنار هم قرار بدیم
Fuzzing
↓
Interesting Input
↓
Dynamic Taint Analysis
↓
Data Flow
↓
Symbolic Execution
↓
Path Constraints
↓
New Input
↓
Crash Analysis
↓
Root Cause
دیگه فقط به اجرای برنامه و دیدن Crash اکتفا نمیکنیم میتونیم مسیر داده رو دنبال کنیم شرطهای لازم رو بفهمیم و برای بررسی مسیر های جدید ورودی های هدفمند تری بسازیم
@reverseengine
