In the past decades, there are lots of researches on language-based techniques to achieve the safety and security of low-level code. Typed assembly language and typed intermediate language like Flint are designed as target languages in certifyin