tag:blogger.com,1999:blog-7011836621605765499.post2236363504854199041..comments2022-10-26T05:07:58.844-07:00Comments on balidani: Boston Key Party - R3V3 writeupbalidanihttp://www.blogger.com/profile/05810943104283312084noreply@blogger.comBlogger5125tag:blogger.com,1999:blog-7011836621605765499.post-57991083522325218792014-03-05T12:41:51.598-08:002014-03-05T12:41:51.598-08:00This was in Z3Py. You would loop through the varia...This was in Z3Py. You would loop through the variable creation and append them to a list. Do the same for the conditions and save them to a separate list.<br /><br />Then loop through your values (0xAC, 0x94, etc.) and build all the Implies statements. <br /><br />I'll see if I can whip something up like that if I have time later this week. It would have saved me some trouble during the CTF. Doing everything by hand was a bit tedious.Anonymoushttps://www.blogger.com/profile/01390227842123562522noreply@blogger.comtag:blogger.com,1999:blog-7011836621605765499.post-51495628056100130112014-03-05T04:32:47.894-08:002014-03-05T04:32:47.894-08:00Very nice, thanks! Is there a way to do this with ...Very nice, thanks! Is there a way to do this with a loop in z3?balidanihttps://www.blogger.com/profile/05810943104283312084noreply@blogger.comtag:blogger.com,1999:blog-7011836621605765499.post-49725214299264498722014-03-03T09:59:35.597-08:002014-03-03T09:59:35.597-08:00Might not be the best Z3, but this was my solution...Might not be the best Z3, but this was my solution for it. The output needed some manipulation (sorting, cleaning, convert from int to char). Nice work!<br /><br />a, b, c, d, e, f, g, h, i, j, k, l, m, n, o, p, q, r, s, t, u, v, w, x, y, z, aa, ab, ac, ad = Ints('a b c d e f g h i j k l m n o p q r s t u v w x y z aa ab ac ad')<br />c_abc, c_def, c_ghi, c_jkl, c_mno, c_pqr, c_stu, c_vwx, c_yzaa, c_abacad = Bools('c_abc c_def c_ghi c_jkl c_mno c_pqr c_stu c_vwx c_yzaa c_abacad')<br />p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24, p25, p26, p27, p28 = Bools('p1 p2 p3 p4 p5 p6 p7 p8 p9 p10 p11 p12 p13 p14 p15 p16 p17 p18 p19 p20 p21 p22 p23 p24 p25 p26 p27 p28')<br /><br />slvr = Solver()<br />slvr.add(Implies(p1, a + c == 0xAC),<br /> Implies(p2, b + d == 0x94),<br /> Implies(p3, c + e == 0xa4),<br /> Implies(p4, d + f == 0x96),<br /> Implies(p5, e + g == 0x94),<br /> Implies(p6, f + h == 0x91),<br /> Implies(p7, g + i == 0x93),<br /> Implies(p8, h + j == 0x9d),<br /> Implies(p9, i + k == 0xa3),<br /> Implies(p10, j + l == 0xa5),<br /> Implies(p11, k + m == 0xae),<br /> Implies(p12, l + n == 0x9f),<br /> Implies(p13, m + o == 0xae),<br /> Implies(p14, n + p == 0x8e),<br /> Implies(p15, o + q == 0xbe),<br /> Implies(p16, p + r == 0x98),<br /> Implies(p17, q + s == 0xb3),<br /> Implies(p18, r + t == 0x94),<br /> Implies(p19, s + u == 0xa8),<br /> Implies(p20, t + v == 0x90),<br /> Implies(p21, u + w == 0xb3),<br /> Implies(p22, v + x == 0x90),<br /> Implies(p23, w + y == 0xad),<br /> Implies(p24, x + z == 0x95),<br /> Implies(p25, y + aa == 0x8f),<br /> Implies(p26, z + ab == 0xa2),<br /> Implies(p27, aa + ac == 0x8a),<br /> Implies(p28, ab + ad == 0x8d),<br /> Implies(c_abc, a + b + c == 0xed),<br /> Implies(c_def, d + e + f == 0xdb),<br /> Implies(c_ghi, g + h + i == 0xe1),<br /> Implies(c_jkl, j + k + l == 0x104),<br /> Implies(c_mno, m + n + o == 0xf7),<br /> Implies(c_pqr, p + q + r == 0xf7),<br /> Implies(c_stu, s + t + u == 0xe9),<br /> Implies(c_vwx, v + w + x == 0xef),<br /> Implies(c_yzaa, y + z + aa == 0xe3),<br /> Implies(c_abacad, ab + ac + ad == 0xd6))<br /><br />#>implying<br /><br />print slvr.check(p1, p2, p3, p4, p5, p6, p7, p8, p9, p10, p11, p12, p13, p14, p15, p16, p17, p18, p19, p20, p21, p22, p23, p24, p25, p26, p27, p28, c_abc, c_def, c_ghi, c_jkl, c_mno, c_pqr, c_stu, c_vwx, c_yzaa, c_abacad)<br />print slvr.model()Anonymoushttps://www.blogger.com/profile/01390227842123562522noreply@blogger.comtag:blogger.com,1999:blog-7011836621605765499.post-69337680251102694692014-03-02T14:08:47.085-08:002014-03-02T14:08:47.085-08:00You can just patch the binary and put NOPs there i...You can just patch the binary and put NOPs there instead of the call. But we ended up solving everything with static analysis.balidanihttps://www.blogger.com/profile/05810943104283312084noreply@blogger.comtag:blogger.com,1999:blog-7011836621605765499.post-15761765979422350832014-03-02T14:05:07.559-08:002014-03-02T14:05:07.559-08:00how to bypass .text:0000000000401165 call bad_leve...how to bypass .text:0000000000401165 call bad_level ? I mean der is a cmp before that which leads to bad_boy .in3ohttps://www.blogger.com/profile/07172335678194012502noreply@blogger.com