Software failures can be very grievous, causing deaths, losing money, etc. In this situation, we may want to prove that the code is correct: it does not crash, it does what we expect, it does not leak sensitive information… Abstract interpretation provides a way for proving such properties using overapproximation of the semantics. Our study case is the operating system of a host platform in planes that lies at the boundary between trusted and untrusted world. Thus, we want to prove that untrusted code can’t affect trusted code. We need to extend the C analyzer we are developing since the OS code contains blocks of inline x86 assembly in the C code. Moreover, the properties we want to prove are not expressible at the C level: we need the more precise semantics of assembly.