Z3 easy_challenge

זהו מאמר שלישי בסדרת המאמרים Z3 למאמר השני, למאמר הראשון

במאמר הקודם נתתי לכם אתגר הנדסה לאחור: להורדת של האתגר

באתגר היה לכם קובץ פשוט שמבקש שם משתמש וסיסמא, עליכם למצוא את שם המשתמש והסיסמא, מה שנראה כך:

טרם הצפייה בפתרון שלי לאתגר אני מאוד ממליץ לכם לנסות ולפתור אותו בעצמכם.

בסרטון הבא הצגתי כיצד ניתן לפתור את האתגר באמצעות IDA + OllyDbg ולבסוף כיצד ניתן לפתור את האתגר גם באמצעות Z3 שזה בעצם נושא המאמר.

לסרטון:

בסרטון השתמשתי ב-OllyDbg שהגדרתי והוספתי לו את כל התוספים השימושיים ביותר, במידה והינכם מעוניין ב-OllyDbg שהגדרתי אתם מוזמנים להוריד אותו ישירות מה-Github שלי:

https://github.com/romanzaikin/OllyDbg-v1.10-With-Best-Plugins-And-Immunity-Debugger-theme-

במאמר זה לא אתייחס להנדסה לאחור של האתגר אלא יותר לפתרון האתגר באמצעות Z3, את ההנדסה לאחור אתם יכולים לראות בסרטון.

אנו נתחיל בפתיחת האתגר ב-IDA מה שיראה כך:

כדי לאתר את הקוד המרכזי של התוכנה אפשר פשוט להשתמש ב shift+f12 ולחפש את הטקסט המודפס על המסך "username" כך:

נלחץ על הטקסט פעמיים ונעבור לאזור הזיכרון שבו הוא מוגדר בתוך ה-data section:

אגב באזור הזה ניתן למצוא גם את שם המשתמש של התוכנה שהינו "root", נלחץ בשורה של username ואז נלחץ על "x" ,כך נפתח את חלון ה-xref:

לחצו על ok ותגיעו לקוד של התוכנה:

כעת לחצו על F5 מה שיבצע hexrays על הקוד:

ניתן לראות שכמות התווים שעלינו להזין צריכה להיות קטנה או שווה ל 0xb ולאחר מכן עלינו להזין תווים לסיסמא שיהיו שווים ל-[dword_41A900[i שהוא מכיל את הרשימה הבאה:

נעתיק את הרשימה:
data = [0x2121, 0x3568, 0x33F6, 0x2c6c, 0x2857,0x24f0,0x30a0,0x12cd,0x14c1,0x18f0,0x1AD8]

ונפתור את התרגיל באמצעות z3.

תחילה עלינו להגדיר את המשתנים שלנו שכל אחד מהם בעצם יהווה תו אחד מהסיסמא, על מנת לעשות זאת אנו יכולים להגדיר משתנים בצורה דינמית ישר באמצעות global כך:

													
from z3 import *

username = bytearray("root")
data = [0x2121, 0x3568, 0x33F6, 0x2c6c, 0x2857, 0x24f0, 0x30a0, 0x12cd, 0x14c1, 0x18f0, 0x1AD8]


solver = Solver()
for i in xrange(11):
	globals()["b{}".format(i)] = BitVec("b{}".format(i),32)

												
												

לאחר מכן עלינו להגדיר את הערך הדצימלי של התווים שאנו מאפשרים ל-z3 להזין על מנת לקבל את הסיסמא:
solver.add(And(globals()["b{}".format(i)] > 48, globals()["b{}".format(i)] < 122))

ולבסוף נגדיר חוק פשוט המבוסס על התנאים שהוצאנו מ-IDA:

solver.add((username[i % 4] ^ 0x14) * globals()["b{}".format(i)] + ( globals()["b{}".format(i)] ^ 0x4d) - 15 == data[i])

הקוד המלא יראה כך:


להורדת הקוד

לאחר שנריץ את הקוד נקבל את התשובה לאתגר:

בסרטון הצגתי לכם שקיימת דרך נוספת לפתרון האתגר והיא בעצם ניצול הבאג הקיים באתגר:

אם נסתכל על הלולאה נראה שהיא מתקיימת (strlen(a2 פעמים, שזה בעצם ככמות התווים בסיסמא.

אך מה יקרה אם לסיסמא לא יהיו תווים כלל?

אז ה-strlen יחזיר 0 והלולאה לא תתבצע, מה שיגרום להחזרת הערך 1 וקבלת הטקסט "Access Granted" ללא הצורך בסיסמא.