"
-| (atom.compound_procedure _ args body) := "(λ (" ++ string.intercalate " " args ++ ") " ++ (atom.repr body) ++ ")"
-| (atom.symbol sym) := sym
-| (atom.list lst) := "(" ++ string.intercalate " " (list.map atom.repr lst) ++ ")"
-| (atom.cell car cdr) := "(" ++ atom.repr car ++ " . " ++ atom.repr cdr ++ ")"
-meta instance : has_repr atom := ⟨atom.repr⟩
-#+END_SRC
-
-The parser is fairly simple, too, but we have to deal with mutual recursion.
-
-#+BEGIN_SRC lean
-meta def parse_until_rparen : ℤ → list token → option (list token × list token)
-| 0 (list.cons (token.rparen) rest) := some ([], rest)
-| n (list.cons (token.rparen) rest) :=
- match parse_until_rparen (n - 1) rest with
- | none := none
- | some result := some (list.cons token.rparen result.fst, result.snd)
- end
-| n (list.cons (token.lparen) rest) :=
- match parse_until_rparen (n + 1) rest with
- | none := none
- | some result := (list.cons token.lparen result.fst, result.snd)
- end
-| n (list.cons tok rest) :=
- match parse_until_rparen n rest with
- | none := none
- | some result := some (list.cons tok result.fst, result.snd)
- end
-| n (list.nil) := none
-
-meta mutual def parse_one, parse
-with parse_one : list token → option (atom × list token)
-| (list.cons token.lparen rest) :=
- match parse_until_rparen 0 rest with
- | none := none
- | some result := some (atom.list (parse result.fst), result.snd)
- end
-| (list.cons token.quot rest) :=
- match parse_one rest with
- | none := none
- | some result := some (atom.list [(atom.symbol "quote"), result.fst], result.snd)
- end
-| (list.cons (token.numeral n) rest) := some (atom.number n, rest)
-| (list.cons (token.symbol "#t") rest) := some (atom.boolean tt, rest)
-| (list.cons (token.symbol "#f") rest) := some (atom.boolean ff, rest)
-| (list.cons (token.symbol sym) rest) := some (atom.symbol sym, rest)
-| _ := none
-with parse : list token → list atom
-| (list.nil) := []
-| stream := match parse_one stream with
-| none := []
-| some (result, (list.nil)) := [result]
-| some (result, rest) := (list.cons result (parse rest))
-end
-
-#eval list.map atom.repr (parse (tokenize "(+ 2 4)"))
-#eval list.map atom.repr (parse (tokenize "(define (list-of-values exps env)
- (if (no-operands? exps)
- '()
- (cons (eval (first-operand exps) env)
- (list-of-values (rest-operands exps) env))))"))
-#+END_SRC
-
-The evaluator has a notion of errors, whereas the language semantics doesn't, so we'll introduce a type for that as well.
-
-#+BEGIN_SRC lean
-inductive lisp_error : Type
-| expected_number : lisp_error
-| expected_symbol : lisp_error
-| expected_list : lisp_error
-| no_such_variable : string → lisp_error
-| bad_lambda : lisp_error
-| bad_begin : lisp_error
-| bad_if : lisp_error
-| bad_define : lisp_error
-| bad_arity : lisp_error
-| excessive_recursion : lisp_error
-| unknown_form : lisp_error
-
-def lisp_error.repr : lisp_error → string
-| (lisp_error.expected_number) := "Expected number"
-| (lisp_error.expected_symbol) := "Expected symbol"
-| (lisp_error.expected_list) := "Expected list"
-| (lisp_error.no_such_variable sym) := "No such variable: " ++ sym
-| (lisp_error.bad_lambda) := "Bad lambda form"
-| (lisp_error.bad_begin) := "Bad begin form"
-| (lisp_error.bad_if) := "Bad if form"
-| (lisp_error.bad_define) := "Bad define form"
-| (lisp_error.bad_arity) := "Compound procedure called with wrong number of arguments"
-| (lisp_error.excessive_recursion) := "Maximum recursion depth exceeded"
-| (lisp_error.unknown_form) := "Unknown form"
-instance : has_repr lisp_error := ⟨lisp_error.repr⟩
-
-def lisp_result (α : Type) := except lisp_error α
-
-meta def lisp_result_atom.repr : lisp_result atom → string
-| (except.ok result) := atom.repr result
-| (except.error err) := "ERROR: " ++ lisp_error.repr err
--- instance : has_repr lisp_result := ⟨lisp_result.repr⟩
-
-meta def lisp_result.repr {α : Type} : lisp_result (atom × α) → string
-| (except.ok (result, _)) := atom.repr result
-| (except.error err) := "ERROR: " ++ lisp_error.repr err
-#+END_SRC
-
-Now, we also need a notion of "state" and "frame."
-
-#+BEGIN_SRC lean
-def state : Type := string → option atom
-instance state_inhabited : inhabited state :=
-inhabited.mk (λ x, none)
-
-def state.update (name : string) (val : atom) (s : state) : state :=
-λname', if name' = name then some val else s name'
-
-notation s `{` name ` ↦ ` val `}` := state.update name val s
-
-def lookup_var : string → list state → option atom
-| var (list.nil) := none
-| var (list.cons s rest) :=
- match s var with
- | some result := some result
- | none := lookup_var var rest
- end
-
--- If we've just pushed a frame onto the environment, and a variable exists in
--- that frame, then looking up that variable in the environment is equivalent to
--- looking it up in the frame.
-lemma lookup_head (x : string) (y : state) (ys : list state) (z : atom) :
- y x = some z → lookup_var x (y :: ys) = some z :=
-begin
- intro h,
- simp [h, lookup_var],
-end
-
-def set_var : string → atom → list state → lisp_result (list state)
-| place new_value (list.nil) := except.error (lisp_error.no_such_variable place)
-| place new_value (list.cons s rest) :=
- match s place with
- | (some _) := except.ok (list.cons (s{place ↦ new_value}) rest)
- | none :=
- match set_var place new_value rest with
- | (except.ok rest') := except.ok (list.cons s rest')
- | (except.error e) := except.error e
- end
- end
-
--- This is only well-defined if |names| = |values|.
-def new_frame : list string → list atom → state
-| (list.cons name rest₁) (list.cons value rest₂) := (new_frame rest₁ rest₂){name ↦ value}
-| _ _ := λ _, none
-#+END_SRC
-
-And, finally, we can get into the implementation of evaluation. First, we'll implement evaluation of procedures. Either the procedure is primitive (or built-in), like =+=, it's a named compound procedure, it's a lambda form, or the name doesn't exist in the environment.
-
-#+BEGIN_EXPORT html
-
-#+END_EXPORT
-
-#+BEGIN_SRC lean
-def collect_params : atom → option (list string)
-| (atom.list (list.cons (atom.symbol param) rest)) :=
- match collect_params (atom.list rest) with
- | some rest' := some (list.cons param rest')
- | none := none
- end
-| (atom.list (list.nil)) := some []
-| _ := none
-
-#eval collect_params (atom.list [atom.symbol "x"])
-#eval collect_params (atom.list [atom.symbol "x", atom.symbol "y"])
-
-def mk_compound_procedure
- (closure_env : list state)
- (paramlist : atom)
- (body : list atom)
- : lisp_result atom :=
-match collect_params paramlist with
-| some params :=
- except.ok
- (atom.compound_procedure
- (λ x, lookup_var x closure_env)
- params
- (atom.list (list.cons (atom.symbol "begin") body)))
-| none := except.error (lisp_error.bad_lambda)
-end
-
-#eval lisp_result_atom.repr
- (mk_compound_procedure
- [(λ _, none)]
- (atom.list [atom.symbol "x"])
- [(atom.symbol "+"), (atom.number 2), (atom.number 4)])
-
-def symbol_name : atom → option string
-| (atom.symbol name) := some name
-| _ := none
-
-def is_primitive_procedure (name : string) : bool :=
- name ∈ ["+", "-", "*", "/", "=", "car", "cdr", "cons", "null?", "eqv?"]
-
-@[simp]
-lemma add_is_primitive : is_primitive_procedure "+" := by exact rfl
-@[simp]
-lemma sub_is_primitive : is_primitive_procedure "-" := by exact rfl
-@[simp]
-lemma mul_is_primitive : is_primitive_procedure "*" := by exact rfl
-@[simp]
-lemma div_is_primitive : is_primitive_procedure "/" := by exact rfl
-@[simp]
-lemma eq_is_primitive : is_primitive_procedure "=" := by exact rfl
-@[simp]
-lemma car_is_primitive : is_primitive_procedure "car" := by exact rfl
-@[simp]
-lemma cdr_is_primitive : is_primitive_procedure "cdr" := by exact rfl
-@[simp]
-lemma cons_is_primitive : is_primitive_procedure "cons" := by exact rfl
-@[simp]
-lemma null_is_primitive : is_primitive_procedure "null?" := by exact rfl
-@[simp]
-lemma eqv_is_primitive : is_primitive_procedure "eqv?" := by exact rfl
-
-def fold_maybe_numeric : (ℤ → ℤ → ℤ) → ℤ → list atom → option ℤ
-| op nil (list.cons (atom.number n) rest) :=
- do {
- rest_sum ← fold_maybe_numeric op nil rest,
- pure (op n rest_sum) }
-| op nil (list.nil) := some nil
-| _ _ _ := none
-
-def primitive_add (args : list atom) : lisp_result atom :=
-match fold_maybe_numeric (λ x y, x + y) 0 args with
-| some result := except.ok (atom.number result)
-| none := except.error lisp_error.expected_number
-end
-
-def primitive_sub (args : list atom) : lisp_result atom :=
-match fold_maybe_numeric (λ x y, x - y) 0 args with
-| some result := except.ok (atom.number result)
-| none := except.error lisp_error.expected_number
-end
-
-def primitive_mul (args : list atom) : lisp_result atom :=
-match fold_maybe_numeric (λ x y, x * y) 1 args with
-| some result := except.ok (atom.number result)
-| none := except.error lisp_error.expected_number
-end
-
-def primitive_div (args : list atom) : lisp_result atom :=
-match fold_maybe_numeric (λ x y, x / y) 1 args with
-| some result := except.ok (atom.number result)
-| none := except.error lisp_error.expected_number
-end
-
-def attach_state : lisp_result atom → list state → lisp_result (atom × list state)
-| (except.ok result) s := except.ok (result, s)
-| (except.error e) _ := except.error e
-
--- TODO: Error reporting could be better.
-def primitive_eq (args : list atom) : lisp_result atom :=
-match args with
-| (list.cons (atom.number x) (list.cons (atom.number y) _)) :=
- except.ok (if x = y then atom.boolean tt else atom.boolean ff)
-| _ := except.error lisp_error.expected_number
-end
-
--- This is where I got sick of being explicit about the return types.
-def primitive_car (args : list atom) : lisp_result atom :=
-match args with
-| (list.cons (atom.cell car cdr) _) := except.ok car
-| (list.cons car cdr) := except.ok car
-| _ := except.error lisp_error.expected_list
-end
-
-def primitive_cdr (args : list atom) : lisp_result atom :=
-match args with
-| (list.cons (atom.cell car cdr) _) := except.ok cdr
-| (list.cons car cdr) := except.ok (atom.list cdr)
-| _ := except.error lisp_error.expected_list
-end
-
-def primitive_cons (args : list atom) : lisp_result atom :=
-match args with
-| (list.cons car (list.cons (atom.list cdr) _)) := except.ok (atom.list (list.cons car cdr))
-| (list.cons car (list.cons cdr _)) := except.ok (atom.cell car cdr)
-| _ := except.error lisp_error.expected_list
-end
-
-def primitive_null (args : list atom) : lisp_result atom :=
-match args with
-| (list.cons (atom.list (list.nil)) _) := except.ok (atom.boolean tt)
-| (list.cons (atom.list _) _) := except.ok (atom.boolean ff)
-| _ := except.error lisp_error.expected_list
-end
-
-def primitive_eqv (args : list atom) : lisp_result atom :=
-match args with
-| (list.cons (atom.symbol x) (list.cons (atom.symbol y) _)) := except.ok (if x = y then atom.boolean tt else atom.boolean ff)
-| _ := except.error lisp_error.expected_symbol
-end
-#+END_SRC
-
-#+BEGIN_EXPORT html
-
-#+END_EXPORT
-
-We can't actually encode a "proper" Scheme implementation in Lean because there'a possibility that we write a program that doesn't terminate. If we cap the maximum evaluation depth, though, we can prove that the evaluator is well-founded. This more accurately models the real world, anyway, since computers have a finite amount of memory. So we have an =evaluation_state= which maintains the current =stack_depth=, and we'll use that as both a guardrail that allows us to prove that our recursive =eval= function eventually terminates.
-
-#+BEGIN_EXPORT html
-
-#+END_EXPORT
-
-#+BEGIN_SRC lean
-structure evaluation_state :=
-(stack_depth : ℕ)
-(environment : list state)
-(form : atom)
-
-def evaluation_state_measure : psum evaluation_state (psum evaluation_state evaluation_state) → ℕ
-| (psum.inl state) := state.stack_depth
-| (psum.inr (psum.inl state)) := state.stack_depth
-| (psum.inr (psum.inr state)) := state.stack_depth
-
-mutual def eval, apply, eval_param_list
-
-with eval : evaluation_state → lisp_result (atom × list state)
-| (evaluation_state.mk 0 _ _) :=
- except.error (lisp_error.excessive_recursion)
-| (evaluation_state.mk (stack_depth + 1) s (atom.undefined)) :=
- except.ok (atom.undefined, s)
-| (evaluation_state.mk (stack_depth + 1) s (atom.boolean bool)) :=
- except.ok (atom.boolean bool, s)
-| (evaluation_state.mk (stack_depth + 1) s (atom.number n)) :=
- except.ok (atom.number n, s)
-| (evaluation_state.mk (stack_depth + 1) s (atom.cell car cdr)) :=
- except.ok (atom.cell car cdr, s)
-| (evaluation_state.mk (stack_depth + 1) s (atom.primitive_procedure name)) :=
- except.ok (atom.primitive_procedure name, s)
-| (evaluation_state.mk (stack_depth + 1) s (atom.compound_procedure closure_env paramlist body)) :=
- except.ok (atom.compound_procedure closure_env paramlist body, s)
-| (evaluation_state.mk (stack_depth + 1) s (atom.symbol sym)) :=
- if sym = "+" then
- except.ok (atom.primitive_procedure "+", s)
- else if sym = "-" then
- except.ok (atom.primitive_procedure "-", s)
- else if sym = "*" then
- except.ok (atom.primitive_procedure "*", s)
- else if sym = "/" then
- except.ok (atom.primitive_procedure "/", s)
- else if sym = "=" then
- except.ok (atom.primitive_procedure "=", s)
- else if sym = "car" then
- except.ok (atom.primitive_procedure "car", s)
- else if sym = "cdr" then
- except.ok (atom.primitive_procedure "cdr", s)
- else if sym = "cons" then
- except.ok (atom.primitive_procedure "cons", s)
- else if sym = "null?" then
- except.ok (atom.primitive_procedure "null?", s)
- else if sym = "eqv?" then
- except.ok (atom.primitive_procedure "eqv?", s)
- else match (lookup_var sym s) with
- | none := except.error (lisp_error.no_such_variable sym)
- | some value := except.ok (value, s)
- end
-| (evaluation_state.mk (stack_depth + 1) s (atom.list (list.cons func rest))) :=
- if symbol_name func = some "quote" then
- except.ok (list.head rest, s)
- else if symbol_name func = some "lambda" then
- match mk_compound_procedure s (list.head rest) (list.tail rest) with
- | (except.ok lambda) := except.ok (lambda, s)
- | (except.error err) := except.error err
- end
- else if symbol_name func = some "begin" then
- match rest with
- | (list.cons head (list.nil)) :=
- eval (evaluation_state.mk stack_depth s head)
- | (list.cons head tail) :=
- match eval (evaluation_state.mk stack_depth s head) with
- | (except.ok (result, s')) :=
- eval (evaluation_state.mk stack_depth s' (atom.list (list.cons (atom.symbol "begin") tail)))
- | (except.error e) := (except.error e)
- end
- | _ := (except.error lisp_error.bad_begin)
- end
- else if symbol_name func = some "set!" then
- match rest with
- | (list.cons (atom.symbol place) (list.cons value _)) :=
- match set_var place value s with
- | (except.ok s') := except.ok (atom.undefined, s')
- | (except.error e) := except.error e
- end
- | _ := except.error lisp_error.bad_arity
- end
- else if symbol_name func = some "if" then
- match rest with
- | (list.cons cond (list.cons ite_true (list.nil))) :=
- match eval (evaluation_state.mk stack_depth s cond) with
- | except.ok ((atom.boolean ff), s') := except.ok (atom.undefined, s')
- | except.ok (_, s') :=
- match eval (evaluation_state.mk stack_depth s ite_true) with
- | except.ok (result, s'') := except.ok (result, s'')
- | except.error e := except.error e
- end
- | except.error e := except.error e
- end
- | (list.cons cond (list.cons ite_true (list.cons ite_false _))) :=
- match eval (evaluation_state.mk stack_depth s cond) with
- | except.ok ((atom.boolean ff), s') :=
- match eval (evaluation_state.mk stack_depth s ite_false) with
- | except.ok (result, s'') := except.ok (result, s'')
- | except.error e := except.error e
- end
- | except.ok (_, s') :=
- match eval (evaluation_state.mk stack_depth s ite_true) with
- | except.ok (result, s'') := except.ok (result, s'')
- | except.error e := except.error e
- end
- | except.error e := except.error e
- end
- | _ := except.error lisp_error.bad_if
- end
- else if symbol_name func = some "define" then
- match rest with
- -- Function definition.
- | (list.cons (atom.list (list.cons (atom.symbol name) args)) body) :=
- match mk_compound_procedure s (atom.list args) body with
- | (except.ok procedure) := except.ok (atom.undefined, list.cons ((list.head s){name ↦ procedure}) (list.tail s))
- | (except.error e) := except.error e
- end
- | (list.cons (atom.symbol name) body) :=
- match eval (evaluation_state.mk stack_depth s (list.head body)) with
- | (except.ok (result, _)) := except.ok (atom.undefined, list.cons ((list.head s){name ↦ result}) (list.tail s))
- | (except.error e) := except.error e
- end
- | _ := except.error lisp_error.bad_define
- end
- else apply (evaluation_state.mk stack_depth s (atom.list (list.cons func rest)))
-| _ := except.error lisp_error.unknown_form
-
-with apply : evaluation_state → lisp_result (atom × list state)
-| (evaluation_state.mk 0 _ _) :=
- except.error (lisp_error.excessive_recursion)
-| (evaluation_state.mk (stack_depth + 1) s (atom.list (list.cons func args))) :=
- let func' := eval (evaluation_state.mk stack_depth s func),
- args_evaluated := eval_param_list (evaluation_state.mk stack_depth s (atom.list args)) in
- match func' with
- | (except.ok ((atom.primitive_procedure "+"), _)) :=
- match args_evaluated with
- | (except.ok (args', s')) := attach_state (primitive_add args') s
- | (except.error e) := except.error e
- end
- | (except.ok ((atom.primitive_procedure "-"), _)) :=
- match args_evaluated with
- | (except.ok (args', s')) := attach_state (primitive_sub args') s
- | (except.error e) := except.error e
- end
- | (except.ok ((atom.primitive_procedure "*"), _)) :=
- match args_evaluated with
- | (except.ok (args', s')) := attach_state (primitive_mul args') s
- | (except.error e) := except.error e
- end
- | (except.ok ((atom.primitive_procedure "/"), _)) :=
- match args_evaluated with
- | (except.ok (args', s')) := attach_state (primitive_div args') s
- | (except.error e) := except.error e
- end
- | (except.ok ((atom.primitive_procedure "="), _)) :=
- match args_evaluated with
- | (except.ok (args', s')) := attach_state (primitive_eq args') s
- | (except.error e) := except.error e
- end
- | (except.ok ((atom.primitive_procedure "car"), _)) :=
- match args_evaluated with
- | (except.ok (args', s')) := attach_state (primitive_car args') s
- | (except.error e) := except.error e
- end
- | (except.ok ((atom.primitive_procedure "cdr"), _)) :=
- match args_evaluated with
- | (except.ok (args', s')) := attach_state (primitive_cdr args') s
- | (except.error e) := except.error e
- end
- | (except.ok ((atom.primitive_procedure "cons"), _)) :=
- match args_evaluated with
- | (except.ok (args', s')) := attach_state (primitive_cons args') s
- | (except.error e) := except.error e
- end
- | (except.ok ((atom.primitive_procedure "null?"), _)) :=
- match args_evaluated with
- | (except.ok (args', s')) := attach_state (primitive_null args') s
- | (except.error e) := except.error e
- end
- | (except.ok ((atom.primitive_procedure "eqv?"), _)) :=
- match args_evaluated with
- | (except.ok (args', s')) := attach_state (primitive_eqv args') s
- | (except.error e) := except.error e
- end
- | (except.ok ((atom.primitive_procedure name), _)) :=
- except.error (lisp_error.no_such_variable name)
- | (except.ok ((atom.compound_procedure closure_env paramlist body), s')) :=
- match args_evaluated with
- | (except.ok (args', s')) :=
- let s'' := (list.cons (new_frame paramlist args') (list.cons closure_env s')) in
- eval (evaluation_state.mk stack_depth s'' body)
- | (except.error e) := except.error e
- end
- | _ := except.error (lisp_error.unknown_form)
- end
-| _ := except.error lisp_error.unknown_form
-
-with eval_param_list : evaluation_state → lisp_result (list atom × list state)
-| (evaluation_state.mk 0 _ _) :=
- except.error (lisp_error.excessive_recursion)
-| (evaluation_state.mk stack_depth s (atom.list (list.nil))) :=
- except.ok ([], s)
-| (evaluation_state.mk (stack_depth + 1) s (atom.list (list.cons elt rest))) :=
- match eval (evaluation_state.mk stack_depth s elt) with
- | (except.ok (result_head, s')) :=
- match eval_param_list (evaluation_state.mk stack_depth s' (atom.list rest)) with
- | except.ok (result_rest, s'') := except.ok (list.cons result_head result_rest, s'')
- | (except.error e) := except.error e
- end
- | (except.error e) := except.error e
- end
-| _ := except.error lisp_error.unknown_form
-
-using_well_founded {rel_tac := λ _ _, `[exact ⟨_, measure_wf evaluation_state_measure⟩]}
-#+END_SRC
-
-#+BEGIN_EXPORT html
-
-#+END_EXPORT
-
-I found the evaluation state structure to actually be quite convenient in reasoning about things like whether or not an evaluation is finite.
-
-#+BEGIN_SRC lean
-lemma finite_implies_nonzero_stack_depth
- (form result : atom)
- (environment environment' : list state)
- (stack_depth : ℕ)
- (h_finite : ¬ (eval (evaluation_state.mk stack_depth environment form) = except.error (lisp_error.excessive_recursion))) :
- stack_depth > 0 :=
-begin
- by_contra',
- apply h_finite,
- simp [le_of_eq] at this,
- simp [this, eval],
-end
-#+END_SRC
-
-The approach I've taken for the program semantics is to compile the expression to a "statement" type, and then reason about the big step semantics of those statements.
-
-At the beginning, I was doing small step semantics, until I realized that it was really hard to reason about a language where everything is an expression without being able to assume hypotheses about the transitive nature of small steps, which Lean didn't like at all. Something about nesting inductive predicates.
-
-#+BEGIN_EXPORT html
-
-#+END_EXPORT
-
-#+BEGIN_SRC lean
-inductive stmt : Type
-| expr : atom → stmt -- 1, #tt, symbol, ...
-| var : string → stmt -- var-name
-| seq : stmt → stmt → stmt -- (begin form ... rest)
-| assign : string → stmt → stmt -- (set! name expr)
-| define : string → stmt → stmt -- (define name expr)
-| ite : stmt → stmt → stmt → stmt -- (if cond expr-true expr-false)
-| app : stmt → list stmt → stmt -- ((lambda (arg1 ... argn) body) param1 ... paramn)
-
-meta def stmt.repr : stmt → string
-| (stmt.expr expr) := "(expr " ++ atom.repr expr ++ ")"
-| (stmt.var name) := "(deref " ++ name ++ ")"
-| (stmt.seq car cdr) := "(seq " ++ stmt.repr car ++ " " ++ stmt.repr cdr ++ ")"
-| (stmt.assign place rhs) := "(assign " ++ place ++ " " ++ stmt.repr rhs ++ ")"
-| (stmt.define place rhs) := "(define " ++ place ++ " " ++ stmt.repr rhs ++ ")"
-| (stmt.ite cond if_true if_false) := "(if " ++ stmt.repr cond ++ " " ++ stmt.repr if_true ++ " " ++ stmt.repr if_false ++ ")"
-| (stmt.app func args) := "(application " ++ stmt.repr func ++ " " ++ string.intercalate " " (list.map stmt.repr args) ++ ")"
-
-instance stmt_inhabited : inhabited stmt :=
-inhabited.mk (stmt.expr (atom.undefined))
-
-def is_some {α : Type} : option α → Prop
-| (some _) := true
-| _ := false
-
-def is_lambda : atom → Prop
-| (atom.list (list.cons (atom.symbol "lambda") _)) := true
-| _ := false
-
-def seq_from_list_stmt : list stmt → stmt
-| (list.nil) := stmt.expr atom.undefined
-| (list.cons head (list.nil)) := head
-| (list.cons head tail) := stmt.seq head (seq_from_list_stmt tail)
-
-mutual def compile_stmt, compile_stmt_list
-with compile_stmt : atom → option stmt
--- Arity 0
-| (atom.list (list.cons func (list.nil))) :=
- do {
- result ← compile_stmt func,
- pure (stmt.app result []) }
--- Arity 1
-| (atom.list (list.cons func (list.cons rest (list.nil)))) :=
- match func with
- | (atom.symbol "begin") := compile_stmt rest
- | (atom.symbol "quote") := some (stmt.expr rest)
- | _ := do {
- result₁ ← compile_stmt func,
- result₂ ← compile_stmt rest,
- pure (stmt.app result₁ [result₂]) }
- end
--- Arity 2
-| (atom.list (list.cons func (list.cons place (list.cons rhs (list.nil))))) :=
- match func with
- | (atom.symbol "begin") :=
- do {
- result₁ ← compile_stmt func,
- result₂ ← compile_stmt place,
- result₃ ← compile_stmt rhs,
- pure (stmt.seq result₂ result₃) }
- | (atom.symbol "set!") :=
- match place with
- | (atom.symbol place) :=
- do {
- rhs_result ← compile_stmt rhs,
- pure (stmt.assign place rhs_result) }
- | _ := none
- end
- -- We'll convert lambda expressions into compound procedures at evaluation
- -- time. We don't have scope information at compile time, so we can't
- -- construct closed environments.
- | (atom.symbol "lambda") := some (stmt.expr (atom.list [func, place, rhs]))
- | (atom.symbol "define") :=
- match place with
- -- Syntax sugar for (define func (lambda (param₁ ...) body))
- | (atom.list (list.cons (atom.symbol func_name) params)) :=
- some (stmt.expr
- (atom.list ([
- (atom.symbol "lambda"),
- (atom.list params),
- (atom.list [(atom.symbol "begin"), rhs])])))
- | (atom.symbol place) :=
- do {
- rhs_result ← compile_stmt rhs,
- pure (stmt.define place rhs_result) }
- | _ := none
- end
- | _ := do {
- result₁ ← compile_stmt func,
- result₂ ← compile_stmt place,
- result₃ ← compile_stmt rhs,
- pure (stmt.app result₁ [result₂, result₃]) }
- end
--- Arity 3
-| (atom.list (list.cons func (list.cons rest_head (list.cons rest_tail₁ (list.cons rest_tail₂ (list.nil)))))) :=
-match func with
- | (atom.symbol "if") :=
- do {
- result₁ ← compile_stmt rest_head,
- result₂ ← compile_stmt rest_tail₁,
- result₃ ← compile_stmt rest_tail₂,
- pure (stmt.ite result₁ result₂ result₃)}
- | (atom.symbol "begin") :=
- do {
- result₁ ← compile_stmt rest_head,
- result₂ ← compile_stmt rest_tail₁,
- result₃ ← compile_stmt rest_tail₂,
- pure (stmt.seq result₁ (stmt.seq result₂ result₃))}
- | _ := do {
- result₁ ← compile_stmt func,
- result₂ ← compile_stmt rest_head,
- result₃ ← compile_stmt rest_tail₁,
- result₄ ← compile_stmt rest_tail₂,
- pure (stmt.app result₁ [result₂, result₃, result₄])}
- end
--- Arity n > 3
-| (atom.list (list.cons func (list.cons rest_head (list.cons rest_tail₁ rest_tail₂)))) :=
- match func with
- | (atom.symbol "begin") :=
- do {
- result₁ ← compile_stmt rest_head,
- result₂ ← compile_stmt rest_tail₁,
- result₃ ← compile_stmt_list rest_tail₂,
- pure (stmt.seq result₁ (stmt.seq result₂ (seq_from_list_stmt result₃)))}
- -- Generalization of `lambda` above.
- -- We're duplicating code to make the equation compiler happy.
- | (atom.symbol "lambda") := some (stmt.expr (atom.list (list.cons func (list.cons rest_head (list.cons rest_tail₁ rest_tail₂)))))
- -- Syntax sugar for (define func (lambda (param₁ ...) body))
- -- We're duplicating code to make the equation compiler happy.
- | (atom.symbol "define") :=
- match rest_head with
- | (atom.list (list.cons (atom.symbol func_name) params)) :=
- some (stmt.expr
- (atom.list ([
- (atom.symbol "lambda"),
- (atom.list params),
- (atom.list ([(atom.symbol "begin")] ++ (list.cons rest_tail₁ rest_tail₂)))])))
- | _ := none
- end
- | _ := do {
- result₁ ← compile_stmt func,
- result₂ ← compile_stmt_list (list.cons rest_head (list.cons rest_tail₁ rest_tail₂)),
- pure (stmt.app result₁ result₂) }
- end
-| (atom.list (list.nil)) := none
-| (atom.symbol sym) :=
- if is_primitive_procedure sym then
- some (stmt.expr (atom.primitive_procedure sym))
- else some (stmt.var sym)
-| e := some (stmt.expr e)
-
-with compile_stmt_list : list atom → option (list stmt)
-| (list.cons head rest) :=
- match compile_stmt head with
- | (some result) :=
- match (compile_stmt_list rest) with
- | some result_rest := some (list.cons result result_rest)
- | none := none
- end
- | none := none
- end
-| (list.nil) := some []
-
-def unwrap_option {α : Type} [inhabited α] : option α → α
-| (some x) := x
-| _ := inhabited.default
-
-mutual inductive args_step, big_step
-with args_step : list stmt × list state → list atom × list state → Prop
-| nil {s} :
- args_step
- ((list.nil), s)
- ((list.nil), s)
-
-| cons {S T s s' s'' u r}
- (hstep : big_step (S, s) (u, s'))
- (hrest : args_step (T, s') (r, s'')) :
- args_step
- (list.cons S T, s)
- (list.cons u r, s'')
-
-with big_step : stmt × list state → atom × list state → Prop
--- I'm not especially happy with this particular rule. I don't think it's
--- unsound, but I'm not 100% confident about that. Unfortunately it's necessary
--- if I don't want to completely rework how function bodies are represented.
-| drop_frame {expr u s s' f rest}
- (heval_in_frame : big_step (expr, s) (u, s'))
- (h_has_frame : s = list.cons f rest) :
- big_step (expr, s) (u, rest)
-
-| self_evaluating {expr s}
- (h_not_lambda : ¬ is_lambda expr):
- big_step
- (stmt.expr expr, s)
- (expr, s)
-
-| construct_compound_procedure {args body closure s}
- (h_well_formed : mk_compound_procedure s args body = except.ok closure):
- big_step
- (stmt.expr (atom.list ([(atom.symbol "lambda"), args] ++ body)), s)
- (closure, s)
-
-| var_deref {x u s}
- (h_lookup_var : lookup_var x s = some u):
- big_step
- (stmt.var x, s)
- (u, s)
-
-| seq {S S' T s t t' u}
- (hS : big_step (S, s) (S', t))
- (hT : big_step (T, t) (u, t')) :
- big_step
- (stmt.seq S T, s)
- (u, t')
-
-| assign {x rhs rhs_expr s s' s''}
- (h_rhs_eval : big_step (rhs, s) (rhs_expr, s'))
- (h_var_exists : set_var x rhs_expr s' = except.ok s'') :
- big_step
- (stmt.assign x rhs, s)
- (atom.undefined, s'')
-
-| define {x rhs rhs_expr s s'}
- (h_rhs_eval : big_step (rhs, s) (rhs_expr, s')) :
- big_step
- (stmt.define x rhs, s)
- (atom.undefined, list.cons ((list.head s'){x ↦ rhs_expr}) (list.tail s'))
-
-| ite_true {b S T s s' t u}
- (hcond : big_step (b, s) ((atom.boolean tt), s'))
- (heval : big_step (S, s') (u, t)) :
- big_step
- (stmt.ite b S T, s)
- (u, t)
-
-| ite_false {b S T s s' t u}
- (hcond : big_step (b, s) ((atom.boolean ff), s'))
- (heval : big_step (T, s') (u, t)) :
- big_step
- (stmt.ite b S T, s)
- (u, t)
-
-| application {closed func params body body' args args' expr s s' s'' s'''}
- (h_func : big_step (func, s) ((atom.compound_procedure closed params body), s'))
- (h_args : args_step (args, s') (args', s''))
- (h_well_formed : compile_stmt body = some body')
- (heval : big_step (body',
- (list.cons (new_frame params args')
- (list.cons closed s')))
- (expr, s'')) :
- big_step
- (stmt.app func args, s)
- (expr, s''')
-
-| application_primitive_add {s s' args args' n}
- (h_args : args_step (args, s) (args', s'))
- (heval: primitive_add args' = except.ok (atom.number n)):
- big_step
- (stmt.app
- (stmt.expr (atom.primitive_procedure "+"))
- args, s)
- (atom.number n, s)
-
-| application_primitive_sub {s s' args args' n}
- (h_args : args_step (args, s) (args', s'))
- (heval: primitive_sub args' = except.ok (atom.number n)):
- big_step
- (stmt.app
- (stmt.expr (atom.primitive_procedure "-"))
- args, s)
- (atom.number n, s)
-
-| application_primitive_mul {s s' args args' n}
- (h_args : args_step (args, s) (args', s'))
- (heval: primitive_mul args' = except.ok (atom.number n)):
- big_step
- (stmt.app
- (stmt.expr (atom.primitive_procedure "*"))
- args, s)
- (atom.number n, s)
-
-| application_primitive_div {s s' args args' n}
- (h_args : args_step (args, s) (args', s'))
- (heval: primitive_div args' = except.ok (atom.number n)):
- big_step
- (stmt.app
- (stmt.expr (atom.primitive_procedure "/"))
- args, s)
- (atom.number n, s)
-
-| application_primitive_eq {s s' args args' b}
- (h_args : args_step (args, s) (args', s'))
- (heval: primitive_eq args' = except.ok (atom.boolean b)):
- big_step
- (stmt.app
- (stmt.expr (atom.primitive_procedure "="))
- args, s)
- (atom.boolean b, s)
-
-| application_primitive_car {s s' args args' u}
- (h_args : args_step (args, s) (args', s'))
- (heval: primitive_car args' = except.ok u):
- big_step
- (stmt.app
- (stmt.expr (atom.primitive_procedure "car"))
- args, s)
- (u, s)
-
-| application_primitive_cdr {s s' args args' u}
- (h_args : args_step (args, s) (args', s'))
- (heval: primitive_cdr args' = except.ok u):
- big_step
- (stmt.app
- (stmt.expr (atom.primitive_procedure "cdr"))
- args, s)
- (u, s)
-
-| application_primitive_cons {s s' args args' u}
- (h_args : args_step (args, s) (args', s'))
- (heval: primitive_cons args' = except.ok u):
- big_step
- (stmt.app
- (stmt.expr (atom.primitive_procedure "cons"))
- args, s)
- (u, s)
-
-| application_primitive_null {s s' args args' u}
- (h_args : args_step (args, s) (args', s'))
- (heval: primitive_null args' = except.ok u):
- big_step
- (stmt.app
- (stmt.expr (atom.primitive_procedure "null?"))
- args, s)
- (u, s)
-
-| application_primitive_eqv {s s' args args' u}
- (h_args : args_step (args, s) (args', s'))
- (heval: primitive_null args' = except.ok u):
- big_step
- (stmt.app
- (stmt.expr (atom.primitive_procedure "eqv?"))
- args, s)
- (u, s)
-#+END_SRC
-
-#+BEGIN_EXPORT html
-
-#+END_EXPORT
-
-This is the simplest program I could think of to show that the program semantics are at least usable.
-
-#+BEGIN_SRC lean
-lemma var_lookup :
- big_step
- (stmt.var "x", [(λ x, none){"x" ↦ atom.number 1}])
- ((atom.number 1), [(λ x, none){"x" ↦ atom.number 1}]) :=
-begin
- apply big_step.var_deref,
- let my_state := [(λ x, none){"x" ↦ atom.number 1}],
- apply lookup_head,
- simp [state.update],
-end
-#+END_SRC
-
-This is a much more involved proof: that the factorial program at the top of this file is "correct," in the sense that it computes `int.factorial`.
-
-As you'll see, my approach to proving this statement involved many obligations, and ended up being very tedious. It's effectively the "intro to algorithms" proof of correctness for factorial, except that we're appealing to the big-step semantics above. By which I mean -- we're doing a rather poor job of leveraging the mathematical tools we just spent pages of code developing. Had I more time to work on this assignment, I might have naturally come to one of the refinement-based solutions, but I chose to be stubborn and just press forward.
-
-#+BEGIN_EXPORT html
-
-#+END_EXPORT
-
-#+BEGIN_SRC lean
-def nat.factorial : ℕ → ℤ
-| 0 := 1
-| (n + 1) := (n + 1) * (nat.factorial n)
-
-def int.factorial : ℤ → ℤ
-| (int.of_nat n) := nat.factorial n
-| (int.neg_succ_of_nat n) := nat.factorial (n + 1)
-
--- Would be trivial if there wasn't casting.
-lemma sub1_cast (n : ℕ) :
- primitive_sub [atom.number (↑n + 1), atom.number 1] = except.ok (atom.number ↑n) :=
-sorry
-
--- Would be trivial (unfold `int.factorial`) if there wasn't casting.
-lemma primitive_mul_fact (n : ℕ) :
- primitive_mul [atom.number (↑n + 1), atom.number (int.factorial ↑n)] = except.ok (atom.number (int.factorial ↑(nat.succ n))) :=
-sorry
-
--- Would be trivial if comparison was decidable.
-lemma factorial_program_compile_inner :
- (compile_stmt
- (atom.list
- [atom.symbol "if", atom.list [atom.symbol "=", atom.number 0, atom.symbol "x"], atom.number 1, atom.list
- [atom.symbol "*", atom.symbol "x", atom.list
- [atom.symbol "factorial", atom.list [atom.symbol "-", atom.symbol "x", atom.number 1]]]])) =
- some
- (stmt.ite (stmt.app (stmt.expr (atom.primitive_procedure "="))
- [stmt.expr (atom.number 0), stmt.var "x"])
- (stmt.expr (atom.number 1))
- (stmt.app (stmt.expr (atom.primitive_procedure "*"))
- [stmt.var "x",
- stmt.app (stmt.var "factorial")
- [stmt.app (stmt.expr (atom.primitive_procedure "-"))
- [stmt.var "x", stmt.expr (atom.number 1)]]])) :=
-sorry
-
--- For convenience -- the `factorial` function definition is pretty unwieldy to
--- be passing around in theorem statements.
-def define_factorial (s : list state) : list state :=
-list.cons ((λ _, none){"factorial" ↦
- (atom.compound_procedure (λ x, none) ["x"]
- (atom.list [
- (atom.symbol "if"),
- (atom.list [(atom.symbol "="), (atom.number 0), (atom.symbol "x")]),
- (atom.number 1),
- (atom.list [
- (atom.symbol "*"),
- (atom.symbol "x"),
- (atom.list [
- (atom.symbol "factorial"),
- (atom.list [
- (atom.symbol "-"),
- (atom.symbol "x"),
- (atom.number 1)])])])]))}) s
-
-lemma factorial_program_correct (n : ℕ) (s : list state) (arg : stmt)
- (h_eval_to_n : big_step
- (arg, define_factorial s)
- (atom.number n, define_factorial s)) :
- big_step
- (stmt.app (stmt.var "factorial") [arg], define_factorial s)
- (atom.number (int.factorial n), define_factorial s) :=
-begin
- let fundef :=
- (atom.compound_procedure (λ x, none) ["x"]
- (atom.list [
- (atom.symbol "if"),
- (atom.list [(atom.symbol "="), (atom.number 0), (atom.symbol "x")]),
- (atom.number 1),
- (atom.list [
- (atom.symbol "*"),
- (atom.symbol "x"),
- (atom.list [
- (atom.symbol "factorial"),
- (atom.list [
- (atom.symbol "-"),
- (atom.symbol "x"),
- (atom.number 1)])])])])),
- have h_lookup_factorial : lookup_var "factorial" (define_factorial s) = some fundef, by
- begin
- simp [define_factorial],
- apply lookup_head,
- simp [state.update],
- end,
- induction' n,
- { apply big_step.application,
- { apply big_step.var_deref,
- simp [h_lookup_factorial, fundef],
- apply and.intro,
- { refl, },
- { apply and.intro,
- { refl, },
- { refl, }}},
- { apply args_step.cons,
- { apply h_eval_to_n, },
- { apply args_step.nil, }},
- { exact factorial_program_compile_inner, },
- { apply big_step.ite_true,
- { apply big_step.application_primitive_eq,
- { apply args_step.cons,
- { apply big_step.self_evaluating, simp [is_lambda], },
- { apply args_step.cons,
- { apply big_step.var_deref,
- simp [new_frame],
- apply lookup_head,
- simp [state.update], },
- { apply args_step.nil, }}},
- { unfold primitive_eq, simp, }},
- { apply drop_two_frames,
- apply big_step.self_evaluating,
- simp [is_lambda], }}},
- { apply big_step.application,
- { apply big_step.var_deref,
- simp [h_lookup_factorial, fundef],
- apply and.intro,
- { refl, },
- { apply and.intro,
- { refl, },
- { refl, }}},
- { apply args_step.cons,
- { apply h_eval_to_n, },
- { apply args_step.nil, }},
- { exact factorial_program_compile_inner, },
- { apply big_step.ite_false,
- { apply big_step.application_primitive_eq,
- { apply args_step.cons,
- { apply big_step.self_evaluating, simp [is_lambda], },
- { apply args_step.cons,
- { apply big_step.var_deref,
- simp [new_frame],
- apply lookup_head,
- simp [state.update], },
- { apply args_step.nil, }}},
- { unfold primitive_eq,
- norm_cast, }},
- { apply drop_two_frames,
- apply big_step.application_primitive_mul,
- { apply args_step.cons,
- { apply big_step.var_deref,
- simp [new_frame, state.update],
- apply lookup_head,
- simp, },
- { apply args_step.cons,
- { have hsimp : ∀ (arg : stmt) (u : atom) (s : list state),
- big_step (arg, new_frame ["x"] [atom.number ↑(nat.succ n)] :: (λ (x : string), none) :: define_factorial s)
- (u, new_frame ["x"] [atom.number ↑(nat.succ n)] :: (λ (x : string), none) :: define_factorial s) ↔
- big_step (arg, define_factorial (new_frame ["x"] [atom.number ↑(nat.succ n)] :: (λ (x : string), none) :: define_factorial s))
- (u, define_factorial (new_frame ["x"] [atom.number ↑(nat.succ n)] :: (λ (x : string), none) :: define_factorial s)),
- by sorry, -- Nontrivial but obvious.
- rw hsimp,
- apply ih,
- { exact h_lookup_factorial, },
- { apply big_step.application_primitive_sub,
- { apply args_step.cons,
- { have hsimp₂ : lookup_var "x"
- (define_factorial
- (new_frame ["x"] [atom.number ↑(nat.succ n)] :: (λ (x : string), none) :: define_factorial s)) =
- lookup_var "x" (new_frame ["x"] [atom.number ↑(nat.succ n)] :: (λ (x : string), none) :: define_factorial s),
- by sorry, -- Nontrivial but obvious.
- apply big_step.var_deref,
- rw hsimp₂,
- simp [new_frame, state.update],
- apply lookup_head,
- simp, },
- { apply args_step.cons,
- { apply big_step.self_evaluating,
- simp [is_lambda], },
- { apply args_step.nil, }}},
- { apply sub1_cast, }}},
- { apply args_step.nil, }}},
- apply primitive_mul_fact, }}}
-end
-#+END_SRC
-
-#+BEGIN_EXPORT html
-
-#+END_EXPORT
-
-The =sorry= keyword lets you pretend to be Pierre de Fermat and say "this should be provable but I don't want to write the proof down." It's helpful in making some progress when you're working towards a deadline, but it completely violates the soundness of Lean's logic.
-
-I'm not sure how enlightening any of this is, but I think it does highlight how much goes into using these sorts of tools for program verification compared to the ease with which we used Alloy to check my answer to a homework problem.
-
-* What I Have Yet to Learn
-
-Quite a bit!
-
-I've alluded to a few things in the previous sections. I have much more to learn about the specification of programming language semantics, and how to apply data refinement in practice. I'm also interested in learning TLA+ and SPARK. They seem to meet somewhere in the middle of Alloy and Lean, which I expect to be the right fit for what I do professionally. I want to learn about the mathematics that underpins SMT, and the algorithms that enable fast SAT solving. I want to learn about how Lean works at a low-level, and the different approaches to encoding logic in a proof assistant.
-
-In short, I've barely scratched the surface. I know enough to be dangerous, but I have a ways to go before I'm the "domain expert" I strive to be.
-
-* Conclusions
-
-In this article, we've introduced what formal methods are and gained a cursory understanding of the techniques suited to "high-level" verification and "low-level" verification. "Formal methods" refers to the use of mathematical techniques to establish properties about software and verify that those properties hold true -- to provide a higher level of confidence to practitioners about the correctness of software than testing alone. Alloy and Forge are well-suited to working with systems at a high-level and leverage SAT solving to verify properties of interest. Lean, Isabelle, and Coq are well-suited to working with systems at a lower level, and work as a mechanization of mathematical logic: a proof in a proof assistant is equivalent to (but typically more formal than) a proof that a mathematician or computer scientist might write on a piece of paper.
-
-Now that I've got that out of my system, it's time to get back to keeping my head down and working on applying what I've learned to something useful. I hope to write about what I'm working on soon, but this blog can be a bit of a distraction, so I'll be taking a short break from writing for now. See you soon!
-
-* Appendix: Using the Tools
-
-Lean 3 is packaged in the Gentoo repositories, but Lean 4 is not. I have an ebuild for it in [[https://git.sr.ht/~jakob/zerodaysfordays][my overlay]] if you use Gentoo and you'd like to experiment with Lean 4.
-
-[[https://github.com/leanprover/lean-mode][lean-mode]] was great but [[https://github.com/leanprover/lean4-mode][lean4-mode]] forces you into using [[https://github.com/emacs-lsp/lsp-mode][lsp-mode]], which I don't like. (I much prefer [[https://github.com/joaotavora/eglot][eglot]].) I'm currently using [[https://github.com/akirak/lean4-mode/commits/modular][this fork]], which isolates the parts which are specific to =lsp-mode=. Then all I need to do is set =/usr/bin/lake serve= as the language server for =lean4-mode= in =eglot-server-programs= and add
-
-#+BEGIN_SRC elisp
-(defvar lean4-goal-buffer (get-buffer-create "*lean4-goal*"))
-
-(defun lean4-update-goal-buffer ()
- (when (eq 'lean4-mode major-mode)
- (jsonrpc-async-request
- (eglot--current-server-or-lose)
- :$/lean/plainGoal (eglot--TextDocumentPositionParams)
- :success-fn
- (lambda (&rest args)
- (let ((goals (seq-reduce #'concat (plist-get (car args) :goals) "")))
- (save-excursion
- (set-buffer lean4-goal-buffer)
- (erase-buffer)
- (insert goals))
- (message goals)))
- :error-fn
- (lambda (&rest args) (message (format "JSONrpc error %s" args))))))
-
-(defun lean4-update-goal-buffer-wrap ()
- (unless (or (window-minibuffer-p) (not (eq major-mode 'lean4-mode)))
- (lean4-update-goal-buffer)))
-
-(add-hook 'post-command-hook #'lean4-update-goal-buffer-wrap)
-#+END_SRC
-
-to my =init.el= and I get a goal buffer similar to the old lean-mode or Proof General.
-
----
-
-[fn:1] [[https://people.cs.umass.edu/~immerman/cs691/cs691.html][CS 691M]] was last offered in 1996. [[https://people.cs.umass.edu/~hconboy/class/2023Spring/CS520/][CS 520]] purportedly discusses "formal specification methods." If you read over the syllabus, you'll quickly understand that to be an empty claim. Perhaps I could have self-taught as part of an [[https://www.cics.umass.edu/content/undergraduate-independent-study-information][independent study]], but the department (at the time) didn't count independent study credits toward your graduation requirements, and I had another offer (with money involved) to do a REU in cryptography, so that's how I spent the limited time I had available to me.
-
-[fn:2] I've allowed myself to move the goalposts: my purpose is now to learn enough to demonstrate that there would be value in sending me back to school to get my Ph.D. and then truly become a domain expert!
-
-[fn:3] It's uncommon to include stochastic tests such as this one in a "test suite". It's desirable to have a test suite that always passes or always fails.
-
-[fn:4] One thing also worth noting is that being able to sleep at night /now/ doesn't necessarily mean you won't have to work on safety-critical or mission-critical software later on in your career. If you're merely a hobbyist, maybe these points aren't especially convincing to you.
-
-[fn:5] Jackson, D. (2002). [[https://homepage.cs.uiowa.edu/~tinelli/classes/181/Spring03/Readings/Jack02b.pdf][Alloy: a lightweight object modelling notation]]. ACM Transactions on software engineering and methodology (TOSEM), 11(2), 256-290.
-
-[fn:6] Boolean SATisfiability and Satisfiability Modulo Theories, respectively.
-
-[fn:7] Nelson, T., Barratt, C., Dougherty, D. J., Fisler, K., & Krishnamurthi, S. (2010, November). The Margrave Tool for Firewall Analysis. In LISA (Vol. 10, pp. 1-18).
-
-[fn:8] There is some risk involved in using a new tool that doesn't have a reputation of stability, but there has to be a critical mass of folks taking that risk and being at the forefront of using the tool to help it get a good reputation. I'm choosing to take that risk.
-
-[fn:9] To be clear: this wasn't my motivation to engage with a study of formal methods.
-
-[fn:10] In temporal mode, Forge always generates traces of infinite length, but there will be a loop somewhere within it.
-
-[fn:11] Even so, I'm covering only a small part of the problem, so I wouldn't expect this article to be that useful to someone trying to cheese a homework assignment.
-
-[fn:12] For more realistic examples of property testing in Scheme, see [[https://ngyro.com/software/guile-quickcheck.html][guile-quickcheck]].
diff --git a/org/Writeups for Dennis Yurichev's Reverse Engineering Challenges (#12-#22)/challenges-re-writeups-2.org b/org/Writeups for Dennis Yurichev's Reverse Engineering Challenges (#12-#22)/challenges-re-writeups-2.org
deleted file mode 100644
index 8eeff01..0000000
--- a/org/Writeups for Dennis Yurichev's Reverse Engineering Challenges (#12-#22)/challenges-re-writeups-2.org
+++ /dev/null
@@ -1,925 +0,0 @@
-#+TITLE: Writeups for Dennis Yurichev's Reverse Engineering Challenges (#12-#22)
-#+TAGS: writeup, reverse-engineering, x86
-#+DATE: <2019-05-28 Tue 15:18>
-#+HAUNT_BASE_DIR: /home/jakob/Blog/haunt/
-
-This is the second set of solutions for my self-imposed challenge of completing
-at least fifty of the exercises on Dennis Yurichev's [[https://challenges.re][challenges.re]] by the end of
-the year. The first set is available [[http:///jakob.space/challenges-re-writeups-1.html][here]].
-
-* Challenge #12
-
-No hints are given for this challenge, but it is the first time a binary is
-available in addition to the disassembly. I didn't download the executable, I
-was able to gather from the tags that the target is amd64 Linux.
-
-If later challenges also provide executables, I may use it as an opportunity to
-explore the NSA's newly-released [[https://www.nsa.gov/resources/everyone/ghidra/][Ghidra]]. At the time of writing this, Ghidra's
-source code has yet to be released, so I'll have to pass up the opportunity this
-time around.
-
-#+BEGIN_SRC c
-#include
-#include
-#include
-#include
-#include
-#include
-#include
-#include
-
-int main(int argc, char **argv)
-{
- // push rbx
- // mov rbx, rsi
- // sub rsp, 160
- int ret;
- struct stat sbuf;
- struct utimbuf tbuf;
-
- // cmp edi, 2
- // je .L2
- if (argc != 2) {
- // mov edi, OFFSET FLAT:.LC0
- // call puts
- puts("Usage: ");
- }
-
- // .L2:
- // mov rsi, QWORD PTR [rbx+8]
- // lea rdx, [rsp+16]
- // mov edi, 1
- // call __xstat
- ret = stat(argv[1], &sbuf);
-
- // test eax, eax
- // js .L10
- if (ret < 0) {
- // .L10:
- // mov edi, OFFSET FLAT:.LC1
- // call puts
- // xor edi, edi
- // call exit
- puts("error #1!");
- exit(0);
- }
-
- // mov rax, QWORD PTR [rsp+88]
- // xor edi, edi
- // mov QWORD PTR [rsp], rax
- tbuf.actime = sbuf.st_atim.tv_sec;
-
- // call time
- /// ...
- // mov QWORD PTR [rsp+8], rax
- tbuf.modtime = time(NULL);
-
- // mov rdi, QWORD PTR [rbx+8]
- // mov rsi, rsp
- // call utime
- ret = utime(argv[1], &tbuf);
-
- // test eax, eax
- // js .L11
- if (ret < 0) {
- // .L11:
- // mov edi, OFFSET FLAT:.LC2
- // call puts
- // xor edi, edi
- // call exit
- puts("error #2!");
- exit(0);
- }
-
- // add rsp, 160
- // xor eax, eax
- // pop rbx
- // ret
- return 0;
-}
-#+END_SRC
-
-The first thing that may stand out in the disassembly listing is =call __xstat=.
-=__xstat= isn't part of the C standard library or POSIX. My understanding of
-functions like these is that sometimes an interface like =stat= will result in a
-call to some internal libc routine when compiled, but the only time I've seen
-this before was with =__printf_chk=. Regardless, search engines are your friend,
-and you should have no trouble arriving at the [[http://refspecs.linuxbase.org/LSB_3.0.0/LSB-PDA/LSB-PDA/baselib-xstat-1.html][relevant page]] in the Linux
-Standard Base Specification. One interesting thing of note is the comment that
-"=ver= shall be =3= or the behavior of these functions is undefined," yet the
-disassembly indicates that =ver= is =1=. I'm doubtful that this is part of the
-challenge, though.
-
-I also just guessed that =QWORD PTR [rsp+88]= was =sbuf.st_atim.tv_sec=, given the
-context that the value is used in. Going from assembly to the corresponding
-fields of a struct is a pain without a tool, which is perhaps an indication that
-I should've downloaded the binary and used Ghidra^h^h^h^h^h^hradare2 to prod at
-it.
-
-Either way, the code updates a file's modification time. It's comparable to
-=touch=, but doesn't create the file if it doesn't exist. The strings are
-intentionally vague, so here's a cleaned up version:
-
-#+BEGIN_SRC c
-#include
-#include
-
-int main(int argc, char **argv)
-{
- struct stat sbuf;
- struct utimbuf tbuf;
-
- if (argc != 2) {
- printf("Usage: %s [path]\n", argv[0]);
- }
-
- if (stat(argv[1], &sbuf) < 0) {
- printf("%s: %s\n", argv[1], strerror(errno));
- exit(0);
- }
-
- tbuf.actime = sbuf.st_atim.tv_sec;
- tbuf.modtime = time(NULL);
-
- if (utime(argv[1], &tbuf) < 0) {
- printf("utime: %s\n", strerror(errno));
- exit(0);
- }
-
- return 0;
-}
-#+END_SRC
-
-* Challenge #13
-
-The question for this exercise is, "[w]hat does this SSE code do?" Uh oh. I
-don't know anything about SSE. Not the end of the world, though. I always
-appreciate an opportunity to learn. Here are some notes I took on chapter 25 of
-Yurichev's book:
-
-_Vectorization_ is the process of taking several arrays as input and producing a
-single array as output. SIMD (Single Instruction, Multiple Data) is a way of
-optimizing vectorization by doing certain array-level operations in parallel.
-
-Intel's initial implementation of SIMD reused FPU register. SSE added 128-bit
-registers (%xmm*) that were separate from the FPU, and AVX added 256-bit
-registers that were separate from the FPU.
-
-Well, that doesn't seem too complicated, and the exercise only uses two
-instructions: =movdqu=, which loads a 16-byte value from memory into an %xmm*
-register, and =pmaxub=, which calculates the maximum values between two %xmm*
-registers.
-
-#+BEGIN_SRC c
-void f(int *dest, int *a, int *b)
-{
- int i;
-
- // xor rax, rax
- // ...
- // add rax, 16
- // cmp rax, 1024
- // jne .L4
- // ...
- // .L4:
- for (i = 0; i < 256; i++) {
- // movdqu xmm0, XMMWORD PTR [rsi+rax]
- // movdqu xmm1, XMMWORD PTR [rdx+rax]
- // pmaxub xmm0, xmm1
- // movdqu XMMWORD PTR [rdi+rax], xmm0
- dest[i] = a[i] > b[i] ? a[i] : b[i];
- }
-
- // rep ret
- return;
-}
-#+END_SRC
-
-=f= will fill an array, =dest=, such that the element at each index contains the
-greater value between =a= and =b= for that index.
-
-* Challenge #14
-
-The challenge description explains that, "[n]ow that's easy," and gives both
-.NET and Java bytecode disassemblies. I am not familiar with either bytecode
-format, but I do know Java (unfortunately), so I went with that.
-
-#+BEGIN_SRC java
-public class Challenge14 {
- public static boolean f(char a) {
- // 0: iload_1
- // 1: bipush 97
- // 3: if_icmplt 14
- // 6: iload_1
- // 7: bipush 122
- // 9: if_icmpgt 14
- if (a < 97 || a > 122) {
- // 14: iload_1
- // 15: bipush 65
- // 17: if_icmplt 28
- // 20: iload_1
- // 21: bipush 90
- // 23: if_icmpgt 28
- if (a < 65 || a > 90) {
- // 28: iconst_0
- // 29: ireturn
- return false;
- }
-
- // 26: iconst_1
- // 27: ireturn
- return true;
- }
-
- // 12: iconst_1
- // 13: ireturn
- return true;
- }
-}
-#+END_SRC
-
-I'm not particularly confident in my translation -- the above is the result of
-skimming the [[https://en.wikipedia.org/wiki/Java_bytecode][Java bytecode]] and [[https://en.wikipedia.org/wiki/Java_bytecode_instruction_listings][Java bytecode instruction listings]] pages on
-Wikipedia -- but that translation does appear to convey a meaningful operation:
-telling whether or not =a= is an ASCII letter.
-
-* Challenge #15
-
-The challenge description explains that, "[n]ow that's really easy."
-
-#+BEGIN_SRC c
-void f(char *dst)
-{
- int i;
-
- // xorps %xmm0, %xmm0
- // movups %xmm0, 240(%rdi)
- // movups %xmm0, 224(%rdi)
- // movups %xmm0, 208(%rdi)
- // movups %xmm0, 192(%rdi)
- // movups %xmm0, 176(%rdi)
- // movups %xmm0, 160(%rdi)
- // movups %xmm0, 144(%rdi)
- // movups %xmm0, 128(%rdi)
- // movups %xmm0, 112(%rdi)
- // movups %xmm0, 96(%rdi)
- // movups %xmm0, 80(%rdi)
- // movups %xmm0, 64(%rdi)
- // movups %xmm0, 48(%rdi)
- // movups %xmm0, 32(%rdi)
- // movups %xmm0, 16(%rdi)
- // movups %xmm0, (%rdi)
- // ret
- for (i = 0; i < 256; i++) {
- dst[i] = '\0';
- }
-}
-#+END_SRC
-
-I initially read the disassembly for this challenge as if it were Intel syntax,
-but it's AT&T. The operation is simple: =f= zeroes out a 256-byte buffer specified
-by the first parameter.
-
-* Challenge #16
-
-Only one disassembly is given for this challenge, and the description hints that
-it is from Clang: "[n]ow this is getting harder. Clang did a lot of optimization
-tricks and this code is heavily optimized for SSE2. Nevertheless, the original
-function is tiny and simple. What does it do?"
-
-In all honesty, I don't think that a translation to C is helpful. As the problem
-mentioned, there's heavy optimization for SSE2, and the assembly code only
-tangentially corresponds to what (I believe) is going on. Instead, I'll attempt
-to justify my partial conclusion that =f= sums an array of integers.
-
-Bytes from =rdi= (indexed with =rcx=) are interleaved into =xmm0= and =xmm2= with
-=pinsrw=, and continually added into =xmm3= and =xmm4=. Then, =xmm0= and =xmm2= are added,
-and =xmm1= is unpacked with =punpckhqdq xmm1, xmm1=. The pseudocode for the
-=punpckhqdq= instruction is given as:
-
-#+BEGIN_SRC c
-Destination[0..63] = Destination[64..127];
-Destination[64..127] = Source[64..127];
-#+END_SRC
-
-So it's unusual to see =xmm1= as both the "Source" and "Destination". This is
-followed by a =paddq xmm1, xmm0=.
-
-I can't really confirm any of this because of the =movdqa xmm1, xmmword ptr
-[rip + .LCPI0_0]= instruction. Some sort of mask is being used in those =pand
-xmm0, xmm1= and =pand xmm2, xmm1= instructions, and I suspect that it's one of many
-tricks coming together so the function works for an array of _integers_, but we
-aren't given =.LCPI0_0=, so I can't tell for sure.
-
-This also means that I can't assemble what's given. If anyone out there is
-experienced in SIMD and would to share some tips for making sense of this one,
-I'd really appreciate it.
-
-* Challenge #17
-
-The description explains that "[t]his is a quite esoteric piece of code, but
-nevertheless, the task it does is very mundane and well-known to anyone. The
-function has 4 32-bit arguments and returns a 32-bit one."
-
-#+BEGIN_SRC c
-int f(int a, int b, int c, int d)
-{
- int tmp1, tmp2;
-
- // sub edx, edi
- c -= a;
-
- // mov r8d, ecx
- // ...
- // sub r8d, esi
- tmp1 = d - b;
-
- // mov ecx, 63
- d = 63;
-
- // mov eax, edx
- // sar eax, cl
- // and eax, edx
- tmp2 = (c >> (d & 0xff)) & c;
-
- // mov edx, r8d
- // sar edx, cl
- // ...
- // and edx, r8d
- c = (tmp1 >> (d & 0xff)) & tmp1;
-
- // add edi, eax
- a += tmp2;
-
- // add esi, edx
- // sub esi, edi
- b += c - a;
-
- // mov eax, esi
- // sar eax, cl
- // and eax, esi
- // add eax, edi
- // ret
- return ((b >> (d & 0xff)) & b) + a;
-}
-#+END_SRC
-
-The initial translation is quite messy, but observe that =d= has a constant value
-of =63=, and =63 & 0xff= is just =63=. Still, there are a number of snippets that look
-like =(c >> (d & 0xff)) & c=, and it isn't obvious what that does.
-
-#+BEGIN_SRC c
-int black_box(int a)
-{
- return (a >> 63) & a;
-}
-
-int main(void)
-{
- int i;
-
- for (i = 0; i >= 0; i += 1) {
- if (black_box(i) != 0) {
- printf("black_box(%d) = %d\n", i, black_box(i));
- }
- }
-
- for (i = 0; i <= 0; i -= 1) {
- if (black_box(i) != i) {
- printf("black_box(%d) = %d\n", i, black_box(i));
- }
- }
-
-
- return 0;
-}
-#+END_SRC
-
-#+BEGIN_SRC
-re.c: In function 'black_box':
-re.c:64:13: warning: right shift count >= width of type [-Wshift-count-overflow]
- return (a >> 63) & a;
- ^~
-#+END_SRC
-
-I'm not sure if this is the intended behavior, but on amd64, this acts as
-\(min(x, 0)\). A first step at simplification can be made.
-
-#+BEGIN_SRC c
-#define MIN(a, b) (a < b ? a : b)
-
-int f(int a, int b, int c, int d)
-{
- a += MIN(c - a, 0);
- c = MIN(d - b, 0);
- b += c - a;
- return MIN(b, 0) + a;
-}
-#+END_SRC
-
-And this can be further cleaned up into a one-liner.
-
-#+BEGIN_SRC c
-#define MIN(a, b) (a < b ? a : b)
-
-int f(int a, int b, int c, int d)
-{
- return a + \
- MIN(b - a + MIN(d - b, 0) - MIN(c - a, 0), 0) + \
- MIN(c - a, 0);
-}
-#+END_SRC
-
-And this happens to be an interesting implementation of \(min(a, b, c, d)\).
-
-* Challenge #18
-
-For challenges with more complicated control flow, I've been drawing the basic
-blocks out on a sheet of paper and drawing arrows between them to identify which
-transitions represent loops, and which transitions represent conditionals. That
-didn't work particularly well for this challenge, though. The solution instead
-came to me instead by just staring at the disassembly for some time.
-
-#+BEGIN_SRC c
-#include
-#include
-#include
-#include
-
-int f3(char *a, uint64_t *b, uint64_t *c, uint64_t *d, uint64_t *e, uint64_t *f)
-{
- int i;
- char *cur;
-
- if (strlen(a) != 36) {
- return a;
- }
-
- cur = a;
- i = 0;
-
- while (i != 37) {
- if (i == 8 || i == 13 || i == 18 || i == 23) {
- if (*cur != '-') {
- return (char *) -1;
- }
- } else {
- if (i == 36 && *cur == '\0') {
- break;
- }
-
- if (!isxdigit(*cur)) {
- return (char *) -1;
- }
- }
-
- i++;
- cur++;
- }
-
- *b = strtoul(a, NULL, 16);
- *c = strtoul(a + 9, NULL, 16);
- *d = strtoul(a + 14, NULL, 16);
- *e = strtoul(a + 19, NULL, 16);
- *f = strtoull(a + 24, NULL, 16);
- return 0;
-}
-#+END_SRC
-
-The code appears to implement a [[https://en.wikipedia.org/wiki/Universally_unique_identifier][UUID]] parser.
-
-* Challenge #19
-
-This challenge was particularly difficult. I began by translating the individual
-basic blocks to C, and connecting them with =goto=.
-
-#+BEGIN_SRC c
-#include
-#include
-
-char *f2_bb(char *a, int b, int c, char *d)
-{
- // rax <- a
- // rbx <- a
-
- // QWORD PTR [rsp+24] <- d
- // QWORD PTR [rsp+16] <- b
- // QWORD PTR [rsp+8] <- c
-
- int i;
- int j;
- int k;
- int *ret;
-
- // f2:
- {
- // test rcx, rcx
- // jne .L21
- if (c == 0) {
- // add rsp, 32
- // pop rbx
- // ret
- return a;
- }
-
- goto BBL21;
- }
-
- // .L21:
- {
- BBL21:
- // lea rdi, [4+rcx*4]
- // ...
- // call malloc
- ret = malloc(c * 4 + 4);
-
- // ...
- // mov DWORD PTR [rax], -1
- ret[0] = -1;
-
- // ...
- // mov DWORD PTR [rax+4], 0
- ret[1] = 0;
-
- // mov r9d, 1
- i = 1;
-
- // ...
- // cmp r9, rcx
- // je .L22
- if (c == 1) {
- goto BBL22;
- }
-
- goto BBL8;
- }
-
- // .L8:
- {
- BBL8:
- // mov edi, DWORD PTR [rax+r9*4]
- // lea r8d, [rdi+1]
- // test r8d, r8d
- // mov DWORD PTR [rax+4+r9*4], r8d
- if ((ret[i + 1] = ret[i] + 1) <= 0) {
- // jle .L5
- goto BBL5;
- }
-
- // movzx r10d, BYTE PTR [rdx+r9]
- // movsx r8, r8d
- // cmp r10b, BYTE PTR [rdx-1+r8]
- if (d[i] != d[ret[i + 1] - 1]) {
- // jne .L7
- goto BBL7;
- }
-
- // jmp .L5
- goto BBL5;
- }
-
- // .L7:
- {
- BBL7:
- // mov r8d, DWORD PTR [rax-4+r8*4]
- // add r8d, 1
- // test r8d, r8d
- // mov DWORD PTR [rax+4+r9*4], r8d
- if ((ret[i + 1] = ret[ret[i + 1] - 1] + 1) > 0) {
- // jg .L23
- goto BBL23;
- }
-
- goto BBL5;
- }
-
- // .L23:
- {
- BBL23:
- // movsx r8, r8d
- // cmp BYTE PTR [rdx-1+r8], r10b
- if (d[ret[i + 1] - 1] == ret[i]) {
- // je .L5
- goto BBL5;
- }
-
- goto BBL7;
- }
-
- // .L5:
- {
- BBL5:
- // add r9, 1
- // cmp r9, rcx
- if (++i != c) {
- // jne .L8
- goto BBL8;
- }
-
- goto BBL22;
- }
-
- // .L22:
- {
- BBL22:
- // xor r8d, r8d
- // xor r10d, r10d
- // xor edi, edi
- i = j = k = 0;
- goto BBL9;
- }
-
- // .L9:
- {
- BBL9:
- // cmp rdi, rsi
- // jae .L24
- if (j >= b) {
- goto BBL24;
- }
-
- goto BBL14;
- }
-
- // .L14:
- {
- BBL14:
- // test r8d, r8d
- if (i < 0) {
- // js .L10
- goto BBL10;
- }
-
- // movsx r9, r8d
- // movzx r11d, BYTE PTR [rdx+r9]
- // cmp BYTE PTR [rbx+rdi], r11b
- if (d[i] == a[j]) {
- // je .L10
- goto BBL10;
- }
-
- // cmp rdi, rsi
- // mov r8d, DWORD PTR [rax+r9*4]
- i = ret[i];
-
- if (j < b) {
- // jb .L14
- goto BBL14;
- }
-
- goto BBL24;
- }
-
- // .L10:
- {
- BBL10:
- // add r8d, 1
- // add r10d, 1
- // movsx rdi, r8d
- j = ++i;
- k++;
-
- // cmp rdi, rcx
- if (j == c) {
- // je .L18
- goto BBL18;
- }
-
- // movsx rdi, r10d
- j = k;
-
- // jmp .L9
- goto BBL9;
- }
-
- // .L18:
- {
- BBL18:
- // movsx r10, r10d
- // sub r10, rcx
- k -= c;
-
- // add rbx, r10
- a += k;
-
- // jmp .L13
- goto BBL13;
- }
-
-
- // .L24:
- {
- BBL24:
- // xor ebx, ebx
- a = NULL;
- goto BBL13;
- }
-
- // .L13:
- {
- BBL13:
- // mov rdi, rax
- // call free
- free(ret);
-
- // add rsp, 32
- // mov rax, rbx
- // pop rbx
- // ret
- return a;
- }
-
-}
-#+END_SRC
-
-#+BEGIN_SRC c
-char *f2(char *a, int b, int c, char *d)
-{
- int i;
- int j;
- int k;
- int *ret;
-
- if (c == 0) {
- return a;
- }
-
- ret = malloc((c + 1) * sizeof(int));
- ret[0] = -1;
- ret[1] = 0;
-
- i = 1;
-
- do {
- if ((ret[i + 1] = ret[i] + 1) > 0
- && d[i] != d[ret[i] - 1]) {
- while ((ret[i + 1] = ret[ret[i + 1] - 1] + 1) > 0) {
- if (d[ret[i + 1] - 1] == ret[i]) {
- break;
- }
- }
- }
- } while (++i < c);
-
- i = j = k = 0;
-
- while (j < b) {
- if (i < 0 || d[i] == a[j]) {
- j = ++i;
- k++;
-
- if (j == c) {
- free(ret);
- return a + k - c;
- }
-
- j = k;
- }
- i = ret[i];
- }
-
- free(ret);
- return NULL;
-}
-#+END_SRC
-
-This challenge was nightmarishly difficult. I plan to come back to it near the
-end of the year, but for now, consider this challenge incomplete. I've been
-banging my head against a wall trying to make sense of it for a number of weeks
-now, and I still don't have a good answer for what it does.
-
-* Challenge #20
-
-Another challenge described as "easy." This time, it really is.
-
-#+BEGIN_SRC c
-#include
-
-float f4()
-{
- return rand() * ((float) 4.65661287307739257813e-10);
-}
-#+END_SRC
-
-I did defer to an ISA reference for =cvtsi2ss= and =mulss= as I'm not particularly
-familiar with x86's floating point instructions. This challenge also gave me an
-opportunity to use [[https://float.exposed/0x30000000][float.exposed]] to turn =.long 805306368= into a floating point
-constant, but \(4.65661287307739257813 \cdot 10^{-10}\) isn't any more
-comprehensible. The purpose of =f4= is clearer when observing the output.
-
-#+BEGIN_SRC prog
-...
-0.086556
-0.535690
-0.176955
-0.791683
-0.575702
-0.418118
-0.952373
-...
-#+END_SRC
-
-=f4= returns a random floating point number on the range \([0, 1]\).
-
-* Challenge #21
-
-I was able to complete the translation for this challenge in under five minutes,
-which I'm quite proud of.
-
-#+BEGIN_SRC c
-#include
-
-int f1(char *a, char *b)
-{
- // rbp <- a
- // rbx <- b
-
- int offset;
-
- // push r12
- // push rbp
- // mov rbp, rdi
- // push rbx
- // mov rbx, rsi
- // call strlen
- // mov rdi, rbx
- // mov r12, rax
- // call strlen
- // sub r12, rax
- offset = strlen(a) - strlen(b);
-
- // mov rsi, rbx
- // lea rdi, [rbp+0+r12]
- // call strcmp
- // pop rbx
- // test eax, eax
- // pop rbp
- // sete al
- // pop r12
- // ret
- return strcmp(a + offset, b) ? 1 : 0;
-}
-#+END_SRC
-
-=f= is a simple "ends with" predicate function. It returns =1= if =a= ends with the
-substring =b=.
-
-* Challenge #22
-
-I stopped when I got to the =// ...=. I'd figured it out by then, and =-Os= made the
-assembly for this quite messy.
-
-#+BEGIN_SRC c
-int f2(int *a, int b, int *c, int d)
-{
- // rcx <- a[b]
- // eax <- d + 1
- // ebp <- c[0]
-
- int i; // r8
- int j;
- int *cur;
-
- i = d + 1;
- j = 0;
-
- while (j < i){
- while (c[j + 1] <= c[0] && j < d)
- j++;
-
- cur = &a[i - 1];
- while (*cur-- > c[0]);
-
- if (j < i) {
- c[j + 1] ^= *(cur + 1);
- *cur ^= *(cur + 1);
- c[j + 1] ^= *cur;
- }
- }
-
- c[0] ^= *(cur + 1);
- // ...
-
- return 0;
-}
-
-void f1(int *a, int b, int *c, int d)
-{
- int ret;
-
- while (b < d) {
- ret = f2(a, b, c, d);
- f1(a, b, c, ret - 1);
- b = ret + 1;
- }
-}
-#+END_SRC
-
-The hint for this challenge is that "[t]his can be tricky, but the algorithm is
-well known and heavily used almost everywhere," which gave it away once I got to
-the mess of =xor= instructions. This is the [[https://en.wikipedia.org/wiki/XOR_swap_algorithm][XOR swap algorithm]], extended so that
-it reverses the contents of =a= and =c=.
-
-#+BEGIN_EXPORT html
-
-#+END_EXPORT
diff --git a/org/Writeups for Dennis Yurichev's Reverse Engineering Challenges (#2-#11)/challenges-re-writeups-1.org b/org/Writeups for Dennis Yurichev's Reverse Engineering Challenges (#2-#11)/challenges-re-writeups-1.org
deleted file mode 100644
index 5450a4a..0000000
--- a/org/Writeups for Dennis Yurichev's Reverse Engineering Challenges (#2-#11)/challenges-re-writeups-1.org
+++ /dev/null
@@ -1,1238 +0,0 @@
-#+TITLE: Writeups for Dennis Yurichev's Reverse Engineering Challenges (#2-#11)
-#+DATE: <2019-03-10 Sun>
-#+TAGS: writeup, reverse-engineering, arm, x86
-
-As mentioned in the (now deleted) post I wrote describing my plans for 2019, one
-of my goals this year is to get through at least 50 of the exercises on Dennis
-Yurichev's [[https://challenges.re/][challenges.re]]. I've decided to document my progress in the form of
-writeups for the challenges I complete, batched in sets of ten exercises. For
-each challenge, I'll try to explain the intuitions that brought me closer to
-answering the recurring question from Yurichev, "[w]hat does this code do?"
-
-* Challenge #2
-
-In nearly all of the challenges available on the site, we're given equivalent
-disassembly listings of a function, =f=, as generated by different compilers on
-different processor architectures, and we're asked to describe what the code
-does. For now, I've decided to take it easy and only pay attention to the
-disassemblies for GCC on x86, as that's what I've done the most work with. We
-aren't given a target operating system, but I think it's reasonable to assume
-that the x86 code uses the [[https://en.wikipedia.org/wiki/X86_calling_conventions#cdecl][cdecl calling convention]].
-
-Although I stayed within my comfort zone in terms of instruction set
-architecture, I refrained from my usual habit of converting the disassembly
-listing to AT&T syntax for once.
-
-#+BEGIN_EXPORT html
-
-
-
-#+END_EXPORT
-
-Below is a rough translation of the disassembly listing to C. My process is
-relatively unchanged from the workflow I described in an [[http://jakob.space/blog/decompilation-by-hand.html][older post]].
-
-#+BEGIN_SRC c :hl_lines 0
-unsigned f(unsigned a)
-{
- // mov eax,DWORD PTR [esp+0x4]
- // bswap eax
- a = ((a & 0xff) << 24)
- | ((a & 0xff00) << 8)
- | ((a & 0xff0000) >> 8)
- | ((a & 0xff000000) >> 24);
-
- // mov edx,eax
- // and eax,0xf0f0f0f
- // and edx,0xf0f0f0f0
- // shr edx,0x4
- // shl eax,0x4
- // or eax,edx
- a = ((a & 0xf0f0f0f) << 4) | ((a & 0xf0f0f0f0) >> 4);
-
- // mov edx,eax
- // and eax,0x33333333
- // and edx,0xcccccccc
- // shr edx,0x2
- // shl eax,0x2
- // or eax,edx
- a = ((a & 0x33333333) << 2) | ((a & 0xcccccccc) >> 2);
-
- // and eax,0x55555555
- // and edx,0xaaaaaaaa
- // add eax,eax
- // shr edx,1
- // or eax,edx
- a = ((a & 0x55555555) << 1) | ((a & 0xaaaaaaaa) >> 1);
-
- // ret
- return a;
-}
-#+END_SRC
-
-I think it should make sense that =add eax,eax= is mathematically equivalent to
-=imul eax, 2=, but it takes another step to see that it's [[https://math.stackexchange.com/questions/1610667/why-shifting-left-1-bit-is-the-same-as-multiply-the-number-by-2][equivalent]] to =shl eax,1=,
-which is represented in the C code as =<< 1=. This isn't terribly complicated, but
-it's an optimization detail that some might not be familiar with. =bswap= is an
-instruction I was unfamiliar with, so I consulted my [[https://c9x.me/x86/html/file_module_x86_id_21.html][favorite x86 reference]]. It
-converts the endianness of the word in the register. If you don't know what that
-means, I'd suggest you read the page in the ISA reference.
-
-The code seems nonsensical at first, but we can compile it and inspect the
-output given some test values.
-
-#+BEGIN_SRC c :hl_lines 0
-#include
-
-void main(void)
-{
- unsigned i;
-
- for (i = 0; i <= 256; i++) {
- printf("%010u %08x\n", i, i);
- printf("%010u %08x\n", f(i), f(i));
- printf("\n");
- }
-}
-#+END_SRC
-
-Which produces:
-
-#+BEGIN_SRC
-0000000000 00000000
-0000000000 00000000
-
-0000000001 00000001
-2147483648 80000000
-
-0000000002 00000002
-1073741824 40000000
-
-0000000003 00000003
-3221225472 c0000000
-
-0000000004 00000004
-0536870912 20000000
-...
-#+END_SRC
-
-What's happening might not be immediately obvious, but there's a pattern in the
-column of input/output represented in hexadecimal. Let's have a look at the
-binary representations of a few pairs:
-
-#+BEGIN_SRC python
-bin(0x00000001) # --> '0b00000000000000000000000000000001'
-bin(0x80000000) # --> '0b10000000000000000000000000000000'
-
-bin(0x00000003) # --> '0b00000000000000000000000000000011'
-bin(0xc0000000) # --> '0b11000000000000000000000000000000'
-
-# ...
-
-bin(0x0000004d) # --> '0b00000000000000000000000001001101'
-bin(0xb2000000) # --> '0b10110010000000000000000000000000'
-#+END_SRC
-
-My answer to the question is that =f= reverses the bits of the word it is given.
-
-* Challenge #3
-
-This time, we're given an array of 64 32-bit integers and a hint that "[t]he
-algorithm is well-known, but I've changed [the] constant so it wouldn't be
-googleable."
-
-#+BEGIN_SRC c :hl_lines 0
-int f(unsigned n)
-{
- unsigned a, b;
-
- // mov edx, edi
- // shr edx
- // or edx, edi
- // mov eax, edx
- a = b = (n >> 1) | n;
-
- // shr eax, 2
- // or eax, edx
- // mov edx, eax
- a = b = (a >> 2) | b;
-
- // shr edx, 4
- // or edx, eax
- // mov eax, edx
- a = b = (b >> 4) | a;
-
- // shr eax, 8
- // or eax, edx
- // mov edx, eax
- a = b = (a >> 8) | b;
-
- // shr edx, 16
- // or edx, eax
- b = (b >> 16) | a;
-
- // imul eax, edx, 79355661 ; 0x4badf0d
- // shr eax, 26
- a = (b * 0x4badf0d) >> 26;
-
- // mov eax, DWORD PTR v[0+rax*4]
- // ret
- return v[a];
-}
-#+END_SRC
-
-The first thing that stood out to me was the presence of =-1= in the array of
-integers. Testing from =0= to =UINT_MAX=, the only =n= that returns =-1= is =0=.
-Interesting. It's also worth noting that the array contains every integer from
-0, 31, so this function is using /some rule/ to map the input space onto [0, 31].
-
-If we inspect the values of =f= for test values from =0= to =UINT_MAX=:
-
-#+BEGIN_SRC :hl_lines 0
- f(1) = 31
- f(2) = 30
- f(3) = 30
- f(4) = 29
- f(5) = 29
- f(6) = 29
- f(7) = 29
- f(8) = 28
- f(9) = 28
-f(10) = 28
-f(11) = 28
-f(12) = 28
-f(13) = 28
-f(14) = 28
-f(15) = 28
-f(16) = 27
-f(17) = 27
-f(18) = 27
-f(19) = 27
-f(20) = 27
-f(21) = 27
-f(22) = 27
-f(23) = 27
-f(24) = 27
-f(25) = 27
-f(26) = 27
-f(27) = 27
-f(28) = 27
-f(29) = 27
-f(30) = 27
-f(31) = 27
-#+END_SRC
-
-There's a pattern of exponential growth here -- every result occurs twice as
-frequently as the previous result. Mathematically, this is \(31 - [log_2(n)]\)
-where the brackets represent the Greatest Integer Function (\(f(x)\) returning
-the largest integer less than or equal to \(x\)). This can be verified by
-comparing the result of =f= to the following function for some test values:
-
-#+BEGIN_SRC c :hl_lines 0
-int my_f(unsigned n)
-{
- return 31 - ((int) (log(n) / log(2)));
-}
-#+END_SRC
-
-* Challenge #4
-
-This time around we're given an additional question to answer: "Some versions
-have the =0x1010101= constant, some do not. Why?" I decided that I'd reverse the
-x86 disassembly first, and then compare it to the other architectures.
-
-#+BEGIN_SRC c :hl_lines 0
-unsigned f(unsigned a)
-{
- // mov edx,edi
- // shr edx,1
- // and edx,0x55555555
- // sub edi,edx
- a -= ((a >> 1) & 0x55555555);
-
- // mov eax,edi
- // shr edi,0x2
- // and eax,0x33333333
- // and edi,0x33333333
- // add edi,eax
- a = (a & 0x33333333) + ((a >> 2) & 0x33333333);
-
- // mov eax,edi
- // shr eax,0x4
- // add eax,edi
- // and eax,0xf0f0f0f
- // imul eax,eax,0x1010101
- // shr eax,0x18
- // ret
- return (((a + (a >> 4)) & 0xf0f0f0f) * 0x1010101) >> 0x18
-}
-#+END_SRC
-
-The past few challenges have shown us that a good way of reversing these
-bit-twiddling functions is to test a few input values and look at the binary
-representations of the input and output values.
-
-#+BEGIN_SRC
- In: 00000000
-Out: 0
-
- In: 00000001
-Out: 1
-
- In: 00000010
-Out: 1
-
- In: 00000011
-Out: 2
-
-...
-
- In: 00001100
-Out: 2
-
- In: 00001101
-Out: 3
-
- In: 00001110
-Out: 3
-
- In: 00001111
-Out: 4
-#+END_SRC
-
-It doesn't take much effort to see that the function is counting the number of
-bits set in the input. This was particularly interesting to me as I was asked to
-derive this algorithm for a past job interview (though I wasn't able to in the
-time given).
-
-This falls apart for numbers larger than =0xff=, however. It returns the number of
-bits plus some constant that changes depending on which bits in the higher bytes
-are set. I'll assume that =f= is only meant to be called with 8-bit integers.
-
-With that, we can move onto the second question. The disassemblies for x86,
-ARM64, and Thumb have the =0x1010101= constant, while the disassemblies for ARM
-and MIPS do not.
-
-Returning to the strategy of inspecting binary representations:
-
-#+BEGIN_SRC
-00000000 00000000 00000000 00000000
-00000000 00000000 00000000 00000000
-
-00000000 00000000 00000000 00000001
-00000001 00000001 00000001 00000001
-
-00000000 00000000 00000000 00000010
-00000010 00000010 00000010 00000010
-
-...
-
-00000000 00000000 00000000 00010000
-00010000 00010000 00010000 00010000
-
-00000000 00000000 00000000 00010001
-00010001 00010001 00010001 00010001
-
-00000000 00000000 00000000 00010010
-00010010 00010010 00010010 00010010
-
-...
-
-00000000 00000000 00000000 11111101
-11111101 11111101 11111101 11111101
-
-00000000 00000000 00000000 11111110
-11111110 11111110 11111110 11111110
-
-00000000 00000000 00000000 11111111
-11111111 11111111 11111111 11111111
-#+END_SRC
-
-It would appear that multiplying a 32-bit integer by =0x1010101= propagates the
-low byte to the three bytes above it. This makes sense when you notice that the
-multiplication is paired with a =shr= of =0x18= -- moving the highest byte into the
-lowest byte.
-
-Though, this doesn't really answer the question. What difference is there
-between the architectures that use the =0x1010101= and the architectures that
-don't? ARM and MIPS still do a shift by =0x18=, so what's going on?
-
-Looking at the ARM example, the instructions around the shift are:
-
-#+BEGIN_SRC asm :hl_lines 0
-ADD r0,r0,r0,LSL #16
-ADD r0,r0,r0,LSL #8
-LSR r0,r0,#24
-#+END_SRC
-
-For MIPS, it looks like:
-
-#+BEGIN_SRC asm :hl_lines 0
-sll $3,$2,8
-addu $2,$3,$2
-sll $3,$2,16
-addu $2,$2,$3
-j $31
-srl $2,$2,24
-#+END_SRC
-
-Both of these (humor me, I know the orders are different) are equivalent to:
-
-#+BEGIN_SRC c :hl_lines 0
-a = (a << 8) + a;
-a = (a << 16) + a;
-a >> 24;
-#+END_SRC
-
-And, with some test values, we can see that this is equivalent to multiplication
-by =0x1010101= and shifting by 24.
-
-#+BEGIN_SRC c :hl_lines 0
-unsigned a(unsigned n)
-{
- n = (n << 8) + n;
- n = (n << 16) + n;
- return n >> 24;
-}
-
-unsigned b(unsigned n)
-{
- return (n * 0x1010101) >> 24;
-}
-
-void main(void)
-{
- for (unsigned i = 0; i < UINT_MAX; i++) {
- if (a(i) != b(i)) {
- printf("%u\n", i);
- }
- }
-}
-#+END_SRC
-
-I suspect the reason it doesn't show up in the ARM or MIPS disassemblies is due
-to the fixed-width instruction encoding. The compiler likely decided it would be
-less efficient to work with the =0x1010101= constant than to break it up into a
-pair of shifts and additions.
-
-* Challenge #5
-
-This is the first challenge we're given that has loops and conditionals, as
-indicated by the telltale labels starting with ".L". Another initial observation
-is that the first instruction in =f= operates on =%rsi=, and the third operates on
-=%rcx=, so it's very likely that this function has four parameters.
-
-Translation to C is more involved than it was with the previous challenges, but
-it is valuable as it makes the purpose of =f= very clear. In lieu of an analysis
-of inputs and outputs, I'll provide a few notes on the process of translation.
-First, =cmp= gave me a bit of trouble as I've been out of practice for some time
-and the difference between AT&T and Intel syntax threw me for a loop.
-Fortunately, the [[https://en.wikibooks.org/wiki/X86_Assembly/Control_Flow#Comparison_Instructions][wikibooks]] for x86 assembly covers this in detail. In AT&T
-syntax, the order is =cmp subtrahend, minuend=, while in Intel syntax, the order
-is =cmp minuend, subtrahend=. The subtrahend is subtracted from the minuend, so,
-in Intel syntax, =cmp rcx, rsi; ja .L10= will jump if =%rcx= is greater than =%rsi=.
-
-Looking further into the function, there is some dereferencing with =BYTE PTR=,
-which tipped me off that this was probably a function operating on a string.
-
-There's a curious =push rbx=, followed by a =pop rbx= before the =ret=. I ignored this
-initially, taking it to be register preservation. It was. An intuition of what's
-worth ignoring is valuable in reverse engineering.
-
-Upon reaching =.L16=, there are a lot of registers in use. It helped to look at
-each register in isolation and see how they were used. For example, =%r10= is used
-in the following instructions: =xor r10d, r10d=, =add r10, 1=, =lea rax, [rdi+r10]=,
-and =cmp r10, r11=. This is very typical of a for-loop counter. =%r9= on the other
-hand only shows up in two instructions: =mov r9d, 1=, and =cmovne r8d, r9d=. =%r9= is
-just used as a source of 1 for =cmovne=, since there are no encodings for =cmovne=
-that have an immediate source.
-
-=cmovne= was unfamiliar to me, so I did look it up in my favorite [[https://c9x.me/x86/html/file_module_x86_id_34.html][x86 reference]].
-It's a conditional move. =movz= was similarly unfamiliar. It simply loads =%bl= with
-the source byte and zeroes out the higher portions of the register.
-
-#+BEGIN_SRC c :hl_lines 0
-char *f(char *a, unsigned b, char *c, unsigned d)
-{
- // cmp rcx, rsi
- // ja .L10
- if (d >= b) {
- // .L10:
- // xor eax, eax
- // ret
- return NULL;
- }
-
-
- // sub rsi, rcx
- // add rsi, 1
- // mov r11, rsi
- b = b - d + 1;
-
- // je .L10
- if (b == 0) {
- // .L10:
- // xor eax, eax
- // ret
- return NULL;
- }
-
- // test rcx, rcx
- // jne .L16
- // mov rax, rdi
- // ret
- if (d == 0) {
- return a;
- }
-
- // .L16:
- // push rbx
- // xor r10d, r10d
- // mov r9d, 1
- // ...
- // cmp r10, r11
- // jne .L4
- for (int i = 0; i != b; i++) {
- // xor r8d, r8d
- unsigned ret = 0;
-
- // .L4:
- // lea rax, [rdi+r10]
- // xor esi, esi
- // ...
- // add rsi, 1
- // cmp rsi, rcx
- // jne .L8
- for (int j = 0; j != d; j++) {
- // movzx ebx, BYTE PTR [rdx+rsi]
- // cmp BYTE PTR [rax+rsi], bl
- // cmovne r8d, r9d
- if (a[i] != c[j]) {
- ret = 1;
- }
- }
-
- // test r8d, r8d
- // je .L12
- if (!ret) {
- // .L12:
- // pop rbx
- // ret
- return a + i;
- }
- }
-
- // xor eax, eax
- // pop rbx
- // ret
- return NULL;
-}
-#+END_SRC
-
-The variable names I chose are pretty opaque, but if you stare at this long
-enough, it should be pretty clear that =f= returns the offset of =c= in =a=. =b= and =d=
-are just the lengths of =a= and =c= respectively.
-
-* Challenge #6
-
-An additional hint given for this exercise is that, "[t]his is one of the
-simplest exercises I made, but still this code can be served as useful library
-function and is certainly used in many modern real-world applications." I'll
-leave the relative addresses in my annotations of the disassembly, as it appears
-to be PIC.
-
-For the sake of showing the mapping between assembly instructions and C code,
-I'll first give a translation that uses =goto=, followed by a cleaned up version.
-
-#+BEGIN_SRC c
-// 0: push rbp
-// 1: mov rbp,rsp
-// 4: mov QWORD PTR [rbp-0x8],rdi
-// 8: mov QWORD PTR [rbp-0x10],rsi
-int f(char *a, char *b)
-{
-_start:
- // c: mov rax,QWORD PTR [rbp-0x8]
- // 10: movzx eax,BYTE PTR [rax]
- // 13: movsx dx,al
- // 17: mov rax,QWORD PTR [rbp-0x10]
- // 1b: mov WORD PTR [rax],dx
- *b = *a;
-
- // 1e: mov rax,QWORD PTR [rbp-0x10]
- // 22: movzx eax,WORD PTR [rax]
- // 25: test ax,ax
- // 28: jne 2c
- // 2a: jmp 38
- if (*a & 0xffff != 0) {
- // 2c: add QWORD PTR [rbp-0x8],0x1
- // 31: add QWORD PTR [rbp-0x10],0x2
- // 36: jmp c
- a++;
- b++;
- goto _start;
- }
-
- // 38: pop rbp
- // 39: ret
-}
-#+END_SRC
-
-#+BEGIN_SRC c
-int f(char *a, char *b)
-{
- while (*a != '\0') {
- *b++ = *a++;
- }
-}
-#+END_SRC
-
-Cool. Yurichev wasn't lying, this is a damn simple exercise, but it is something
-that's used in nearly every C program. It's =strcpy=!
-
-* Challenge #7
-
-This exercise gives the same hint as last time, and similarly uses address
-offsets instead of symbols.
-
-Control flow isn't as initially obvious as some of the past exercises, but the
-first instruction is a pretty good tell that this function takes a =char *= as a
-parameter, and the =test dl,dl= was a good tell that the control flow depends on
-the individual characters in that parameter. The =0x41= in that ==lea
-esi,[rdx-0x41]= instruction stood out to me, as =0x41= is 'A' in ASCII, and the
-=0x20= in the =add edx,0x20= was also a big clue, as ='a' - 'A'= is =0x20=.
-
-#+BEGIN_SRC c
-void f(char *a)
-{
- char *cur;
-
- // 0: movzx edx,BYTE PTR [rdi]
- // 3: mov rax,rdi
- // 6: mov rcx,rdi
- // 9: test dl,dl
- // b: je 29
- // 29: repz ret
- if (*a == '\0')
- return;
-
- // 6: mov rcx,rdi
- cur = a;
-
- // 25: test dl,dl
- // 27: jne 10
- while (*cur != '\0') {
- // 10: lea esi,[rdx-0x41]
- // 13: cmp sil,0x19
- // 17: ja 1e
- // 19: add edx,0x20
- // 1c: mov BYTE PTR [rcx],dl
- if (*cur - 0x41 <= 0x19)
- *cur += 0x20;
-
- // 1e: add rcx,0x1
- // 22: movzx edx,BYTE PTR [rcx]
- cur++;
- }
-
- // 29: repz ret
-}
-#+END_SRC
-
-Just from the tells outlined in the previous paragraph, I don't even need to run
-=f= to know that it converts =a= to lowercase, albeit only capable of transforming
-capital ASCII characters (producing garbage for, say, a space character).
-
-* Challenge #8
-
-The hint we're given this time is, "[t]his is one of the busiest algorithms
-under the hood, though, usually hidden from programmers. It implements one of
-the most popular algorithms in computer science. It features recursion and a
-callback function."
-
-In preparation for an exercise that's would likely be more difficult than the
-past few, I did a couple quick perusals to get a basic idea of the control flow,
-the parameters, and the return values. The =mov rbp,rdx= early on indicates that
-there are at least three parameters.
-
-There's a =push rbp= instruction, but [[https://en.wikipedia.org/wiki/Function_prologue][explicit creation of a stack frame]]. There
-are also =push r12= and =push rbx= instructions. These all occur at the beginning of
-the function, so we see some register preservation and an indication that these
-are the registers that are going to be used in the code.
-
-I find that a lot of reverse engineering involves getting good footing, so
-this is the information you want when starting out.
-
-What I normally try to find out next is whether the parameters and return type
-are integers or pointers: =mov rsi,QWORD PTR [rbx]=, after =%rsi= was moved into
-=%rbx= is a good tell that the second parameter is a pointer, likely to an array
-of pointer as it's dereferenced as =QWORD PTR=, and the =call r12= tells me that the
-first parameter is the callback that was mentioned in the hint. The =js 40= after
-testing the callback's return value tells me that its return value is signed --
-probably an int, not a pointer -- and the pair of =mov rsi,QWORD PTR [rbx]= and
-=mov rdi,rbp= before the call indicate that it takes two parameters.
-
-#+BEGIN_SRC c
-void *f(int (*a)(void *, int), void **b, int c)
-{
- int ret;
- // 0: push r12
- // 2: test rsi,rsi
- // ...
- // 10: je 32
- if (b == 0) {
- // 32: pop rbx
- // 33: pop rbp
- // 34: xor eax,eax
- // 36: pop r12
- // 38: ret
- return NULL;
- }
-
- // r12 <- a
- // rbx <- b
- // rbp <- c
-
- while (1) {
- // (This code path is also duplicated at 49-54. The branch that
- // contains the duplicated code has been omitted, as the same
- // effect arises from this loop continuing to iterate.
- //
- // 18: mov rsi,QWORD PTR [rbx]
- // 1b: mov rdi,rbp
- // 1e: call r12
- ret = a(*b, c);
-
- // 21: test eax,eax
- // 23: je 56
- if (ret == 0) {
- // 56: mov rax,rbx
- // 59: pop rbx
- // 5a: pop rbp
- // 5b: pop r12
- // 5d: ret
- return b;
- }
-
- // 25: js 40
- else if (ret < 0) {
- // 40: mov rbx,QWORD PTR [rbx+0x10]
- b = b[4];
-
- // 44: test rbx,rbx
- // 47: je 32
- if (b == NULL) {
- // 32: pop rbx
- // 33: pop rbp
- // 34: xor eax,eax
- // 36: pop r12
- // 38: ret
- return NULL;
- }
- }
-
- else {
- // 27: mov rbx,QWORD PTR [rbx+0x18]
- b = b[6];
-
- // 2b: test rbx,rbx
- // 30: jne 18
- if (b == NULL) {
- // 32: pop rbx
- // 33: pop rbp
- // 34: xor eax,eax
- // 36: pop r12
- // 38: ret
- return NULL;
- }
- }
- }
-}
-#+END_SRC
-
-In deriving meaning from this, I have a bit of an advantage; I've just recently
-implemented this exact algorithm for my university's computer systems principle
-course. This is the search function for a binary search tree, which takes an
-arbitrary comparison function, =a=,, and returns the first node for which =a=
-returns 0. The function returns =NULL= if the item is not in the tree. =c= is some
-sort of "data" parameter for the callback function, hence why it isn't used in
-the algorithm.
-
-=b= is probably a pointer to a struct looking something like the following:
-
-#+BEGIN_SRC c
-struct tree_node {
- char data[0x10];
- struct tree_node *left;
- struct tree_node *right;
-}
-#+END_SRC
-
-as =QWORD PTR [rbx+0x10]= is followed when =a= returns something less than 0
-(represented in the struct as =left=), and =QWORD PTR [rbx+0x18]= is followed when =a=
-returns something greater than 0 - (represented in the struct as =right=).
-
-This exercise is a little unusual. The hint mentions recursion, but this
-algorithm is entirely iterative. Perhaps it was implemented recursively in C,
-and the compiler performed some sort of tail-call optimization? I honestly have
-no idea.
-
-* Challenge #9
-
-The hint we're given this time is, "[n]ow that's easy." I certainly hope it is.
-
-This is the first challenge we're given that uses libc. It's also the first
-challenge in which we see the compiler using [[https://en.wikipedia.org/wiki/Switch_statement#Compilation][binary search]] to optimize a
-conditional with more than one branch. I tend to write these out as =switch=
-statements whenever I see them, but it's perfectly reasonable for a compiler to
-optimize an =if= in the same way.
-
-#+BEGIN_SRC c
-#include
-#include
-
-int f(char a)
-{
- // sub rsp, 8
- // movzx eax, BYTE PTR [rdi]
- switch (a) {
- // cmp al, 89
- // je .L3
- case 'Y':
- // cmp al, 121
- // jne .L2
- case 'y':
- // .L3:
- // mov eax, 1
- // add rsp, 8
- // ret
- return 1;
-
- // jle .L21
- // ...
- // .L21:
- // cmp al, 78
- // je .L6
- case 'N':
- // ...
- // cmp al, 110
- // je .L6
- case 'n':
- // .L6:
- // xor eax, eax
- // add rsp, 8
- // ret
- return 0;
-
- default:
- // .L2:
- // mov edi, OFFSET FLAT:.LC0
- // call puts
- // xor edi, edi
- // call exit
- puts("error!");
- exit(0);
- }
-}
-#+END_SRC
-
-Yurichev wasn't lying, this was an easy challenge. In fact, if I were reverse
-engineering a binary and came across something like this, I probably wouldn't
-bother translating the assembly to equivalent C. It's a function that converts a
-character to a boolean (in the sense of a prompt that asks the user for 'Y' or
-'N' -- "Yes" or "No") and exits prematurely if the character wouldn't make sense
-in that context.
-
-* Challenge #10
-
-The hint time is "[t]his code snippet is short, but tricky. What does it do?
-It's used heavily in low-level programming and is well-known to many low-level
-programmers. There are several ways to calculate it, and this is the one of
-them."
-
-The snippet really is short, clocking in at only four instructions, but I still
-felt the need to break out [[https://godbolt.org/][Compiler Explorer]] for this one. The part about being
-"used heavily in low-level programming" threw me off a bit, since I saw =neg= and
-thought that perhaps that'd correspond to the =~= operator in C, which I've only
-seen used in very low-level bit shifting code. This initial assumption would've
-led me astray, however, and I'm glad I took the extra minute to verify.
-
-#+BEGIN_SRC c
-int f(int a)
-{
- return -a;
-}
-#+END_SRC
-
-#+BEGIN_SRC asm
-f(int):
- push rbp
- mov rbp, rsp
- mov DWORD PTR [rbp-4], edi
- mov eax, DWORD PTR [rbp-4]
- neg eax
- pop rbp
- ret
-#+END_SRC
-
-#+BEGIN_SRC c
-int f(int a)
-{
- return ~a;
-}
-#+END_SRC
-
-#+BEGIN_SRC asm
-f(int):
- push rbp
- mov rbp, rsp
- mov DWORD PTR [rbp-4], edi
- mov eax, DWORD PTR [rbp-4]
- not eax
- pop rbp
- ret
-#+END_SRC
-
-=not= corresponds to =~=, and =neg= corresponds to =-= We're dealing with =neg= here.
-
-The equivalent C code for the snippet is given. Because I had Compiler Explorer
-open already, I decided to throw this in there for kicks and giggles. x86-64 gcc
-8.3 with =-O2= spits out the exact same series of instructions as the challenge. I
-love the predictability of C compilers.
-
-#+BEGIN_SRC c
-int f(int a, int b)
-{
- return (a + b - 1) & -b;
-}
-#+END_SRC
-
-This doesn't answer our question, though. What does this do? We can test a few
-values of =a= and =b= with the following snippet, replacing =2<<0= with various
-constants.
-
-#+BEGIN_SRC c
-int main(void)
-{
- int i, j;
- j = 2 << 0;
- for (i = 0; i < 256; i++) {
- printf("%-8x %-8x %-8x\n", i, j, f(i, j));
- }
-}
-#+END_SRC
-
-#+BEGIN_SRC
-0 2 0
-1 2 2
-2 2 2
-3 2 4
-4 2 4
-5 2 6
-6 2 6
-7 2 8
-8 2 8
-9 2 a
-a 2 a
-b 2 c
-c 2 c
-d 2 e
-e 2 e
-f 2 10
-...
-0 8 0
-1 8 8
-2 8 8
-3 8 8
-4 8 8
-5 8 8
-6 8 8
-7 8 8
-8 8 8
-9 8 10
-a 8 10
-b 8 10
-c 8 10
-d 8 10
-e 8 10
-f 8 10
-10 8 10
-11 8 18
-12 8 18
-#+END_SRC
-
-It would seem that this is some sort of "least multiple of \(b\) such that \(b <
-a\) given that \(b\) is a power of two, but I feel as though I'm grasping at
-straws here.
-
-As a Gentoo user, I have the Linux source tree checked out at =/usr/src/linux=,
-and because the hint mentions low-level programming, I decided to create a
-regular expression for the C I came up with and let =ag= have a go at it.
-
-=ag "\\(.*-[^>].*\\).*&.*\\-" /usr/src/linux= yielded quite a few results. Before
-I ran the command, I wasn't expecting much, thinking that my regex was too
-permissive, but the first result I saw looked remarkably like the C expression I
-had come up with -- right at the beginning of =sysv_readdir= in =fs/sysv/dir.c=:
-
-#+BEGIN_SRC c
-static int sysv_readdir(struct file *file, struct dir_context *ctx)
-{
- unsigned long pos = ctx->pos;
- struct inode *inode = file_inode(file);
- struct super_block *sb = inode->i_sb;
- unsigned long npages = dir_pages(inode);
- unsigned offset;
- unsigned long n;
-
- ctx->pos = pos = (pos + SYSV_DIRSIZE-1) & ~(SYSV_DIRSIZE-1);
- if (pos >= inode->i_size)
- return 0;
-#+END_SRC
-
-Hm. Remember how I mentioned that I expected =neg= to correspond to a =~=? Well,
-jumping back to Compiler Explorer:
-
-#+BEGIN_SRC c
-int f(int a)
-{
- return ~a;
-}
-#+END_SRC
-
-#+BEGIN_SRC asm
-f(int):
- mov eax, edi
- not eax
- ret
-#+END_SRC
-
-#+BEGIN_SRC c
-int f(int a)
-{
- return ~(a - 1);
-}
-#+END_SRC
-
-#+BEGIN_SRC asm
-f(int):
- mov eax, edi
- neg eax
- ret
-#+END_SRC
-
-Modifying our search slightly to =ag "\\(.*-[^>].*\\).*&.*\\~.*\\-.*1"= yields a
-massive number of results, some of which are named macros. Here's one of them,
-in =include/uapi/linux/if_packet.h=:
-
-#+BEGIN_SRC c
-#define TPACKET_ALIGN(x) (((x)+TPACKET_ALIGNMENT-1)&~(TPACKET_ALIGNMENT-1))
-#+END_SRC
-
-Cool. That makes me feel much more confident in my answer.
-
-* Challenge #11
-
-The hint for this exercise is: "[t]his is a somewhat large function (in contrast
-to the other exercises in this blog), but heavily used nowadays in various
-software. As it can be clearly seen, it uses standard C/C++ functions including
-strlen() and sscanf(). Some other helper function is also used. I intentionally
-gave it this name to conceal its real function. So what does the whole code
-snippet do?"
-
-I'd like to apologize in advance for the sloppiness of the code that follows.
-Also, I've renamed =helper= to =is_hex_digit=, as it makes the code for =f= clearer.
-
-#+BEGIN_SRC c
-#include
-#include
-
-int is_hex_digit(char a)
-{
- // lea edx, [rdi-48]
- // mov eax, 1
- // cmp edx, 9
- // jbe .L2
- if (a <= '9') {
- // .L2:
- // ret
- return 1;
- }
-
- // and edi, -33
- // xor eax, eax
- // sub edi, 65
- // cmp edi, 5
- // setbe al
- // .L2:
- // ret
- return (a & -33) <= 'F' ? 1 : 0;
-}
-
-int f(char *a, char *b)
-{
- int len;
- int local_12;
- char *cur;
- char *end;
- char *dst;
- char *next;
-
- // push r15
- // xor eax, eax
- // or rcx, -1
- // push r14
- // push r13
- // push r12
- // mov r12, rsi
- // push rbp
- // mov rbp, rsi
- // push rbx
- // mov rbx, rdi
- // sub rsp, 24
- // repnz scasb
- // not rcx
- dst = b;
- cur = a;
- len = strlen(a);
-
- // lea r14, [rbx-1+rcx]
- // .L6:
- // cmp rbx, r14
- // ja .L24
- while (cur <= end) {
- // movsx eax, BYTE PTR [rbx]
- // ...
- // mov DWORD PTR [rsp+12], eax
- local_12 = (int) *cur;
-
- // lea r13, [rbx+1]
- next = cur + 1;
-
- // mov r15, r13
- // cmp eax, 43
- // jne .L7
- if (*cur == '+') {
- // mov DWORD PTR [rsp+12], 32
- local_12 = ' ';
- // jmp .L8
- } else {
- // .L7:
- // cmp eax, 37
- // jne .L8
- // movsx edi, BYTE PTR [rbx+1]
- // call helper
- // test eax, eax
- // jne .L9
- if (*cur == '%' && is_hex_digit(*(cur + 1))) {
- // .L9:
- // movsx edi, BYTE PTR [rbx+2]
- // lea r13, [rbx+3]
- next = cur + 3;
-
- // call helper
- // test eax, eax
- // je .L11
- if (!is_hex_digit(*(cur + 2))) {
- // .L11:
- // or eax, -1
- // jmp .L10
- // .L10:
- // add rsp, 24
- // pop rbx
- // pop rbp
- // pop r12
- // pop r13
- // pop r14
- // pop r15
- // ret
- return -1;
- }
-
- // lea rdx, [rsp+12]
- // xor eax, eax
- // mov esi, OFFSET FLAT:.LC0
- // mov rdi, r15
- // call __isoc99_sscanf
- // test eax, eax
- // je .L11
- if (!sscanf(cur + 1, "%2X", &local_12)) {
- // .L11:
- // or eax, -1
- // jmp .L10
- // .L10:
- // add rsp, 24
- // pop rbx
- // pop rbp
- // pop r12
- // pop r13
- // pop r14
- // pop r15
- // ret
- return -1;
- }
- }
-
- }
-
- // .L8:
- // test r12, r12
- // je .L12
- if (b != NULL) {
- // mov eax, DWORD PTR [rsp+12]
- // mov BYTE PTR [rbp+0], al
- *dst = local_12;
- }
-
- // .L12:
- // inc rbp
- // mov rbx, r13
- // jmp .L6
- dst++;
- cur = next;
- }
-
- // .L24:
- // mov eax, ebp
- // sub eax, r12d
- // .L10:
- // add rsp, 24
- // pop rbx
- // pop rbp
- // pop r12
- // pop r13
- // pop r14
- // pop r15
- // ret
- return dst - b;
-}
-#+END_SRC
-
-This could very well be cleaned up. In fact, I'm not even sure that my
-translation is completely correct, but I got to the point where I felt it was
-"good enough" and I could explain that =f= is a function for decoding a
-[[https://en.wikipedia.org/wiki/Percent-encoding][percent-encoded]] string, where =a= is the encoded string and =b= is a destination to
-decode to. If not for the telltale ='+'= corresponding to a =' '= and use of a ='%'=
-character, I probably would have spent more time cleaning up my translation and
-making sense of it. But I've seen code like this many times in my life, it
-really is "heavily used nowadays in various software."
-
-I began this challenge by reversing =helper=, which I think was a good move as it
-gave me some footing. I didn't even notice '%' or '+' in =f= at first, but the
-realization that =helper= worked with hexadecimal digits got me started on ideas
-for what =f= might do.
-
-On the topic of =helper=, the reason I was able to pick out that it's checking for
-hexadecimal digits was realizing that \(a - 48 \leq 9\) is equivalent to \(a
-\leq 49 + 9\). The comparison is otherwise pretty unclear. And I suspect that
-the =-33= is related to how ASCII is encoded.
-
-The control flow for =f= is pretty intimidating with its 8 labels. When it came
-time to look at =f=, I drew out a rudimentary control flow graph on paper --
-scribbling down the label names and drawing arrows between the different labels.
-I found this to be very useful in identifying which jumps are loops (cycles in
-the graph), which are conditionals (branches), and which labels are related
-(linear relationships).
-
-#+BEGIN_EXPORT html
-
-#+END_EXPORT
diff --git a/org/Writeups for Dennis Yurichev's Reverse Engineering Challenges (#23-#35)/challenges-re-writeups-3.org b/org/Writeups for Dennis Yurichev's Reverse Engineering Challenges (#23-#35)/challenges-re-writeups-3.org
deleted file mode 100644
index 44b3021..0000000
--- a/org/Writeups for Dennis Yurichev's Reverse Engineering Challenges (#23-#35)/challenges-re-writeups-3.org
+++ /dev/null
@@ -1,817 +0,0 @@
-#+TITLE: Writeups for Dennis Yurichev's Reverse Engineering Challenges (#23-#35)
-#+DATE: <2019-08-18 Sun 10:42>
-#+TAGS: writeup, reverse-engineering, x86
-
-This is the third set of solutions for my self-imposed challenge of completing
-at least fifty of the exercises on Dennis Yurichev's [[https://challenges.re][challenges.re]] by the end of
-the year. The previous set is available [[http:///jakob.space/challenges-re-writeups-2.html][here]].
-
-* Challenge #23
-
-The problem is prefaced with, "[t]his is another implementation of a well-known
-library function, works only in a 64-bit environment." Translating the
-disassembly directly to C reveals unrolled loops, but the intent isn't too
-difficult to figure out.
-
-#+BEGIN_SRC c
-int f(char *a)
-{
- int i;
-
- if (a[0] == '\0') {
- return 0;
- }
-
- if (a[1] == (char) 0xff) {
- return 1;
- }
-
- if (a[2] == (char) 0xff) {
- return 2;
- }
-
- if (a[3] == (char) 0xff) {
- return 3;
- }
-
- if (a[4] == (char) 0xff) {
- return 4;
- }
-
- if (a[5] == (char) 0xff) {
- return 5;
- }
-
- i = 0;
-
- while (a[6] != (char) 0xff) {
- if (a[7] == (char) 0xff) {
- return i + 7;
- }
-
- i += 8;
- a += 8;
-
- if (a[1] == (char) 0xff) {
- return i;
- }
-
- if (a[1] == (char) 0xff) {
- return i + 1;
- }
-
- if (a[2] == (char) 0xff) {
- return i + 2;
- }
-
- if (a[3] == (char) 0xff) {
- return i + 3;
- }
-
- if (a[4] == (char) 0xff) {
- return i + 4;
- }
-
- if (a[5] == (char) 0xff) {
- return i + 5;
- }
- }
-
- return i + 6;
-}
-#+END_SRC
-
-=f= returns the index of the first occurrence of =0xff= in =a=. In addition to asking
-for the purpose of the code, the challenge poses a few additional questions.
-
-First: "The code may crash under some specific circumstances. Which are...?" =f=
-will crash in the case that there isn't a 0xff character in the string.
-
-Second: "The code can be easily optimized using SSEx. How?" =movq= can be used to
-dereference the characters of =a=, and the location of the =0xff= character can be
-found using =pcmpeqb=. Actually implementing this is left as an exercise to the
-reader. And I'm not saying that just because writing SIMD by hand makes me want
-to break down and cry... or anything like that...
-
-Finally: "The code will not work correctly on big-endian architectures. How to
-fix it?" In the disassembly, the LSB of =rdx= (=dl=) is treated as the _first_
-character in the sliding window. On a big-endian system, dereferencing the
-window as an integer would mean that the LSB would correspond with the _last_
-character in the window. To fix this, you would need to change which parts of
-the register are being looked at. I realize that's a rather anemic answer, but
-the alternative would be going all-in and implementing =f= on a big-endian
-platform, which I don't really want to do right now.
-
-* Challenge #26
-
-I decided to skip challenges #24 and #25 as they were listed as "Level 2" and
-"Level 3" respectively in terms of difficulty. Challenge #25 in particular
-seemed particularly demanding. Challenge #26, on the other hand, was a
-relatively straightforward bytecode reverse engineering task. Like Challenge
-#14, disassemblies for both .NET and the JVM are given, and as I'm more familiar
-with Java than C# (unfortunately), that's the disassembly I chose to work with.
-
-#+BEGIN_SRC java
-public static byte f(byte a) {
- return (byte) ((((long) a * 8623620610L) & 1136090292240L) % 1023L);
-}
-#+END_SRC
-
-Again, I'm not familiar with JVM bytecode, so I broke out [[https://en.wikipedia.org/wiki/Java_bytecode_instruction_listings][my favorite JVM
-reference]]. Here are the instructions we're concerned with:
-
-#+BEGIN_SRC java
-iload_0 // load an int value from local 0
-i2l // convert an int to a long
-l2i // convert a long to an int
-i2b // convert an int to a byte
-ldc2_w // push a constant onto the stack
-lmul // multiply two longs
-land // perform a bitwise and on two longs
-lrem // perform remainder division on two longs
-#+END_SRC
-
-Even if you don't know how the JVM works, I think the purpose of =f= is fairly
-clear as soon as you know what those few instructions do.
-
-I've typically been using Matt Godbolt's amazing [[https://godbolt.org/][Compiler Explorer]] to check my
-solutions, but this time around I used [[http://javabytes.io/][Javabytes]]. The disassembly of my
-translation for =f= matches what was given for the challenge, so I'm quite
-confident in my answer. As for what it does: I began my analysis as I typically
-do, giving the function some test values and observing the output.
-
-#+BEGIN_SRC java
-public static void main(String[] args) {
- for (int i = 0; i < 256; i++) {
- System.out.printf("%3i: b\n", i, f((byte) i));
- }
-}
-
-// 0: 0
-// 1: -128
-// 2: 64
-// 3: -64
-// 4: 32
-// ...
-// 253: 63
-// 254: -65
-// 255: 127
-#+END_SRC
-
-That isn't very telling, but the oscillating sign gives me an idea.
-
-#+BEGIN_SRC java
-public static String toPaddedBinary(byte a) {
- String s = String.format("%8s", Integer.toBinaryString(a));
- s = s.replace(' ', '0');
- return s.substring(s.length() - 8, s.length());
-}
-
-public static void main(String[] args) {
- for (int i = 0; i < 256; i++) {
- System.out.printf("%s: %s\n", toPaddedBinary((byte) i), toPaddedBinary(f((byte) i)));
- }
-}
-
-// 00000000: 00000000
-// 00000001: 10000000
-// 00000010: 01000000
-// ...
-// 11111101: 10111111
-// 11111110: 01111111
-// 11111111: 11111111
-#+END_SRC
-
-So =f= reverses the bits of =a=.
-
-* Challenge #27
-
-This challenge threw me for a bit of a loop, as it didn't give the usual amd64
-output from GCC 4.9. Rather an i386 disassembly from MSVC 2010 was given,
-alongside an arm64 disassembly from GCC 4.9. I tried both, but had some
-significant trouble with the MSVC disassembly as it seemed to be dealing with
-64-bit integers on a 32-bit architecture.
-
-After quickly reviewing CDOT's [[https://wiki.cdot.senecacollege.ca/wiki/Aarch64_Register_and_Instruction_Quick_Start#General-Purpose_Registers][AArch64 reference]] to get an idea of register
-widths, this is the translation came up with:
-
-#+BEGIN_SRC c
-int f(int a)
-{
- return (((int) (((long) a * 0xc64b2279) >> 32)) + a) >> 9 - (a >> 31);
-}
-#+END_SRC
-
-I'm not particularly confident in this, however, as the behavior of =f= is to
-return \(floor(a / 289)\). I suspect my poor understanding of the [[http://infocenter.arm.com/help/topic/com.arm.doc.dui0068b/CIHBEAGE.html][flexible
-second operand]] (i.e. in =sub w0, w1, w0, asr 31=) is what gave me me the most
-trouble. Perhaps this is a challenge I should return to when I properly learn
-ARM.
-
-I tried a more direct translation to Python,
-
-#+BEGIN_SRC python
-def test_f(a):
- result = a * 0xc64b2279
- upper = result & 0xffffffff00000000
- lower = result & 0xffffffff
- return ((upper + lower) >> 9) + \
- (((upper + lower) >> 9) >> 31)
-
-fmt = lambda n: bin(n)[2:].rjust(32, '0')
-
-for i in range(256):
- print("{}\n{}\n".format(fmt(i), fmt(test_f(i))))
-#+END_SRC
-
-which didn't yield any recognizable patterns.
-
-Actually, before implementing it in Python, I implemented it in Emacs Lisp (I
-might have been waiting on Python to compile? I don't remember).
-
-#+BEGIN_SRC elisp
-(defun test-f (a)
- (let* ((result (* a #xc64b2279))
- (upper (logand result #xffffffff00000000))
- (lower (logand result #xffffffff)))
- (+ (ash (+ upper lower) 9)
- (ash (ash (+ upper lower) 9) 31))))
-#+END_SRC
-
-Either way, this challenge wasn't fruitful.
-
-* Challenge #28
-
-I suspect that this challenge was made a bit easier by GCC's optimizations. The
-amd64 disassembly includes two unused functions, =f2= and =my_memdup= -- they're
-used in some of the other disassemblies, but I chose to ignore them.
-
-#+BEGIN_SRC c
-#include
-#include
-
-int f1(int *a, int *b)
-{
- return *a > *b ? 0 : -1;
-}
-
-int f_main(void *src, int n)
-{
- int tmp;
- char *dst;
-
- dst = malloc(n * sizeof(int));
- memcpy(dst, src, n * sizeof(int));
- qsort(dst, n, sizeof(int), f1);
-
- if (n > 1) {
- tmp = dst[n >> 1] + \
- dst[n >> 1 - 1];
- return (tmp + (tmp >> 31)) >> 1;
- }
-
- return dst[0];
-}
-#+END_SRC
-
-I've started to see this =(tmp + (tmp >> 31)) >> 1= idiom rather frequently, so I
-decided to finally look it up, coming across [[https://stackoverflow.com/questions/40638335/why-does-the-compiler-generate-a-right-shift-by-31-bits-when-dividing-by-2][this]] Stack Overflow answer. I'm
-glad I did, because realizing that it carries out signed integer division by two
-makes this exercise far more clear.
-
-#+BEGIN_SRC c
-#include
-#include
-
-int f1(int *a, int *b)
-{
- return *a > *b ? 0 : -1;
-}
-
-int f_main(void *src, int n)
-{
- char *dst;
-
- dst = malloc(n * sizeof(int));
- memcpy(dst, src, n * sizeof(int));
- qsort(dst, n, sizeof(int), f1);
-
- if (n > 1) {
- return (dst[n / 2] + dst[n / 2 - 1]) / 2;
- }
-
- return dst[0];
-}
-#+END_SRC
-
-=f_main= returns the [[https://en.wikipedia.org/wiki/Median][median]] of a set of values.
-
-* Challenge #30
-
-I have, once again, skipped another challenge that was being listed as "level
-2," which brings us to the thirtieth challenge. This one is strikingly different
-from the other challenges I've covered here; rather than being asked to describe
-what a program does, the instruction read:
-
-"This program requires a password. Try to find it.
-
-As an additional exercise, try to change the password by patching the executable
-file. Also try using one with a different length. What is the shortest possible
-password here?
-
-Also try to crash the program using only string input."
-
-We're given several links to downloads. Binaries are provided for 32-bit
-Microsoft Windows, Mac OS X, and i386/mips Linux. I went with i386 Linux, as I'd
-be able to run the challenge natively.q
-
-#+BEGIN_SRC
-jakob@Epsilon /tmp $ sha256sum password1
-96b8110208d61c7ac586910ebad22ef2e4bbeb867e6d6429967846698b9d02fc password1
-#+END_SRC
-
-Being faced with a binary, I was tempted to use this as an opportunity to try
-out [[https://ghidra-sre.org/][Ghidra]], but while I waited for OpenJDK 11 to download, I peered inside with
-radare2 and decided that it wasn't worth the trouble. Here's the disassembly,
-according to radare:
-
-#+BEGIN_SRC
-[0x080484ed]> pdf
- ;-- eip:
-┌ (fcn) main 149
-│ main ();
-│ ; var int local_4h @ esp+0x4
-│ ; var int local_1ch @ esp+0x1c
-│ ; var int local_9ch @ esp+0x9c
-│ ; DATA XREF from 0x08048407 (entry0)
-│ 0x080484ed 55 pushl %ebp
-│ 0x080484ee 89e5 movl %esp, %ebp
-│ 0x080484f0 83e4f0 andl $0xfffffff0, %esp
-│ 0x080484f3 81eca0000000 subl $0xa0, %esp
-│ 0x080484f9 65a114000000 movl %gs:0x14, %eax ; [0x14:4]=-1 ; 20
-│ 0x080484ff 8984249c0000. movl %eax, local_9ch
-│ 0x08048506 31c0 xorl %eax, %eax
-│ 0x08048508 c70424208604. movl $str.enter_password:, 0(%esp) ; [0x8048620:4]=0x65746e65 ; "enter password:"
-│ 0x0804850f e89cfeffff calll sym.imp.puts ; int puts(const char *s)
-│ 0x08048514 8d44241c leal local_1ch, %eax ; 0x1c ; 28
-│ 0x08048518 89442404 movl %eax, local_4h
-│ 0x0804851c c70424308604. movl $0x8048630, 0(%esp) ; [0x8048630:4]=0x6e007325
-│ 0x08048523 e8b8feffff calll sym.imp.__isoc99_scanf
-│ 0x08048528 83f801 cmpl $1, %eax ; 1
-│ ┌─< 0x0804852b 740c je 0x8048539
-│ │ 0x0804852d c70424338604. movl $str.no_password_supplied, 0(%esp) ; [0x8048633:4]=0x70206f6e ; "no password supplied"
-│ │ 0x08048534 e877feffff calll sym.imp.puts ; int puts(const char *s)
-│ │ ; JMP XREF from 0x0804852b (main)
-│ └─> 0x08048539 c74424044886. movl $str.metallica, local_4h ; [0x8048648:4]=0x6174656d ; "metallica"
-│ 0x08048541 8d44241c leal local_1ch, %eax ; 0x1c ; 28
-│ 0x08048545 890424 movl %eax, 0(%esp)
-│ 0x08048548 e843feffff calll sym.imp.strcmp ; int strcmp(const char *s1, const char *s2)
-│ 0x0804854d 85c0 testl %eax, %eax
-│ ┌─< 0x0804854f 750e jne 0x804855f
-│ │ 0x08048551 c70424528604. movl $str.password_is_correct, 0(%esp) ; [0x8048652:4]=0x73736170 ; "password is correct"
-│ │ 0x08048558 e853feffff calll sym.imp.puts ; int puts(const char *s)
-│ ┌──< 0x0804855d eb0c jmp 0x804856b
-│ ││ ; JMP XREF from 0x0804854f (main)
-│ │└─> 0x0804855f c70424668604. movl $str.password_is_not_correct, 0(%esp) ; [0x8048666:4]=0x73736170 ; "password is not correct"
-│ │ 0x08048566 e845feffff calll sym.imp.puts ; int puts(const char *s)
-│ │ ; JMP XREF from 0x0804855d (main)
-│ └──> 0x0804856b 8b94249c0000. movl local_9ch, %edx ; [0x9c:4]=-1 ; 156
-│ 0x08048572 653315140000. xorl %gs:0x14, %edx
-│ ┌─< 0x08048579 7405 je 0x8048580
-│ │ 0x0804857b e820feffff calll sym.imp.__stack_chk_fail ; void __stack_chk_fail(void)
-│ │ ; JMP XREF from 0x08048579 (main)
-│ └─> 0x08048580 c9 leave
-└ 0x08048581 c3 retl
-#+END_SRC
-
-As you can see, this is just like any other "easy crackme." A simple string
-comparison. radare2 doesn't automatically decode 0x8048630 as a string, but it's
-trivial to obtain its value.
-
-#+BEGIN_SRC
-:> psz @ 0x8048630
-%s
-#+END_SRC
-
-Translating it into C is similarly trivial.
-
-#+BEGIN_SRC c
-#include
-#include
-
-int main(void)
-{
- char buf[128];
- puts("enter password:");
- if (scanf("%s", buf) != 1) {
- puts("no password supplied");
- }
- if (strcmp(buf, "metallica") == 0) {
- puts("password is correct");
- } else {
- puts("password is not correct");
- }
-}
-#+END_SRC
-
-I do have to complement Yurichev's choice of strong passwords. \m/
-
-One may wonder where I pulled =128= from. Our stack layout looks something like
-this:
-
-#+BEGIN_SRC prog
-+-------------------------------------+
-|%esp |
-|Scratch space for function arguments.|
-+-------------------------------------+
-|%esp + 0x1c |
-|Buffer starts here |
-|... |
-|Buffer ends here |
-+-------------------------------------+
-|%esp + 0x9c |
-|Stack canary, perhaps? |
-+-------------------------------------+
-|%esp + I DON'T CARE ANYMORE |
-|Here be dragons. |
-+-------------------------------------+
-#+END_SRC
-
-radare2 is kind enough to automatically name local variables according to their
-position in the stack layout, so I was able to derive this from the names
-=local_1ch= and =local_9ch=. =local_4h= isn't really a local variable -- it looks like
-one, but that's just how the compiler decided to set up arguments for the
-various function calls (dereferencing the stack pointer, as opposed to using
-=push=). Anyway, subtracting =0x9c= from =0x1c= gets you 128 -- hence, the buffer size
-in my translation.
-
-It's pretty easy to patch the password, since =strcmp= operates on C strings. Just
-patch the characters. No sort of length needs to be adjusted since they're
-null-terminated. The shortest possible password would be zero characters long,
-which would be achieved by patching in a null byte at the 'm' in "metallica".
-This can be done however you like, though radare makes it easy if you've opened
-the file in "write mode": just seek to the location of the 'm' and =wx 00=.
-Crashing the program is similarly easy, since there are no bounds checks on the
-call to =scanf=.
-
-#+BEGIN_SRC
-jakob@Epsilon /tmp $ python -c "print('a' * 256)" | ./test
-enter password:
-password is not correct
-Segmentation fault
-#+END_SRC
-
-* Challenge #31
-
-Yowch. We're only given disassemblies from MSVC this time.
-
-#+BEGIN_SRC c
-double f(double a, int b)
-{
- double cur;
- cur = 1.0;
- while (((double) (((int) (cur - a)) - b)) <= 0.001)
- cur = (a + 1.0) * 0.5;
- return cur;
-}
-#+END_SRC
-
-Once again, I deferred to [[https://float.exposed/][float.exposed]] to decode the floating-point constant
-values. =__real@3ff0000000000000= is =1.0=, =__real@3f50624dd2f1a9fc= is approximately
-=0.001=, and =__real@3fe0000000000000= is =0.5=. I also needed to look up most of the
-SIMD instructions. =cvttsd2si= converts a double to an int, =cdq= converts an int
-into a long, =cvtdq2pd= converts an int to a double, and =comisd= is comparable to
-=cmp=.
-
-This converges for very few values. Which is a pain, since this translation
-gives me some very promising output in [[https://godbolt.org/][Compiler Explorer]]. But considering the
-value that the loop gets stuck on, I suspect that =f= averages =a= and =b=.
-
-* Challenge #32
-
-We're given a hint that, "[t]his is a standard C library function. The source
-code is taken from MSVC 2010."
-
-#+BEGIN_SRC c
-#include
-
-char *f(char *a, char *b)
-{
- char *cur;
- char *a_cur;
- char *b_cur;
-
- cur = a;
-
- if (*b == '\0') {
- return a;
- }
-
- while (*cur != '\0') {
- a_cur = cur;
- b_cur = b;
-
- while (*a_cur != '\0' && *b_cur != '\0' && *a_cur == *b_cur) {
- a_cur++;
- b_cur++;
- }
-
- if (*b_cur == '\0') {
- return cur;
- }
-
- cur++;
- }
-
- return NULL;
-}
-#+END_SRC
-
-I think the translation makes the purpose of this function reasonably clear, but
-the hint means I can verify my work against C's tiny standard library. =f= is
-obviously one of the library's [[https://en.wikipedia.org/wiki/C_string_handling][string functions]]. Can you guess which one?
-
-(My answer is that =f= is an implementation of =strstr=.)
-
-* Challenge #33
-
-What gave it away for me this time was the "crypto" tag. I stopped in my
-translation efforts about here,
-
-#+BEGIN_SRC c
-void f(void *a, void *b, void *c)
-{
- int mushroom; // _k0
- int bean; // _k1
- int tomato; // _k2
- int corn; // _k3
-
- // eax = a[0]
- // ecx = a[1]
-
- mushroom = b[0];
- bean = b[1];
-
- // esi = b[3];
- // edx = 0;
-
- tomato = b[2];
- corn = b[3];
-
- // edi = 32;
-
- // LL8
- esi = ecx >> 5 + bean;
- ebx = ecx << 4 + mushroom;
- edx -= 0x61c88647;
-
- esi ^= ebx;
- ebx = ecx + edx;
- esi ^= ebx;
-
- eax += esi;
-
- esi = eax >> 5 + corn;
- ebx = eax << 4 + tomato;
-
- esi ^= ebx;
- ebx = eax + edx;
- esi ^= ebx;
-
- ecx += esi;
- edi--;
-
- // When edi == 0: c[0] = eax, c[1] = ecx
-}
-#+END_SRC
-
-and decided to do a search for '0x61c88647 hash'. This yields a few interesting
-results, such as [[https://stackoverflow.com/questions/38994306/what-is-the-meaning-of-0x61c88647-constant-in-threadlocal-java][one]] describing the constant used in ThreadLocal.java's
-implementation Fibonacci hashing and [[https://softwareengineering.stackexchange.com/questions/63595/tea-algorithm-constant-0x9e3779b9-said-to-be-derived-from-golden-ratio-but-the][another]] describing the constants used in
-the Tiny Encryption Algorithm.
-
-This immediately set off bells for me. I read Bruce Schneier's /Applied
-Cryptography/ some years back and was instantly reminded that TEA uses [[https://en.wikipedia.org/wiki/Block_cipher#Operations][ARX]] with
-shifts of =5= and =4=. If you pull up Wikipedia's reference code for TEA encryption,
-you'll be greeted with the following:
-
-#+BEGIN_SRC c
-void encrypt (uint32_t v[2], uint32_t k[4]) {
- uint32_t v0=v[0], v1=v[1], sum=0, i; /* set up */
- uint32_t delta=0x9E3779B9; /* a key schedule constant */
- uint32_t k0=k[0], k1=k[1], k2=k[2], k3=k[3]; /* cache key */
- for (i=0; i<32; i++) { /* basic cycle start */
- sum += delta;
- v0 += ((v1<<4) + k0) ^ (v1 + sum) ^ ((v1>>5) + k1);
- v1 += ((v0<<4) + k2) ^ (v0 + sum) ^ ((v0>>5) + k3);
- } /* end cycle */
- v[0]=v0; v[1]=v1;
-}
-#+END_SRC
-
-Armed with this, I can confidently say that =f= is an implementation of TEA
-encryption with a schedule constant of =0x61c88647=.
-
-* Challenge #34
-
-Another crypto challenge. This time, we're told that "[t]his is a well-known
-cryptographic algorithm from the past." The disassembly was simple enough that I
-thought to translate it into standard mathematical notation rather than C, but
-it turned out to be far less helpful than the equivalent C.
-
-#+BEGIN_SRC c
-uint16_t f(uint16_t a)
-{
- uint16_t tmp;
-
- tmp = a << 2;
- tmp ^= a;
- tmp <<= 1;
- tmp ^= a;
- tmp <<= 2;
- tmp ^= a;
-
- return ((tmp & 32) << 10) | (a >> 1);
-}
-#+END_SRC
-
-That said, I'm not familiar with the particular algorithm. There's a clear
-pattern, but I'm not sure where to start looking. Is it a hash function? Some
-kind of bastardized XOR encryption? Who knows.
-
-* Challenge #35
-
-This was a tough one. I'll give my initial translation to C and explain where I
-went wrong:
-
-#+BEGIN_SRC c
-#include
-#include
-
-int f(int x, int y)
-{
- int a, b;
-
- if (x == 0) {
- return y;
- }
-
- if (y == 0) {
- return x;
- }
-
- a = x >> ffs(x);
- b = y >> ffs(y);
-
- while (a != b) {
- if (a < b) {
- SWAP(a, b);
- }
-
- if (a == 1) {
- break;
- }
-
- b = (b - a) >> ffs(b - a);
- }
-
- return a << ffs(x | y);
-}
-#+END_SRC
-
-One thing worth remarking on in the disassembly is this:
-
-#+BEGIN_SRC asm
- xor esi, edx
- xor edx, esi
- xor esi, edx
-#+END_SRC
-
-This is the [[https://en.wikipedia.org/wiki/XOR_swap_algorithm][XOR swap algorithm]]. In an attempt to make the translation more
-clear, I replaced it with a (non-existent) =SWAP= macro. =ffs= is also a POSIX
-extension that [[https://stackoverflow.com/questions/757059/position-of-least-significant-bit-that-is-set][corresponds nicely]] to the =bsf= instruction.
-
-The issue? I've been reading these MSVC disassemblies wrong the whole time. Take
-this instruction, for example: =mov edx, DWORD PTR _y$[esp+4]=. I'd never actually
-done out the calculations. As it turns out, =_rt$2[esp+8]= aliases with =y=. I
-thought that =_rt$2= was a distinct variable and that the compiler was storing to
-some local variable but never using it. This isn't the case, hence why the
-translation doesn't work as intended.
-
-What I need to start doing for these MSVC disassemblies is translating them into
-something I can assemble.
-
-#+BEGIN_SRC asm
-global f
-f:
- push ecx
- push esi
- mov esi, DWORD [esp+12]
- test esi, esi
- jne init
- mov eax, DWORD [esp+16]
- pop esi
- pop ecx
- ret
-init:
- mov edx, DWORD [esp+16]
- mov eax, esi
- test edx, edx
- je exit
- or eax, edx
- push edi
- bsf edi, eax
- bsf eax, esi
- mov ecx, eax
- mov DWORD [esp+8], eax
- bsf eax, edx
- shr esi, cl
- mov ecx, eax
- shr edx, cl
- mov DWORD [esp+16], eax
- cmp esi, edx
- je return
-lp:
- jbe skip
- xor esi, edx
- xor edx, esi
- xor esi, edx
-skip:
- cmp esi, 1
- je return
- sub edx, esi
- bsf eax, edx
- mov ecx, eax
- shr edx, cl
- mov DWORD [esp+16], eax
- cmp esi, edx
- jne lp
-return:
- mov ecx, edi
- shl esi, cl
- pop edi
- mov eax, esi
-exit:
- pop esi
- pop ecx
- ret 0
-#+END_SRC
-
-Actually, I should be doing this for all of the challenges... Anyway, observing
-a few test values for =f=:
-
-#+BEGIN_SRC prog
-f(1, 1) = 1
-f(1, 2) = 1
-f(1, 3) = 1
-f(1, 4) = 1
-f(1, 5) = 1
-f(1, 6) = 1
-f(1, 7) = 1
-f(1, 8) = 1
-f(1, 9) = 1
-...
-f(1, 252) = 1
-f(1, 253) = 1
-f(1, 254) = 1
-f(1, 255) = 1
-f(2, 1) = 1
-f(2, 2) = 2
-f(2, 3) = 1
-f(2, 4) = 2
-f(2, 5) = 1
-f(2, 6) = 2
-f(2, 7) = 1
-f(2, 8) = 2
-f(2, 9) = 1
-f(2, 10) = 2
-f(2, 11) = 1
-f(2, 12) = 2
-...
-f(9, 1) = 1
-f(9, 2) = 1
-f(9, 3) = 3
-f(9, 4) = 1
-f(9, 5) = 1
-f(9, 6) = 3
-f(9, 7) = 1
-f(9, 8) = 1
-f(9, 9) = 9
-...
-f(10, 1) = 1
-f(10, 2) = 2
-f(10, 3) = 1
-f(10, 4) = 2
-f(10, 5) = 5
-f(10, 6) = 2
-f(10, 7) = 1
-f(10, 8) = 2
-f(10, 9) = 1
-f(10, 10) = 10
-f(10, 11) = 1
-f(10, 12) = 2
-...
-#+END_SRC
-
-It took me a while, but I eventually noticed the pattern. =f= is the [[https://en.wikipedia.org/wiki/Greatest_common_divisor][greatest
-common divisor]] function.
diff --git a/org/Writeups for Dennis Yurichev's Reverse Engineering Challenges (#36-#74)/challenges-re-writeups-4.org b/org/Writeups for Dennis Yurichev's Reverse Engineering Challenges (#36-#74)/challenges-re-writeups-4.org
deleted file mode 100644
index 1108af7..0000000
--- a/org/Writeups for Dennis Yurichev's Reverse Engineering Challenges (#36-#74)/challenges-re-writeups-4.org
+++ /dev/null
@@ -1,1150 +0,0 @@
-#+TITLE: Writeups for Dennis Yurichev's Reverse Engineering Challenges (#36-#74)
-#+DATE: <2019-12-29 Sun 19:55>
-#+TAGS: writeup, reverse-engineering, x86
-
-This is the fourth and final set of for my self-imposed challenge of completing
-at least fifty of the exercises on Dennis Yurichev's [[https://challenges.re][challenges.re]] by the end of
-the year. The previous set is available [[http:///jakob.space/challenges-re-writeups-3.html][here]].
-
-We'll actually be covering twenty challenges in this one. I'd been so busy with
-school that I forgot to make a post when I hit forty.
-
-* Challenge #36
-
-The description this time describes that this is "[a] well-known algorithm
-again. What does it do? Also, take notice that the code for x86 uses FPU, but
-SIMD instructions are used instead in the x64 code. That's OK."
-
-#+BEGIN_SRC c
-long state = 0x12345678;
-
-float f1(void)
-{
- state = state * 0x19660d + 0x3c6ef35f;
- return ((float) ((state & 0x7fffff) | 0x40000000)) - 3.0f;
-}
-
-void f(void)
-{
- int i;
- int count;
- float a;
- float b;
-
- for (i = 0, count = 0; i < 1000000; i++) {
- a = f1();
- b = f1();
-
- if (a * a + b * b > 1.0f) {
- count++
- }
- }
-
- ((float) (((double) count) * 2.25) / 10.9073486328125);
-}
-#+END_SRC
-
-I thought this was a lame challenge. The floating point operations of =f1= have
-been optimized to the point that it's unrecognizable, so if you aren't familiar
-with the standard bit-twiddling tricks that GCC uses to speed up floating-point
-operations, you aren't going to be able to come up with anything meaningful --
-especially since neither function take parameters. My response? =f= returns the
-constant value =206282.937500=.
-
-I thought this might be the [[https://en.wikipedia.org/wiki/Fast_inverse_square_root][fast inverse square root]], but I don't believe it is.
-
-* Challenge #37
-
-Ah, another challenge for which the description is that it is a "[w]ell-known
-function" and only x86 disassembly given is from MSVC. Fortunately, this one is
-not too difficult.
-
-#+BEGIN_SRC c
-int f(int a, int b)
-{
- int i;
- int n;
-
- if (a == 0) {
- return b + 1;
- }
-
- n = b;
- i = a;
-
- do {
- if (n == 0) {
- n = 1;
- } else {
- n = f(i, n - 1);
- }
- } while (--i != 0);
-
- return n + 1;
-}
-#+END_SRC
-
-This is the Ackermann function, albeit using a loop rather than a direct
-translation of the Ackermann–Péter function to code.
-
-To answer Yurichev's additional questions, a stack overflow occurs if 4 and 2
-are supplied as input because those are [[https://www.wolframalpha.com/input/?i=Ackermann(4,2)][absurd parameters for this function]], and
-this function bears the error of not enforcing the constraints given in the
-definition of the Ackermann–Péter function.
-
-* Challenge #38
-
-Fun. Another challenge provided as a binary.
-
-#+BEGIN_SRC prog
-jakob@Upsilon ~ $ sha256sum 17
-8f73f329e0988968a9fa40f61da906e83b46817bcb5c0e93f7e95aa74c30e8e0 17
-jakob@Upsilon ~ $ file 17
-17: ELF 64-bit LSB executable, x86-64, version 1 (SYSV), dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2, for GNU/Linux 2.6.18, BuildID[sha1]=bdeac54f2d98db38d7a63a43f1c41857432686c4, stripped
-#+END_SRC
-
-I stopped a bit early because, for once, the question wasn't "[w]hat does this
-code do?", but was instead, "[t]his program prints some information to stdout,
-each time different. What is that?"
-
-#+BEGIN_SRC c
-#include
-#include
-
-static time_t current_time;
-
-int fcn.004006c4(void)
-{
- return current_time = current_time * 0x19660d * 0x3c6ef35f;
-}
-
-int main(int argc, char **argv)
-{
- char *s2;
- void **s1;
- int var_1ch;
- int var_18h;
- int var_11h;
-
- s2 = malloc(230);
- s1 = malloc(80);
- var_1ch = 0;
-
- while (var_1ch <= 9) {
- s1[var_1ch++] = calloc(230, 1);
- }
-
- current_time = time(NULL);
-
- var_1ch = 0;
- while (var_1ch <= 230) {
- var_11h = fcn.00400b60(fcn.004006c4());
- s2[var_1ch++] = var_11h & 1;
- }
-
- var_1ch = 0;
- while (1) {
- fcn.00400970(s2, 230);
- fcn.0040072a(s2, 230, 110);
-
- var_18h = 0;
- while (var_18h <= 8) {
- if (!memcmp(s1[var_18h++], s2, 230)) {
- exit(0);
- }
- }
-
- var_18h = 0;
- while (var_18h <= 8) {
- memcpy(s1[var_18h], s1[++var_18h], 230);
- }
-
- memcpy(s1[9], s2, 230);
- var_1ch++;
- }
-}
-#+END_SRC
-
-The only nondeterminism I saw in the disassembly was from =time=. The actual
-output of the program is incomprehensible -- appearing to be some sort of
-ASCII-art fractal. For this reason, I'm concluding that the information printed
-to =stdout= is the current time.
-
-* Challenge #39
-
-The description for this challenge got me excited. "This program requires a
-password. Find it."
-
-#+BEGIN_SRC prog
-jakob@Upsilon ~ $ sha256sum password2
-8c8365f316de896c453511c5f484755600208b87ad0f1595a2900cbf5a36db24 password2
-#+END_SRC
-
-=main= is simple enough that I feel I can omit the: it reads in a password with
-=scanf=, and then checks it with the following snippet.
-
-#+BEGIN_SRC prog
-│ 0x0804853e e87affffff calll fcn.080484bd
-│ 0x08048543 3df8010000 cmpl $0x1f8, %eax ; 504
-#+END_SRC
-
-We want to find some =password= such that =fcn.080484bd(password) = 0x1f8=.
-Peeking into =fcn.080484bd=, I was a little disappointed.
-
-#+BEGIN_SRC prog
-┌ (fcn) fcn.080484bd 46
-│ fcn.080484bd (int32_t arg_8h);
-│ ; var int32_t var_4h @ ebp-0x4
-│ ; arg int32_t arg_8h @ ebp+0x8
-│ ; CALL XREF from main @ 0x804853e
-│ 0x080484bd 55 pushl %ebp
-│ 0x080484be 89e5 movl %esp, %ebp
-│ 0x080484c0 83ec10 subl $0x10, %esp
-│ 0x080484c3 c745fc000000. movl $0, var_4h
-│ ┌─< 0x080484ca eb10 jmp 0x80484dc
-│ │ ; CODE XREF from fcn.080484bd @ 0x80484e4
-│ ┌──> 0x080484cc 8b4508 movl arg_8h, %eax ; [0x8:4]=-1 ; 8 ; edx
-│ ╎│ 0x080484cf 0fb600 movzbl 0(%eax), %eax
-│ ╎│ 0x080484d2 0fbec0 movsbl %al, %eax
-│ ╎│ 0x080484d5 0145fc addl %eax, var_4h
-│ ╎│ 0x080484d8 83450801 addl $1, arg_8h ; [0x8:4]=-1 ; 1
-│ ╎│ ; CODE XREF from fcn.080484bd @ 0x80484ca
-│ ╎└─> 0x080484dc 8b4508 movl arg_8h, %eax ; [0x8:4]=-1 ; 8 ; edx
-│ ╎ 0x080484df 0fb600 movzbl 0(%eax), %eax
-│ ╎ 0x080484e2 84c0 testb %al, %al
-│ └──< 0x080484e4 75e6 jne 0x80484cc ; likely
-│ 0x080484e6 8b45fc movl var_4h, %eax ; edx
-│ 0x080484e9 c9 leave ; edx
-└ 0x080484ea c3 retl ; edx
-#+END_SRC
-
-Do I even need to provide a C translation? The disassembly should be glaringly
-obvious: this "check" function just returns the sum of the string argument's
-individual bytes. Coming up with a valid password is trivial.
-
-#+BEGIN_SRC prog
-jakob@Upsilon ~ $ ./password2
-enter password:
-AAAAAAA1
-password is correct
-#+END_SRC
-
-The problem also suggests that I "try to change the password by patching the
-executable file," but this doesn't invokve anything more than changing the word
-at =0x08048544=.
-
-* Challenge #41
-
-The question this time is: "[t]his program prints some numbers to stdout. What
-is it?"
-
-#+BEGIN_SRC prog
-jakob@Upsilon ~ $ file problem
-problem: ELF 64-bit LSB executable, x86-64, version 1 (SYSV), dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2, for GNU/Linux 2.6.24, BuildID[sha1]=a89ecf1ae2f2474548d09ca3ebccd7db4162fa1e, stripped
-jakob@Upsilon ~ $ sha256sum problem
-ab3864e8fceeffe4b166cb7481332e88a1fe90b6a406e635c6921119c91a00fd problem
-#+END_SRC
-
-I wrote a C translation without running the program. In retrospect, this wasn't
-a bad idea. The calculation is a function of some integer, but the binary spits
-out subsequent numbers with no sort of delimitation. Having the C translation
-means that I could add a =printf("\n");= after the call to =fcn_00400536(var_4h++);=
-and get output similar to the following:
-
-#+BEGIN_SRC prog
-jakob@Upsilon ~ $ /tmp/test
-1
-
-2
-1
-
-3
-10
-5
-16
-8
-4
-2
-1
-
-4
-2
-1
-
-5
-16
-8
-4
-2
-1
-#+END_SRC
-
-Here's the C translation.
-
-#+BEGIN_SRC c
-void fcn_00400536(int a)
-{
- printf("%d\n", a);
- while (a != 1) {
- if (a & 1 != 0) {
- a = a * 3 + 1;
- } else {
- a >>= 1;
- }
- printf("%d\n", a);
- }
-}
-
-int main(int argc, char **argv)
-{
- int var_4h;
- var_4h = 1;
- while (var_4h <= 15) {
- fcn_00400536(var_4h++);
- }
- return var_4h;
-}
-#+END_SRC
-
-We can pick any interesting sequence and plug it into [[https://oeis.org/search?q=3%2C10%2C5%2C16%2C8%2C4%2C2%2C1&language=english&go=Search][OEIS]], which identifies
-=fcn_00400536= as "A070165: Irregular triangle read by rows giving trajectory of n
-in Collatz problem." Ah, yes. This is looking familiar now. This is the famously
-unsolved problem in mathematics, the [[https://en.wikipedia.org/wiki/Collatz_conjecture][Collatz conjecture]].
-
-* Challenge #43
-
-#+BEGIN_SRC prog
-jakob@Upsilon ~ $ file unknown_utility_2_3
-unknown_utility_2_3: ELF 32-bit LSB executable, Intel 80386, version 1 (SYSV), dynamically linked, interpreter /lib/ld-linux.so.2, for GNU/Linux 2.6.24, BuildID[sha1]=cb74037dd37694879f6250bfb5623c273ef68ca6, stripped
-jakob@Upsilon ~ $ sha256sum unknown_utility_2_3
-9d3df3be78f21971059ba2d9973a1358865ccbe2f47f78fc5800779d6f6083fe unknown_utility_2_3
-#+END_SRC
-
-I really wasn't feeling it today, so I took the easy way out and just ran the
-binary provided on a test file. It spits out a floating point number, which
-seems to decrease as the file becomes less interesting. Just a hunch, but maybe
-it's binary entropy?
-
-#+BEGIN_SRC prog
-jakob@Upsilon ~ $ python -c "print('a' * 256)" > test.txt
-jakob@Upsilon ~ $ ./unknown_utility_2_3 test.txt
-0.036753
-jakob@Upsilon ~ $ rahash2 -a entropy test.txt
-test.txt: 0x00000000-0x00000100 entropy: 0.03675295
-jakob@Upsilon ~ $ dd bs=256 count=1 if=/dev/urandom > test.txt
-1+0 records in
-1+0 records out
-256 bytes copied, 7.0438e-05 s, 3.6 MB/s
-jakob@Upsilon ~ $ ./unknown_utility_2_3 test.txt
-7.069718
-jakob@Upsilon ~ $ rahash2 -a entropy test.txt
-test.txt: 0x00000000-0x000000ff entropy: 7.06971784
-#+END_SRC
-
-Well, that's an answer I'm certainly happy with.
-
-* Challenge #48
-
-It looks like we're starting to get into the realm of =win32=. The question for
-this challenge is, "[w]hat does this win32-function do?"
-
-#+BEGIN_SRC asm
-main:
- push 0xFFFFFFFF
- call MessageBeep
- xor eax,eax
- retn
-#+END_SRC
-
-This is pretty simple. It's a wrapper for =MessageBeep=. According to [[https://docs.microsoft.com/en-us/windows/win32/api/winuser/nf-winuser-messagebeep][MSDN]], the
-=0xFFFFFFFF= parameter produces "[a] simple beep. If the sound card is not
-available, the sound is generated using the speaker."
-
-* Challenge #49
-
-Another rather simple one. The disassembly for this challenge is given in AT&T
-syntax, which is my preferred way of reading x86 assembly.
-
-#+BEGIN_SRC asm
-main:
- pushq %rbp
- movq %rsp, %rbp
- movl $2, %edi
- call sleep
- popq %rbp
- ret
-#+END_SRC
-
-A wrapper around =sleep=, presumably the only provided by =unistd.h=, calling it
-with an argument of two seconds.
-
-* Challenge #52
-
-Another simple disassembly:
-
-#+BEGIN_SRC asm
-$SG3103 DB '%d', 0aH, 00H
-
-_main PROC
- push 0
- call DWORD PTR __imp___time64
- push edx
- push eax
- push OFFSET $SG3103 ; '%d'
- call DWORD PTR __imp__printf
- add esp, 16
- xor eax, eax
- ret 0
-_main ENDP
-#+END_SRC
-
-To copy straight from [[https://docs.microsoft.com/en-us/cpp/c-runtime-library/reference/time-time32-time64?view=vs-2019][MSDN]], this prints the number of "seconds elapsed since
-midnight (00:00:00), January 1, 1970, Coordinated Universal Time (UTC)."
-
-MSDN also answers the follow-up question: "=time= is a wrapper for =_time64= and
-=time_t= is, by default, equivalent to =__time64_t=. If you need to force the
-compiler to interpret =time_t= as the old 32-bit =time_t=, you can define
-=_USE_32BIT_TIME_T=. This is not recommended because your application may fail
-after January 18, 2038; the use of this macro is not allowed on 64-bit
-platforms."
-
-* Challenge #53
-
-I thought this was an interesting challenge. "This code, compiled in Linux
-x86-64 using GCC is crashing while execution (segmentation fault). It's also
-crashed if compiled by MinGW for win32. However, it works in Windows environment
-if compiled by MSVC 2010 x86. Why?"
-
-#+BEGIN_SRC c
-#include
-#include
-
-void alter_string(char *s)
-{
- strcpy (s, "Goodbye!");
- printf ("Result: %s\n", s);
-};
-
-int main()
-{
- alter_string ("Hello, world!\n");
-};
-#+END_SRC
-
-The code is modifying a string constant, which GCC tends to put in a read-only
-memory segment (=.rodata=) in the resultant executable. Writing to a read-only
-memory segment will cause a segmentation fault. I haven't tested it, but the
-question statement makes me think that MSVC puts string constants in a writable
-segment, so this would work just fine.
-
-* Challenge #54
-
-No disassembly is given for this challenge. The only thing on the page is "[w]hy
-isn't the x86 LOOP instruction used by modern compilers anymore?" Some searching
-yields [[https://stackoverflow.com/questions/35742570/why-is-the-loop-instruction-slow-couldnt-intel-have-implemented-it-efficiently/35743699#35743699][this Stack Overflow answer]]. Basically, =loop= is from the time before x86
-became horribly complex, and so on modern processors, it's slow.
-
-* Challenge #56
-
-I decided to skip challenge #55, as it would really just be a walkthrough of
-which r2 commands I used. Challenge #56 is not particularly difficult. I went
-along with the disassembly from MSVC.
-
-#+BEGIN_SRC c
-#include
-
-int main(void)
-{
- int n;
- n = 100;
- do {
- printf("%d", n);
- } while (n-- != 0);
- return 0;
-}
-#+END_SRC
-
-The code prints the integers from 100 to 0.
-
-* Challenge #57
-
-This is almost the same disassembly as last time.
-
-#+BEGIN_SRC c
-#include
-
-int main(void)
-{
- int n;
- n = 1;
- do {
- printf("%d", n);
- n += 3;
- } while (n < 100);
- return 0;
-}
-#+END_SRC
-
-* Challenge #58
-
-This time, we're fortunate enough to be given a disassembly from GCC 4.8.1,
-albeit with =-O3=.
-
-#+BEGIN_SRC c
-int f(char *a)
-{
- int count;
- count = 0;
- while (*a != '\0') {
- if (*a++ == ' ') {
- count++;
- }
- }
- return count;
-}
-#+END_SRC
-
-=f= counts the number of spaces in a given string. As an aside, when I was first
-learning to read assembly, I recall someone describing =-O3= as "unintelligible to
-humans." The more reverse engineering I've done, the more I've realized that the
-optimizations at that level tend to not be as absurd as people make them out to
-be. I considered this to be an easy challenge.
-
-* Challenge #59
-
-This one was /really/ easy.
-
-#+BEGIN_SRC asm
-_a$ = 8
-_f PROC
- mov ecx, DWORD PTR _a$[esp-4]
- lea eax, DWORD PTR [ecx*8]
- sub eax, ecx
- ret 0
-_f ENDP
-#+END_SRC
-
-The function just returns =a * 7=. I suspect the multiplication followed by
-subtraction was an optimization, since multiplication by a power of two can be
-implemented as a left shift.
-
-* Challenge #61
-
-Perhaps the most difficult part of this challenge was going out my way to [[https://float.exposed/0x4014000000000000][ensure
-that the constant really was 5.0]].
-
-#+BEGIN_SRC c
-double f(double a, double b, double c, double d, double e)
-{
- return (a + b + c + d + e) / 5;
-}
-#+END_SRC
-
-=f= simply averages five numbers.
-
-* Challenge #62
-
-The challenge notes that the compiler was optimizing for space, which may
-explain the pointless nested loop.
-
-#+BEGIN_SRC c
-void f(float *a, float *b, float *c)
-{
- int i;
- int j;
-
- long coffee;
- long cake;
-
- coffee = a - b;
- cake = c - b;
-
- for (i = 200; i > 0; i--) {
- for (j = 100; j > 0; j--) {
- b[cake] = b[0] + b[coffee];
- b += 8;
- }
- }
-}
-#+END_SRC
-
-=f= adds 20000 elements from =a= and =b=, storing their sums in =c=.
-
-* Challenge #64
-
-I was swamped with preparing for finals this weekend, so I decided to skip
-challenge #63 in favor of something less arduous. The question for this one is,
-"[a]n array of array[x][y] form is accessed here. Try to determine the
-dimensions of the array, at least partially, by finding y."
-
-#+BEGIN_SRC c
-double f(double *array, int x, int y)
-{
- return array[y + x * 15];
-}
-#+END_SRC
-
-The array has some number of rows each containing 15 elements.
-
-* Challenge #65
-
-The question here is the same as the previous challenge.
-
-#+BEGIN_SRC c
-int f(int *array, int x, int y, int z)
-{
- return array[z + 5 * 16 * (y + 4 * 15 * x)];
-}
-#+END_SRC
-
-Assuming an array of integers, the dimensions of the array are 15 x 20 x ...
-
-* Challenge #74
-
-I skipped way ahead this time because I was done with finals and knew that this
-was the last of the challenges I'd be doing this year. So I looked through what
-remained in search of something difficult, but interesting, and settled on this
-one.
-
-We're given a binary,
-
-#+BEGIN_SRC prog
-jakob@Epsilon ~ $ sha256sum challenge74
-6d2ac11d1e6200d6a2cca988189764b6acdb7811d24619e8e66f1796c8c27394 challenge74
-jakob@Epsilon ~ $ file challenge74
-challenge74: ELF 64-bit LSB executable, x86-64, version 1 (SYSV), dynamically linked, interpreter /lib64/ld-linux-x86-64.so.2, for GNU/Linux 2.6.24, BuildID[sha1]=7fa3bd4aa738bced5aaccb161090818646e07704, stripped
-#+END_SRC
-
-as well as a few valid keys.
-
-#+BEGIN_SRC prog
-2Z7A7-EK270-TMHR4-BHC71-CEB52-HELL0-HELL0-EONP9
-2Z7A7-6I7R9-MZGO9-FDQJ3-JN0Q6-HELL0-HELL0-72KJ9
-#+END_SRC
-
-I took this as an opportunity to try out the [[https://github.com/radareorg/r2ghidra-dec][r2ghidra-dec]] plugin for Radare.
-Let's see how it does.
-
-#+BEGIN_SRC c
-// WARNING: Could not reconcile some variable overlaps
-// WARNING: [r2ghidra] Detected overlap for variable var_20h// WARNING: [r2ghidra] Failed to match type signed int64_t for variable var_10h to Decompiler type: Unknown type
-// identifier signed
-// WARNING: [r2ghidra] Detected overlap for variable var_ch
-// WARNING: [r2ghidra] Failed to match type signed int64_t for variable var_8h to Decompiler type: Unknown type
-// identifier signed
-// WARNING: [r2ghidra] Detected overlap for variable var_8h
-// WARNING: [r2ghidra] Failed to match type signed int for variable var_4h to Decompiler type: Unknown type identifier
-// signed
-// WARNING: [r2ghidra] Detected overlap for variable var_4h
-// WARNING: [r2ghidra] Detected overlap for variable var_bh
-
-undefined8 main(uint32_t argc, char **argv)
-{
- int64_t iVar1;
- char cVar2;
- int32_t iVar3;
- int64_t in_FS_OFFSET;
- int64_t var_30h;
- int64_t var_24h;
- int64_t var_8h;
-
- iVar1 = *(int64_t *)(in_FS_OFFSET + 0x28);
- var_24h._0_4_ = argc;
- sym.imp.puts("Crackme/keygenme by Dennis Yurichev, http://challenges.re/74");
- sym.imp.putchar(10);
- if ((uint32_t)var_24h == 1) {
- sym.imp.puts("Command line: ");
- // WARNING: Subroutine does not return
- sym.imp.exit(0);
- }
- iVar3 = sym.imp.memcmp(argv[1] + 0x1e, "HELL0-HELL0", 0xb);
- if (iVar3 != 0) {
- sym.imp.puts("SN format is incorrect");
- // WARNING: Subroutine does not return
- sym.imp.exit(0);
- }
- iVar3 = fcn.00400bb5((int64_t)argv[1], (int64_t)&var_24h + 4);
- if (iVar3 == -1) {
- sym.imp.puts("SN format is incorrect");
- // WARNING: Subroutine does not return
- sym.imp.exit(0);
- }
- cVar2 = fcn.0040085e((void *)((int64_t)&var_24h + 4));
- if (cVar2 == '\0') {
- sym.imp.puts("SN is not valid");
- } else {
- sym.imp.puts("SN valid");
- }
- if (iVar1 != *(int64_t *)(in_FS_OFFSET + 0x28)) {
- // WARNING: Subroutine does not return
- sym.imp.__stack_chk_fail();
- }
- return 0;
-}
-#+END_SRC
-
-When I saw this, I was blown away. Damn. The NSA did a great job with this.
-Here's my cleaned up version.
-
-#+BEGIN_SRC c
-#include
-
-int main(int argc, char **argv)
-{
- char buf[24];
-
- printf("Crackme/keygenme by Dennis Yurichev, http://challenges.re/74\n\n");
-
- if (argc == 1) {
- puts("Command line: ");
- exit(0);
- }
-
- if (memcmp(argv[1] + 0x1e, "HELL0-HELL0", 0xb)) {
- puts("SN format is incorrect");
- exit(0);
- }
-
- if (fcn_00400bb5(argv[1], buf) == -1) {
- puts("SN format is incorrect");
- exit(0);
- }
-
- if (fcn_0040085e(buf) == '\0') {
- puts("SN is not valid");
- } else {
- puts("SN valid");
- }
-
- return 0;
-}
-#+END_SRC
-
-Aside from getting rid of temporary variables, I removed =iVar1= as it's no more
-than a stack canary, and I fixed up a few "errors" that the decompiler made. As
-an example, notice that strange assignment to =var_24h._0_4_=? Let's see what the
-disassembly says.
-
-#+BEGIN_SRC asm
- pushq %rbp
- movq %rsp, %rbp
- subq $0x30, %rsp
- movl %edi, var_24h ; argc
- movq %rsi, var_30h ; argv
-#+END_SRC
-
-This is the only write to =var_24h=, so the line should have been =var_24h = argv=.
-For some reason, the decompiler saw this as assignment to a =struct= field. I
-ended up removing it anyway. Using 'argc' is clearer.
-
-There's also that odd =(void *)((int64_t)&var_24h + 4)=, but if we look at the
-disassembly,
-
-#+BEGIN_SRC asm
- leaq var_20h, %rdx
- movq %rdx, %rsi
- movq %rax, %rdi
- callq fcn.00400bb5
- ...
- leaq var_20h, %rax
- movq %rax, %rdi
- callq fcn.0040085e
-#+END_SRC
-
-So that should've just been =var_20h= in the decompilation. Regardless, I'm
-impressed. And I have to say, as a plugin, r2ghidra is really good. =pdg= takes a
-few seconds, but if you rename some variables with =afvn= and run it again, it
-spits out the updated version instantly, which makes me think that it's probably
-doing some sort of caching and quick substitution.
-
-Anyway, back to the challenge. We can tell from the decompilation already that
-the sixth and seventh components must be "HELL0-HELL0". It also has to contain
-eight components, delimited by '-', as we can see from =fcn_00400bb5=:
-
-#+BEGIN_SRC c
-var_10h._0_4_ = 0;
-while ((int32_t)var_10h < 7) {
- if (*(char *)(arg1 + (int64_t)((int32_t)var_10h * 6) + 5) != '-') {
- return 0xffffffff;
- }
- var_10h._0_4_ = (int32_t)var_10h + 1;
-}
-#+END_SRC
-
-Here's the gist of the key verification algorithm:
-
-- =fcn_00400bb5= parses the key into a buffer (I renamed this to =parse_key=)
- - Calls out to a =charcode= function which maps numerals to their numeric values
- ('0' becomes 0) and letters 'A' through 'Z' to 10-35.
- - The buffer is written with 3 bytes per component. I thought this was a
- decompiler mistake at first, but I checked the disassembly and it really is
- 3 bytes per component. 24 bytes total.
-- =fcn_0040085e= does further verification and enables features based on the
- parsed key (I renamed this to =enable_features=).
- - The resultant parsed buffer needs to start with 0xdeadbabe.
- - The 4th and 5th bytes give a numerical year, the 6th a numerical month, and
- the 7th a numerical day.
- - There's a sanity checks to ensure that the day is between 1 and 31, that
- the month is between 1 and 12, and that the year is between 2016 and 2101.
- - The 7th bit of byte 8 enables feature A
- - The 1st bit of byte 9 enables feature B
- - The 2nd bit of byte 10 enables feature C
- - The 4th bit of byte 11 enables feature D
- - The 1st bit of byte 12 enables feature E
- - There's one final check of the last 8 bytes against a =checksum= function.
-
-#+BEGIN_SRC c
-#include
-
-uint64_t checksum(int64_t init, char *parsed, int64_t length)
-{
- uint64_t ret;
- char *cur;
- int i;
- int j;
-
- cur = parsed;
- ret = ~init;
- i = length;
-
- while (i != 0) {
- ret = ret ^ (uint64_t) *cur;
- j = 0;
- while (i--, cur++, j < 8) {
- if ((ret & 1) == 0) {
- ret = ret >> 1;
- } else {
- ret = ret >> 1 ^ 0x42f0e1eb0badbad0;
- }
- j++;
- }
- }
-
- return ~ret;
-}
-#+END_SRC
-
-I actually didn't realize that last part until I'd already hacked together a
-quick key verifier.
-
-#+BEGIN_SRC common-lisp
-(use-package :cl-utilities)
-
-(defun charcode (c)
- (let ((value (char-code c)))
- (cond ((<= (char-code #\0) value (char-code #\9)) (- value #x30))
- ((<= (char-code #\A) value (char-code #\Z)) (- value #x37)))))
-
-(defun hash-component (component)
- (let* ((characters (coerce component 'list))
- (values (mapcar #'charcode characters)))
- (unless (or (/= 5 (length values)) (find nil values))
- (+ (* #x000001 (nth 0 values))
- (* #x000024 (nth 1 values))
- (* #x000510 (nth 2 values))
- (* #x00b640 (nth 3 values))
- (* #x19a100 (nth 4 values))))))
-
-(defun parse-key (key)
- (reduce #'append
- (mapcar #'(lambda (component)
- (let ((hash (hash-component component)))
- (list (logand hash #xff)
- (logand (ash hash -8) #xff)
- (logand (ash hash -16) #xff))))
- (split-sequence #\- key))))
-
-(defun key-valid-p (key)
- ;; Must begin with 0xdeadbabe, and have HELL0 for components 6 and 7.
- (and (equal (subseq key 0 4) '(222 173 186 190))
- (equal (subseq key 15 21) '(153 95 15 153 95 15))))
-
-(defun key-attributes (key)
- (let ((parsed (parse-key key)))
- (list :valid (key-valid-p parsed)
- :expiry-year (logior (ash (nth 4 parsed) 8)
- (nth 5 parsed))
- :expiry-month (nth 6 parsed)
- :expiry-day (nth 7 parsed)
- :feature-a (plusp (logand (nth 8 parsed) (ash 1 6)))
- :feature-b (plusp (logand (nth 9 parsed) (ash 1 0)))
- :feature-c (plusp (logand (nth 10 parsed) (ash 1 1)))
- :feature-d (plusp (logand (nth 11 parsed) (ash 1 2)))
- :feature-e (plusp (logand (nth 12 parsed) (ash 1 0))))))
-
-(key-attributes "2Z7A7-EK270-TMHR4-BHC71-CEB52-HELL0-HELL0-EONP9")
-;; (:VALID T :EXPIRY-YEAR 2053 :EXPIRY-MONTH 5 :EXPIRY-DAY 22 :FEATURE-A T
-;; :FEATURE-B T :FEATURE-C T :FEATURE-D T :FEATURE-E NIL)
-
-(key-attributes "2Z7A7-6I7R9-MZGO9-FDQJ3-JN0Q6-HELL0-HELL0-72KJ9")
-;; (:VALID T :EXPIRY-YEAR 2042 :EXPIRY-MONTH 2 :EXPIRY-DAY 21 :FEATURE-A T
-;; :FEATURE-B T :FEATURE-C T :FEATURE-D T :FEATURE-E T)
-#+END_SRC
-
-We can verify our results.
-
-#+BEGIN_SRC prog
-jakob@Epsilon ~ $ ./challenge74 "2Z7A7-EK270-TMHR4-BHC71-CEB52-HELL0-HELL0-EONP9"
-Crackme/keygenme by Dennis Yurichev, http://challenges.re/74
-
-Expiration date: 2053-05-22
-Feature A: ON
-Feature B: ON
-Feature C: ON
-Feature D: ON
-Feature E: OFF
-SN valid
-jakob@Epsilon ~ $ ./challenge74 "2Z7A7-6I7R9-MZGO9-FDQJ3-JN0Q6-HELL0-HELL0-72KJ9"
-Crackme/keygenme by Dennis Yurichev, http://challenges.re/74
-
-Expiration date: 2042-02-21
-Feature A: ON
-Feature B: ON
-Feature C: ON
-Feature D: ON
-Feature E: ON
-SN valid
-#+END_SRC
-
-But, as I mentioned, I'd missed the checksum, so we'll need to deal with that in
-developing a keygen. What makes this so difficult is that the bytes of the
-checksum are incorporated in the checksum value. So, I thought this might be an
-opportunity to add something else to my toolbox: the [[https://en.wikipedia.org/wiki/Z3_Theorem_Prover][Z3 Theorem Prover]].
-
-I'd never used it before, but it seems to show up in CTF writeups quite
-frequently. I did a bit of reading ([[https://jomo.tv/security/mrmcd-ctf-writeup-flag-checker][this]], [[https://ericpony.github.io/z3py-tutorial/guide-examples.htm][this]] and [[https://stackoverflow.com/questions/53726998/using-z3-where-constraint-depends-on-output-of-function][this]]) and put together this:
-
-#+BEGIN_SRC python
-from z3 import *
-
-s = Solver()
-
-def checksum(init, key):
- result = BitVecVal(~init, 64)
-
- for byte in key:
- result ^= ZeroExt(56, byte)
- for i in range(8):
- result = (result >> 1 & 0x7fffffffffffffff) ^ (0x42f0e1eb0badbad0 * (result & 1))
-
- result = ~result
-
- return result
-
-def unpack(word):
- result = BitVecVal(0, 64)
- result |= ZeroExt(56, word[0])
- result |= ZeroExt(56, word[1]) << 8
- result |= ZeroExt(56, word[2]) << 16
- result |= ZeroExt(56, word[3]) << 24
- result |= ZeroExt(56, word[4]) << 32
- result |= ZeroExt(56, word[5]) << 40
- result |= ZeroExt(56, word[6]) << 48
- result |= ZeroExt(56, word[7]) << 56
- return result
-
-key = [BitVec("bv{}".format(i), 8) for i in range(24)]
-
-FEATURE_A = False
-FEATURE_B = False
-FEATURE_C = False
-FEATURE_D = False
-FEATURE_E = False
-
-s.add(key[0] == 222)
-s.add(key[1] == 173)
-s.add(key[2] == 186)
-s.add(key[3] == 190)
-s.add(key[4] == ((2019 & 0xff00) >> 8))
-s.add(key[5] == 2019 & 0x00ff)
-s.add(key[6] == 12)
-s.add(key[7] == 25)
-s.add(key[8] & 0b100000 == (1 if FEATURE_A else 0))
-s.add(key[9] & 0b000001 == (1 if FEATURE_B else 0))
-s.add(key[10] & 0b000010 == (1 if FEATURE_C else 0))
-s.add(key[11] & 0b001000 == (1 if FEATURE_D else 0))
-s.add(key[12] & 0b000001 == (1 if FEATURE_E else 0))
-s.add(key[15] == 153)
-s.add(key[16] == 95)
-s.add(key[17] == 15)
-s.add(key[18] == 153)
-s.add(key[19] == 95)
-s.add(key[20] == 15)
-
-s.add(unpack(key[16:]) == checksum(0, key))
-
-s.check()
-print(s.model())
-#+END_SRC
-
-Accurately translating the checksum function was a pain in the tuckus. The right
-shift was giving me a hard time since the Z3 right shift doesn't prepend with
-zeroes. The =& 0x7fffffffffffffff= is my attempt at dealing with that.
-
-As an aside, I just want to say that GDB's =call= functionality is godsend. It
-made verifying my translation so much easier.
-
-#+BEGIN_SRC prog
-(gdb) p (unsigned long long) $checksum(0, &{'\xff', '\xff', '\xff'}, 3)
-$14 = 18446742974197923840
-#+END_SRC
-
-So, I let this run overnight, which brought me back to when I was more active
-with CTF and would let my half-complete solutions run while I slept.
-
-#+BEGIN_SRC prog
-jakob@Epsilon ~ $ python solver.py
-[bv22 = 196,
- bv13 = 18,
- bv21 = 216,
- bv23 = 130,
- bv14 = 209,
- bv8 = 130,
- bv10 = 108,
- bv9 = 170,
- bv11 = 208,
- bv12 = 240,
- bv20 = 15,
- bv19 = 95,
- bv18 = 153,
- bv17 = 15,
- bv16 = 95,
- bv15 = 153,
- bv7 = 24,
- bv6 = 12,
- bv5 = 227,
- bv4 = 0,
- bv3 = 190,
- bv2 = 186,
- bv1 = 173,
- bv0 = 222]
-#+END_SRC
-
-This was waiting for me when I got back from the gym the next morning.
-
-#+BEGIN_SRC common-lisp
-(string-join
- (mapcar #'ahash-component-inverse
- (mapcar #'triplet-to-number '((222 173 186)
- (190 0 27)
- (12 24 13)
- (170 108 208)
- (240 18 20)
- (153 95 15)
- (153 95 15)
- (216 196 130))))
- "-")
-#+END_SRC
-
-#+BEGIN_SRC prog
-CL-USER> (string-join
- (mapcar #'ahash-component-inverse
- (mapcar #'triplet-to-number '((222 173 186)
- (190 0 27)
- (12 24 13)
- (170 108 208)
- (240 18 20)
- (153 95 15)
- (153 95 15)
- (216 196 130))))
- "-")
-"2Z7A7-AHX11-S4EI0-6LR48-K37S0-HELL0-HELL0-KPO35"
-CL-USER> (key-attributes "2Z7A7-AHX11-S4EI0-6LR48-K37S0-HELL0-HELL0-KPO35")
-(:VALID NIL :EXPIRY-YEAR 27 :EXPIRY-MONTH 12 :EXPIRY-DAY 24 :FEATURE-A NIL
- :FEATURE-B NIL :FEATURE-C NIL :FEATURE-D NIL :FEATURE-E NIL)
-#+END_SRC
-
-Oh no...
-
-#+BEGIN_SRC python
-...
-s.add(key[4] == 2019 & 0xff00)
-...
-#+END_SRC
-
-That should've been =s.add(key[4] == ((2019 & 0xff00) >> 8))=...
-
-;-;
-
-Let's try this again.
-
-#+BEGIN_SRC prog
-jakob@Epsilon ~ $ python solver.py
-[bv22 = 80,
- bv13 = 39,
- bv21 = 204,
- bv23 = 133,
- bv14 = 124,
- bv8 = 140,
- bv10 = 12,
- bv9 = 168,
- bv11 = 183,
- bv12 = 184,
- bv20 = 15,
- bv19 = 95,
- bv18 = 153,
- bv17 = 15,
- bv16 = 95,
- bv15 = 153,
- bv7 = 25,
- bv6 = 12,
- bv5 = 227,
- bv4 = 7,
- bv3 = 190,
- bv2 = 186,
- bv1 = 173,
- bv0 = 222]
-#+END_SRC
-
-This time it actually ran for a whole two days.
-
-#+BEGIN_SRC prog
-CL-USER> (mapcar #'hash-component-inverse
- (mapcar #'triplet-to-number
- '((222 173 186)
- (190 7 227)
- (12 25 140)
- (168 12 183)
- (184 39 124)
- (153 95 15)
- (153 95 15)
- (204 80 133))))
-("2Z7A7" "YFWU8" "CGSG5" "CF457" "K9EU4" "HELL0" "HELL0" "OH975")
-CL-USER> (key-attributes "2Z7A7-YFWU8-CGSG5-CF457-K9EU4-HELL0-HELL0-OH975")
-(:VALID T :EXPIRY-YEAR 2019 :EXPIRY-MONTH 12 :EXPIRY-DAY 25 :FEATURE-A NIL
- :FEATURE-B NIL :FEATURE-C NIL :FEATURE-D NIL :FEATURE-E NIL)
-#+END_SRC
-
-#+BEGIN_SRC prog
-jakob@Epsilon ~ $ ./challenge74 "2Z7A7-YFWU8-CGSG5-CF457-K9EU4-HELL0-HELL0-OH975"
-Crackme/keygenme by Dennis Yurichev, http://challenges.re/74
-
-Expiration date: 2019-12-25
-Feature A: OFF
-Feature B: OFF
-Feature C: OFF
-Feature D: OFF
-Feature E: OFF
-SN valid
-#+END_SRC
-
-There we go. A working keygen! (Provided you're willing to wait).
-
-* An End-of-Year Reflection
-
-This was fun, but I think in planning this out, I should have preferred depth
-over breadth, like getting through some of the challenges on [[http://reversing.kr/index.php][reversing.kr]]. The
-challenges I got the most out of were the ones I had to spend more than a day
-reversing. Another thing that made regret the choice of Dennis Yurichev's
-challenges is the significance of context in reverse engineering. Most of these
-challenges give little more than a disassembly. There are exceptions --
-challenge #33, for example, was one I was able to solve because the description
-said that it was a cryptographic function. But for the most part, I think being
-able to see the "big picture" would have been a more realistic way to practice
-my reverse engineering chops.
-
-One idea I've been toying with is putting out a crackme on a monthly basis.
-Infrequent enough that it wouldn't be overwhelming, and I'd be able to make it a
-sizeable challenge. I'd be able to give out hints every week, and post the
-solution at the end of the month. Actually, I may do this through the [[https://ctf.cs.umass.edu/][wargames]]
-site we're putting together at university. Stay tuned!
diff --git a/org/Writeups for PlaidCTF 2019/plaidctf-2019.org b/org/Writeups for PlaidCTF 2019/plaidctf-2019.org
deleted file mode 100644
index 8491347..0000000
--- a/org/Writeups for PlaidCTF 2019/plaidctf-2019.org
+++ /dev/null
@@ -1,456 +0,0 @@
-#+TITLE: Writeups for PlaidCTF 2019
-#+DATE: <2019-04-14 Sun>
-#+TAGS: writeup, security, reverse-engineering, capture-the-flag, x86, c, python
-
-My long-lived hiatus from capture-the-flag has come to an end, as I got off my
-ass this weekend to play in PlaidCTF 2019. Being a one-man team is pretty
-lonely, but my old team wasn't playing, and even if they were, I don't know if I
-would've wanted to make the commute just to play with them.
-
-The team name I came up with was 0x7c_Jake since I've been listening to a lot of
-[[https://en.wikipedia.org/wiki/Less_Than_Jake][Less than Jake]] recently and =0x7c= is =jl= in x86. With any luck, though, I won't be
-playing under that team name again -- I'm going to reach out to the ACM chapter
-at my university and ask about starting a team associated with the school.[fn:1]
-
-But I'd imagine that you don't care much for that. You're here for my challenge
-solutions, aren't you?
-
-* can you guess me (100 pts)
-
-This was a pretty simple Python sandbox escape challenge. The constraint was
-that your input could have a maximum of 10 unique characters.
-
-#+BEGIN_SRC python :hl_lines 0
-count_digits = len(set(inp))
-if count_digits <= 10: # Make sure it is a number
- val = eval(inp)
-else:
- raise
-#+END_SRC
-
-So if you were thinking of sending off =print(secret_value_for_password)=, you're
-out of luck.
-
-#+BEGIN_SRC python :hl_lines 0
-f = lambda x: (len(set(x)) <= 10, len(set(x)))
-f("secret_value_for_password") # >>> (False, 15)
-#+END_SRC
-
-This was the challenge I poked at for warm up, and in about fifteen minutes I
-had what I believe is an unintended solution.
-
-#+BEGIN_SRC prog
- ____ __ __ ____ __ __
- / ___|__ _ _ _\ \ / /__ _ _ / ___|_ _ ___ ___ ___| \/ | ___
-| | / _` | '_ \ V / _ \| | | | | _| | | |/ _ \/ __/ __| |\/| |/ _ \
-| |__| (_| | | | | | (_) | |_| | |_| | |_| | __/\__ \__ \ | | | __/
- \____\__,_|_| |_|_|\___/ \__,_|\____|\__,_|\___||___/___/_| |_|\___|
-
-
-
-Input value: help(flag)
-No Python documentation found for 'PCTF{hmm_so_you_were_Able_2_g0lf_it_down?_Here_have_a_flag}'.
-Use help() to get the interactive help utility.
-Use help(str) for help on the str class.
-
-Nope. Better luck next time.
-#+END_SRC
-
-* i can count (50 pts)
-
-The premise of this challenge is that there's some integer encoded as an ASCII
-string. It's continually incremented by one and then checked against a
-=check_flag=[fn:2] function. The flag is just whatever integer satisfies =check_flag=.
-
-You certainly _could_ have reverse engineered =check_flag= and plugged all of its
-constraints into z3, but the function is 1394 bytes long. An easier solution is
-to realize that the constraints are checked for each digit of the integer, open
-the program in a debugger, set some breakpoints at various points in =check_flag=,
-and brute-force the value digit-by-digit.
-
-This would've been a nice opportunity to use r2pipe or GDB's Python APIs, but I
-started this challenge close enough to the end of the competition that doing it
-by hand in GDB was the best course of action. I broke at =check_flag+0x31= so I
-could see what the individual digit being checked was, as well as at
-=check_flag+0x532= so I could see if the function was jumping to a =ret= -- which
-would indicate that the digit doesn't satisfy the constraints. Every time I came
-across a correct digit, I'd add a bogus '/' to the end of the integer string
-with =set *((char *)0x56555000+0x3048) = 0x2f=[fn:3] so that =check_flag= started
-checking the following digit, rather than incrementing the integer and ruining
-everything. Again, the return key on my keyboard would have appreciated it if I
-scripted my solution, but it worked and I was able to get the flag of
-"PCTF{2052419606511006177}".
-
-* big_maffs (250 pts)
-
-I found this challenge to be really difficult, and at the time of writing this,
-my solution is still running. I began by reverse engineering the binary to its
-equivalent C.
-
-#+BEGIN_SRC c :hl_lines 0
-#include
-#include
-#include
-#include
-
-struct string {
- uint64_t length;
- char *data;
-};
-
-static char peanut[] = {
- 0x05, 0xbb, 0x01, 0x59, 0x6f, 0x06, 0x18, 0x61, 0x3d, 0xa0,
- 0x3a, 0xe4, 0x9c, 0xe4, 0xe1, 0xe6, 0x73, 0x93, 0x81, 0xf2,
- 0x10, 0x6b
-};
-
-static char banana[] = {
- 0x00, 0x01, 0x00, 0x01, 0x00, 0x01, 0x01, 0x01,
- 0x00, 0x00, 0xff, 0xff, 0x00, 0x00, 0x00, 0x00,
-};
-
-static struct string *global_4090;
-
-
-// 0x00001189 1 26 eom_error
-void eom_error(void)
-{
- puts("no more memory? https://downloadmoreram.com/");
- exit(1);
-}
-
-// 0x000011a3 3 51 my_malloc
-void *my_malloc(int size)
-{
- char *ret;
- if ((ret = malloc(size)) == NULL) {
- eom_error();
- }
- return ret;
-}
-
-// 0x000011d6 3 62 my_realloc
-void *my_realloc(char *data, int length)
-{
- char *res;
-
- // STACK SIZE 0x20
- if ((res = realloc(data, length)) == NULL) {
- eom_error();
- }
-
- return res;
-}
-
-// 0x00001214 1 97 make_string
-struct string *make_string(char *data, int n)
-{
- struct string *ret;
-
- // STACK SIZE 0x20
- ret = my_malloc(sizeof(struct string));
- ret->data = my_malloc(n);
- memcpy(ret->data, data, n);
- ret->length = n;
-
- return ret;
-}
-
-// 0x00001695 7 72 all_null?
-int all_null(struct string *s)
-{
- int null_count;
-
- null_count = 0;
- while (null_count < s->length) {
- if (s->data[null_count] == '\0') {
- null_count++;
- } else {
- return 0;
- }
- }
-
- return 1;
-}
-
-// 0x000016dd 8 146 ends_with_digit?
-int ends_with_digit(struct string *s)
-{
- int i;
-
- // STACK SIZE 0x18
- if (all_null(s)) {
- return 0;
- }
-
- i = s->length - 1;
-
- while (i >= 0) {
- if (s->data[i] == '\0') {
- i--;
- } else {
- // True for c > 64, as well as the following cases:
- // - c == 1
- // - 4 <= c <= 7
- // - 16 <= c <= 31
- return (s->data[i] & 0xaa) > (s->data[i] & 0x55);
- }
- }
-
- return 0;
-}
-
-// 0x00001275 1 70 resize_string_by_one
-void resize_string_by_one(struct string *s)
-{
- // STACK SIZE 0x10
- s->length++;
- s->data = my_realloc(s->data, s->length);
-}
-
-// 0x000012bb 21 492 strum
-void strum(struct string *a, struct string *b)
-{
- int onion;
- int brisket;
- int cheese;
- char donut;
- char syrup;
- char carrot;
- char melon;
- char butter;
-
- // STACK SIZE 0x30
-
- butter = '\0';
- cheese = 0;
-
- // 0x13c3
- while (cheese < b->length) {
- melon = '\0';
- brisket = 0;
-
- while (brisket < 8) {
- syrup = butter \
- + ((a->data[cheese] >> brisket) & 1) \
- + ((b->data[cheese] >> brisket) & 1);
-
- if (banana[syrup + 2] != '\0') {
- melon |= 1 << brisket;
- }
-
- butter = banana[syrup + 8];
- brisket++;
- }
-
- if (a->length == cheese) {
- resize_string_by_one(a);
- }
-
- a->data[cheese] = melon;
- cheese++;
- }
-
- while (butter != '\0') {
- if (cheese >= a->length) {
- resize_string_by_one(a);
- }
-
- carrot = '\0';
- onion = 0;
-
- while (onion < 8) {
- donut = butter + ((a->data[cheese] >> onion) & 1);
-
- if (banana[donut + 2] != '\0') {
- carrot |= 1 << onion;
- }
-
- butter = banana[donut + 8];
- onion++;
- }
-
- a->data[cheese] = carrot;
- cheese++;
- }
-}
-
-// This function is extremely similar to strum, but with 'subl %eax, %esi; movl
-// %esi, %eax' at 0x00001335 instead of 'addl %esi, %eax'.
-void bake(struct string *a, struct string *b)
-{
- int onion;
- int brisket;
- int cheese;
- char donut;
- char syrup;
- char carrot;
- char melon;
- char butter;
-
- // STACK SIZE 0x30
-
- butter = '\0';
- cheese = 0;
-
- // 0x13c3
-
- while (cheese < b->length) {
- melon = '\0';
- brisket = 0;
-
- while (brisket < 8) {
- syrup = butter \
- + ((a->data[cheese] >> brisket) & 1) \
- - ((b->data[cheese] >> brisket) & 1);
-
- if (banana[syrup + 2] != '\0') {
- melon |= 1 << brisket;
- }
-
- butter = banana[syrup + 8];
- brisket++;
- }
-
- if (a->length == cheese) {
- resize_string_by_one(a);
- }
-
- a->data[cheese] = melon;
- cheese++;
- }
-
- while (butter != '\0') {
- if (cheese >= a->length) {
- resize_string_by_one(a);
- }
-
- carrot = '\0';
- onion = 0;
-
- while (onion < 8) {
- donut = butter + ((a->data[cheese] >> onion) & 1);
-
- if (banana[donut + 2] != '\0') {
- carrot |= 1 << onion;
- }
-
- butter = banana[donut + 8];
- onion++;
- }
-
- a->data[cheese] = carrot;
- cheese++;
- }
-}
-
-struct string *gaze(struct string *a, struct string *b)
-{
- struct string *local_8;
- struct string *local_10;
- struct string *local_18;
- struct string *local_20;
- struct string *local_28;
-
- // STACK SIZE 0x40
-
- if (all_null(a)) {
- local_28 = make_string("\x00", 1);
- strum(local_28, b);
- strum(local_28, global_4090);
- return local_28;
- }
-
- if (all_null(b)) {
- local_20 = make_string("\x00", 1);
- strum(local_20, a);
- bake(local_20, global_4090);
- return gaze(local_20, global_4090);
- }
-
- local_18 = make_string("\x00", 1);
- strum(local_18, b);
- bake(local_18, global_4090);
-
- local_10 = gaze(a, local_18);
-
- local_8 = make_string("\x00", 1);
- strum(local_8, a);
- bake(local_8, global_4090);
-
- return gaze(local_8, local_10);
-}
-
-void fcn_176f(struct string *a, struct string *b)
-{
- // STACK SIZE 0x10
- while (!ends_with_digit(a)) {
- bake(a, b);
- }
- strum(a, b);
-}
-
-// 0x00001935 4 230 main
-int main(int argc, char **argv)
-{
- struct string *local_8;
- struct string *local_10;
- struct string *local_18;
- int local_1c;
-
- // STACK SIZE 0x20
- global_4090 = make_string("\x01", 1);
-
- puts("Generating your flag, please wait warmly...");
-
- local_18 = make_string("\x1e", 1);
- local_10 = gaze(local_18, local_18);
-
- local_8 = make_string((void *) 0x206e, 0x17);
- fcn_176f(local_10, local_8);
-
- local_1c = 0;
-
- while (local_1c <= 0x15) {
- peanut[local_1c] ^= local_10->data[local_1c];
- local_1c++;
- }
-
- printf("Your flag is: %s\n", peanut);
- return 0;
-}
-#+END_SRC
-
-TL;DR: among other things, there's a function called =gaze=[fn:4] that recursively
-generates an XOR decryption key for =peanut=.
-
-I took this be an "optimize me" challenge. My current solution memoizes the
-results of =gaze= into a linked list to reduce the number of recursive
-computations made. In retrospect, I probably should've used a binary search tree
-or a hash table instead of a linked list, but I was trying to quickly hack
-together a solution. Also in retrospect, I probably should spent my time
-figuring out what =strum= and =bake= _really_ do and reversing the calculation rather
-than trying my hand at optimizing it. Ah, well.
-
-One neat thing I found out about from working on this challenge was the
-=MALLOC_CHECK_= environment variable recognized by glibc. If it's set to =0=, heap
-corruption errors are silently ignored. My solution needed it, and I'm unsure of
-whether the heap corruption is in my translation of the original binary, or if
-it was in my memoization code. Either way, I have a feeling it will make itself
-useful again in the near future.
-
----
-
-Addendum: As it turns out, memoization was a wildly sophomoric attempt at a
-solution, and the real solution was, as I mentioned, to figure out the purposes
-of =strum= and =bake=. It turns out that =strum= is base (-2) addition, =bake= is base
-(-2) subtraction, =gaze= is the Ackermann function, and that the structure is
-actually a [[https://en.wikipedia.org/wiki/Arbitrary-precision_arithmetic][bignum]], not a string. In this case, that poor assumption led me down
-a wrong path. Once you figure that out, you'll need to put your modular
-arithmetic chops to work as well. An excellent writeup from sasdf of [[https://balsn.tw/][Balsn]] is
-available [[https://sasdf.cf/ctf/writeup/2019/plaid/rev/bigmaffs/][here]].
-
-[fn:1] So if you currently study at UMass Amherst and you'd be interested in joining a CTF team, [[http://jakob.space/about/][shoot me an email!]]
-[fn:2] The executable wasn't stripped.
-[fn:3] Where =0x56555000= is the address that the binary was loaded to in memory, and =0x3048= is the beginning of the ASCII-encoded integer (plus an offset for whichever digit I was on)
-[fn:4] This time the binary _was_ stripped. I didn't bother updating the temporary names I used. Yes, I use foods for variables and random verbs for functions.
--
cgit v1.3