Operating system (OS) kernels are the basis of designing safety-critical software systems. The correct running of any computer systems relies on the correctness of the underlying OS kernels, therefore, it is highly desirable to verify the correctness of OS kernels formally. However, the behavior such as multi-task concurrency, data sharing and race that exist in OS, brings great challenge to the verification of OS kernels. Recently, the theorem proving based methods have been applied for the formal verification of OS functionality modules, and achieved some successful applications. OS kernel capability-based access control module provides a fine-grained access control, designed to prevent unauthorized users from accessing system kernel resources and services. In the implementation of the capability-based access control, the capability spaces of all tasks form a set of tree structures, and at the same time each capability node contains nested complex data structures, plus the widespread operations in capability functions including access, modification, and (recursive) deletion to capability space, make the formal verification of capability-based access control more difficult compared to other OS modules. In this paper, based on concurrent separation logic with refinement CSL-R, we have verified the functional correctness of capability-based access control of an OS kernel in aerospace embedded field, by proving the refinement between capability API functions and their abstract specification. We first formally define the capability data structure, based on which we define the global capability invariant to keep the consistency of the capability spaces; then, we define the pre/post-conditions for internal functions and the abstract specification for API functions that reflect their functional correctness; and finally, we prove the refinement between the C implementation for API functions and their abstract specification. All the above definitions and verification are formalized in Coq theorem prover. During verification, we found errors for the C implementation, which have been confirmed and modified by the designer of the OS kernel.