L4, the second-generation of microkernel, greatly compensates for the shortcomings of the first-generation of microkernel in flexibility and performance, which has attracted the attention of academia and industry. The kernel is the basic component for implementing the operating system. Once it has errors, it may cause the breakdown of whole system, further causing losses to users. Therefore, it is very important to improve the correctness and reliability of the kernel. Virtual memory subsystem is a key mechanism to implement L4 kernel. This study focuses on the formal modeling and verification of this mechanism. A formal model is presented, which involves all operations of mapping mechanism, all management operations of address space, and MMU behavior with TLB. The properties of functional correctness, safety, and security are formalized. Through reasoning about partial correctness, invariants and unwinding conditions, it is shown that the proposed model satisfies these properties in the theorem prover Isabelle/HOL. During modeling and verification, three problems are found related to functional correctness and security in source code. The corresponding solutions or suggestions are given in this study as well.