Instruction Semantics: Related Work

Comparisions

Instructions support comparision (intel opcodes)

Tool	Instruction Support Status
Total Att instructions	3868
Total Att/Intel Opcodes	1281/982

Comparision A Vs B	A	B	A-B	B-A	A & B
A: Strata B: McSema	393	498	173	278	220
A: Strata Vector Imms B: McSema	76	498	43	465	33
A: ACL2 B: Strata	191	393	67	269	124
A: ACL2 B: McSema	191	498	29	336	162
A: Strata/Stoke Unsupported B: McSema	107	498	61	452	46

Other Related Work

• From inX to MINC

  • They defined two languages, MinX and MinC, roughly corresponding to simplified subsets of x86 and C. He then defined a semantics-preserving compilation relation between MinC and MinX, and uses this as a way to determine correctness of a certain machine-code type inference algorithm.

• Evolving Exact Decompilation

  • This paper is more about correct decompilation from binary to C. The idea is to do byte equivalence of binary and the recompiled binary from candidate C codes. The cndidates are chozen from a big corpus and applied with guided slource to source mutation before recompilation.

• Angr (using VEX as the IR for analysis)

  • https://www.youtube.com/watch?v=eqaddt9ssbQ

• Rocksalt

  • Parser

• SaltShaker

• Compcert

• x86proved

  • https://x86proved.codeplex.com/
  • Extend the model to cover more features of x86 e.g. instructions, floating point, 64-bit, SIMD, paging, multi-core
  • Improve the automation of proofs
  • Languages

• LLVM's backend X86 semantic table

• ACL2

  • x86isa Documentation

• The Semantics of x86 Multiprocessor Programs

• Include semantics for each instruction

• ACL2: http://www.cs.utexas.edu/users/moore/acl2/manuals/current/manual/index-seo.php/X86ISA____IMPLEMENTED-OPCODES

• https://alastairreid.github.io/specification_languages/: Last paragraph

• Testing Intermediate Representations for Binary Analysis

  • Differentially test Valgrind, BAP and BINSEC.
  • Convert the semantics in individual IR to UIR and then to Z3 formulas to run Z3 on them.
  • Does not condifer floating pount instructions.
  • Test one instruction at a time.
  • SKip testing an instruction whenever the convertion to UIR is difficult.

Projects hoisting a semantics of x86

• ANGR using VEX
  • IR details: https://docs.angr.io/docs/ir.html
  • The speed of angr as an analysis tool or emulator is greatly handicapped by the fact that it is written in python (https://docs.angr.io/docs/speed.html)
  • Angr (using VEX) has an excellent instruction Support. We had the vex representation of all the register variants from angr project at here
• BAP
• BINSEC
• QEMU
• MCSEMA
• RADARE2
  • The IR is called ESIL.
  • Not easy to read. (https://monosource.gitbooks.io/radare2-explorations/content/tut3/tut3_-_esil.html)
  • Can interpret ESIL (https://radare.gitbooks.io/radare2book/content/disassembling/esil.html)
  • Lacks FP support.
  • Completeness Check: Out of 1083 register instructions, 664 are not supported!

       cd binary-decompilation/x86-semantics/docs/instruction_manuals/instruction_instances/Registers
       ~/x86-semantics/scripts/process_spec.pl --radare2_support  --file ~/x86-semantics/docs/relatedwork/strata/Registers/register_instructions.txt |& tee  ../../../relatedwork/radare2/register_instr_support.txt