Upgrade to Pro — share decks privately, control downloads, hide ads and more …

実装して学ぶ Symbolic Backward Execution

実装して学ぶ Symbolic Backward Execution

2019/01/20 情報科学若手の会冬の陣2019 #wakate2019w

シンボリック実行のマイナーなアルゴリズムSBEをPythonで実装して得た知見を共有します。今回のSBEエンジンは最弱事前条件に基づいて計算します。

友利奈緒(@K_atc)

January 20, 2019
Tweet

More Decks by 友利奈緒(@K_atc)

Other Decks in Science

Transcript

  1. Symbolic Backward Execution (by @K_atc) Security Engineer Interested in vulnerability

    detection (especially symbolic execution), illustration. Doing for 6 years. Person same with author. https://www.pixiv.net/member.php?id=4440209 Profile
  2. Symbolic Backward Execution (by @K_atc) Symbolic execution is a execution

    symbolizes any inputs. Symbol is similar to mathematical variables, and is NOT fixed values. In symbolic execution, execution environment such as registers, stack, memory, and files are symbolized. What is symbolic execution? Concept of Forward Symbolic Execution (FSE) (FSE is a method often adopted to implement symbolic execution) void testme(int a, int b) { int c = 0; if (a * b == 6) { c = 1; if (a == 1) c = 3; } assert(a * b * c == 6); } a ✕ b = 6 ∧ c ≠ 0 a ✕ b ≠ 6 ∧ c = 0 Φ a ✕ b = 6 ∧ a = 1 ∧ c = 1 a ✕ b = 6 ∧ a ≠ 1 ∧ c = 1 ✔ Assertion pass ✔ Assertion pass ✔ Assertion fail … path constraint
  3. Symbolic Backward Execution (by @K_atc) [KLEE 2008] Authentication Bypass [Firmalice

    2015] [AEG 2011, EOEDroid 2018] ✕ [Driller 2016, QSYM 2018] [KLEE] Cadar, Cristian et al. “KLEE: Unassisted and Automatic Generation of High-Coverage Tests for Complex Systems Programs.” OSDI (2008). [Firmalice] Shoshitaishvili, Yan et al. “Firmalice - Automatic Detection of Authentication Bypass Vulnerabilities in Binary Firmware.” NDSS (2015). [AEG] Avgerinos, Thanassis et al. “AEG: Automatic Exploit Generation.” NDSS 2011 (2011). [EOEDroid] Yang, Guangliang et al. “Automated Generation of Event-Oriented Exploits in Android Hybrid Apps.” NDSS (2018). [Driller] Stephens, Nick et al. “Driller: Augmenting Fuzzing Through Selective Symbolic Execution.” NDSS (2016). [QSYM] Yun, Insu et al. “QSYM : A Practical Concolic Execution Engine Tailored for Hybrid Fuzzing.” USENIX Security Symposium (2018).
  4. Symbolic Backward Execution (by @K_atc) S Weakest Precondition 0 ≦

    x 0 ≦ x ∧ x ≦ a (a 0) x 0 x x True False ℤ ∅ Stronger Weaker
  5. Symbolic Backward Execution (by @K_atc) ※SMT * z3py *SMT Satisfiability

    Modulo Theories ∀∃ from z3 import * x, y = Ints('x y') wp = True wp = And(y > 3, wp) wp = substitute(wp, (y, x + 2)) simplify(wp) print(wp) Not(x <= 1) { ? } y := x + 2; assert y > 3; {true} x > 1 ⇄ x > 1
  6. Weakest Precondition Python SBE Python Symbolic Backward Execution (by @K_atc)

    Translate GCL & Gen Symbol Vars wp(S, Q) GCL S Q Python Code Models Solve (Concretize) Symbolic Backward Execution Engine ❶ ❷ ❸ • • • If ※ • ※ ❶ GCLのノードの実装 Python →Python AST→GCL wp
  7. GCL Python ❶ GCL Symbolic Backward Execution (by @K_atc) class

    GCL(): op = "" def __init__(self): pass class Substitute(GCL): op = op.Substitute def __init__(self, x, e): self.x = x # self.e = e # def __repr__(self): return "{}({}, {})".format(self.op, self.x, self.e) x, e
  8. Symbolic Backward Execution (by @K_atc) 1. Python ast AST 2.

    AST GCL ❷ Python →Python AST→GCL import ast code = "if (x > 0): y = 1" p = ast.parse(code) S = seq_node(p.body) if isinstance(node, ast.Assign): target = expr_node(node.targets[0], depth + 1, function_name) value = expr_node(node.value, depth + 1, function_name) assign_returned_values = __assign_returned_values(node.value) return assign_returned_values + gcl.Substitute(target, value) Assign →GCL GCL If(x > 0, Substitute(y, 1), Skip()) S Module(body=[If(test=Compare(left=Name(id=‘x’, ctx=Load()), ops=[Gt()], comparators=[Num(n=0)]), body=[Assign(targets=[Name(id='y', ctx=Store())], value=Num(n=1))], orelse=[])]) p Python AST GCL
  9. Symbolic Backward Execution (by @K_atc) ❸ wp(S, Q) def wp(S,

    Q): …. snipped … if S.op is node.op.Substitute: … snipped … if z3.is_expr(Q): return z3.substitute(Q, (S.x, S.e)) else: # Q is Bool return Q … snipped … if S.op is node.op.Seq: return wp(S.S1, wp(S.S2, Q)) … snipped … Weakest Precondition Python wp(S, Q)
  10. { ??? } y = (x + 1) * 2

    if y >= 6: z = 1 else: z = 0 assert(z == 1) { True } presen-demo.py Symbolic Backward Execution (by @K_atc) x
  11. Symbolic Backward Execution (by @K_atc) if expr = """ y

    = (x + 1) * 2 if y >= 6: z = 1 else: z = 0 assert(z == 1) """ p = ast.parse(expr) S = seq_node(p.body) Q = True print("S = {}".format(S)) print("Q = {}".format(Q)) P = wp(S, Q) P = simplify(P) print("wp(S, Q) = {}".format(P)) S = Seq(Substitute(y, (x + 1)*2), Seq(If(y >= 6, Substitute(z, 1), Substitute(z, 0)), Assert(z == 1))) Q = True wp(S, Q) = x >= 2
  12. Symbolic Backward Execution (by @K_atc) • • • GCL WP

    FSE • • GCL • • DBI Dynamic Binary Instrumentation → SBE Hybrid Fuzzing SBE
  13. • Weakest Precondition SBE Python • SBE Weakest Precondition •

    ✌(‘ω’✌ ) ✌(‘ω’)✌ ( ✌‘ω’)✌ • • ※ • While CFG • SBE BAP [DWP] Symbolic Backward Execution (by @K_atc) [DWP] David Brumley, Ivan Jager, Efficient Directionless Weakest Preconditions, CMU-CyLab-10-002.
  14. Symbolic Backward Execution (by @K_atc) • Hoare_J: , http://proofcafe.org/sf/Hoare_J.html ※

    Software Foundations • Weakest Precondition Calculus, https://cs.anu.edu.au/courses/comp2600/Lectures/19wp1.pdf • Roberto Baldoni, et al., A Survey of Symbolic Execution Techniques, arxiv, 2018. • Symbolic Execution, https://www.seas.harvard.edu/courses/cs252/2011sp/slides/Lec13- SymExec.pdf • David Brumley, Ivan Jager, Efficient Directionless Weakest Preconditions, CMU-CyLab-10-002, 2010.