Typestate Checking of Machine Code

摘要: We check statically whether it is safe for untrusted foreign machine code to be loaded into a trusted host system. Our technique works on ordinary code, and mechanically synthesizes (and verifies) safety proof. earlier work along these lines was based C-like type system, which does not suffice whose origin C++ source code. In the present paper, we address this limitation with an improved typestate system introduce several new techniques, including: summarizing effects of function calls so that our analysis can stop at boundaries, inferring information about sizes types stack-allocated arrays, symbolic range propagating array bounds. These techniques make approach checking more precise, efficient, able handle larger collection real-life sequences than previously case.