Fundamental safety properties of machine code such as memory safety could be subsumed by type safety, so if the code is type
safe, then it satisfies the fundamental safety policy. We present a new approach based on ELF logical framework to check type
safety of machine code, and implement a prototype system to do experiments on sample programs.