[Binary Code Analsysis - Reading Critique] WYSINWYX

The paper addresses the idea that the source code is not what is actually executed. This idea is defined as the WYSINWYX (What You See Is Not What You eXecute) phenomenon. The paper elaborates more on this phenomenon by showing concrete examples in program compilation and execution. The author explains that such phenomenon is caused due to the operations of compilers such as dead code elimination, reordering instruction, and optimizations, etc. The author positions his stance that high-level code analysis fails to capture lost details during the compilation process causing many vulnerabilities of the software to be exposed.

The author continues by stressing some advantages binary level analysis has over static code analysis. Some of those advantages is that such technique do not need any source code, availability to recognize modification operated by compilers, and entire program including libraries can be analyzed at once, etc. 

Finally, the author shares their work of a tool that analyzes a x86 executable, named "CodeSurfer/x86". The tool works by recovering IR (intermediate representation) from the binary by utilizing IDAPro with VSA (value-set analysis) which is an algorithm to analyse static information retrieved from IDA. The collection of IR built by VSA is then passed to the path inspector which provides interrfaces for model-checking facilities. At the model checking stage, processed by WPDS++, the reachability to vulnerability states are checked.

The paper has done a great job of introducing the motivation of the advantage binary analysis has over static analysis with easy to understand concrete examples and how they have built their own tool. However, I believe the paper could have concluded stronger if they have shown that the final output (IR and model checking results) given by CodeSurfer/x86 is actually valid. How can we validate that the recovered IR is valid?