?
A Memory Model for Deductively Verifying Linux Kernel Module
Several previous evaluations of memory models for SMT-based deductive verification tools have shown that the choice of memory model may significantly affect both the number of automatically discharged verification conditions and the capabilities of the verification tool. One of the most efficient memory models for deductive verification of low-level C code is based on region analysis and component-as-array modeling. However, originally this model doesn’t support many C language idioms widely used in low-level system code including the Linux kernel. The paper suggests a modification of this model that extends it with full support for arbitrarily nested structures, unions and arrays, arbitrary pointer arithmetic and general pointer type casts. The extension for nested structures and arrays requires no additional annotation overhead. The support for pointer arithmetic, unions and pointer type casts generally requires user annotations. The proposed model fully preserves the performance of the original memory model for earlier supported code. Preliminary practical evaluation on an industrial security kernel module showed a small specification overhead required for code where the proposed model is not fully automatic.