Critical applications and increasing scale of software hasmade software assurance a big problem. Currently, programmers can write type-safe codes in typed languageswith sound type systems, such as Java, Cyclone, even typed assembly language(TAL). But high assurance does mean not only type safe, but also correctness and security. Since type is not expressive enough, there are still no high assurance software released in typed language, especially operating system and runtime library, which are infrastructure softwares in the computing system. Logic predicates are more expressive than types, thus substituting types with logic predicates as program specification seems a good idea. In this paper, we present a certified dynamic storage allocation library (malloc/free) in SCAP, which is a new MIPS-like assembly language with expressive and power specification structure. And we encode the SCAP language and the certified library in a modern higher-order logic(HOL) proof assistant Coq. In this work, we confirm the expressiveness and modularity of SCAP. So we can expect SCAP to be a expressive target language for some safe high-level languages in the future.