jtpaasch

QEMU

Some quick tips for using QEMU from the command line (on macOS, but should work on Linux too).

Creating and booting an image

Download an OS ISO, e.g., the netinstall Debian 9.7 ISO:

wget https://cdimage.debian.org/debian-cd/current/amd64/iso-cd/debian-9.7.0-amd64-netinst.iso

jtpaasch

(** 

MAKEFILE:

plugin = primus_evaluator_example

all: clean build install

build:
        bapbuild -pkg bap-primus -tags 'warn(A)' $(plugin).plugin

jtpaasch

BIL

To run the examples below, open baptop, then:

open Bap.Std;;

Documentation

• https://binaryanalysisplatform.github.io/bap/api/master/Bap.Std.Bil.html

jtpaasch

(*********************************************************)
(** Simple functor example. *)

(** A simple signature. *)
module type X = sig
  val x : int
end

(** Here's a fuctor. 
 *  It takes an input: [M], which is an implementation

jtpaasch

Analyzing binaries

Useful tutorials:

• https://reverseengineering.stackexchange.com/a/1936
• https://cs.dartmouth.edu/~sergey/cs108/dyn-linking-with-gdb.txt

LDD

Show the dynamically linked libraries:

jtpaasch

module Token = struct

  type t =
    | L_array_bracket
    | R_array_bracket
    | L_object_bracket
    | R_object_bracket
    | Colon
    | Comma

jtpaasch

Running/Compiling OCaml

Tutorial/cheat sheat for running/compiling OCaml.

Style guideline

• https://ocaml.org/learn/tutorials/guidelines.html

jtpaasch

Option (from Jane Street Core)

Convert a value to an optional something:

let some_message = Option.some "goodbye";;

Suppose you have some data:

jtpaasch

Sequence (from Jane Street Core)

Suppose you have a list.

let x = ["a"; "b"; "c"];;

Convert it to a sequence:

jtpaasch

(** * Tactics: More Basic Tactics *)

(** This chapter introduces several additional proof strategies
    and tactics that allow us to begin proving more interesting
    properties of functional programs.  We will see:

    - how to use auxiliary lemmas in both "forward-style" and
      "backward-style" proofs;
    - how to reason about data constructors (in particular, how to use
      the fact that they are injective and disjoint);