Typing for Machine Language and Safety Checking for Machine Code

Based on the idea of type systems, this paper reengineers a new set of type expressions and a type system for machine code of Intel/x86’s infrastructure Although machine language program is a binary untyped code, types of its registers and memory exist implicitly in semantics of instructions The type inferring algorithm built on type systems can statically infer safety of the machine code The machine language discussed includes some of important characters, such as jumps, function call, return, and so on, and shows that the approach can be applied to type checking for low level code of other infrastructures