Towards deductive verification of C programs with shared data

The paper takes a look at the problem of deductive verification of Linux kernel code that is concurrent and involves accesses to shared data and interactions with highly concurrent environment. The presence of shared data does not allow to apply traditional deductive verification techniques based solely on function contracts and loop invariants, so we consider verification of such code using type invariants and a particular object-oriented methodology. For Linux kernel modules one of the usual goals of deductive verification is a formal proof of the code's compliance to a specification of a synchronization discipline. We propose formalizing both the synchronization discipline and the required properties of the code in terms of ownership methodology with locally checked invariants (LCI) that was previously successfully applied for verifying the Microsoft Hyper-V Hypervisor with VCC deductive verification tool. However to maintain good compatibility with the various specific C features and extensions used in the Linux kernel code, efficiently handle data type representations with many large nested structure definitions and provide a reacher specification language we propose using Frama-C static analysis platform with its ACSL specification language and Jessie plugin for deductive verification as these tools have shown a good applicability to verification of sequential Linux kernel code fragments in the course of the Astraver project. The paper presents preliminary discussion of issues arising from integration of support for the ownership methodology and LCI into both the ACSL specification language and its underlying toolset. In particular, the issue of reusing existing ACSL specifications in sequential context and the related issue of establishing a correspondence between ACSL notion of validity and LCI notions of owned, wrapped and closed object are discussed. The overall approach to specification of concurrent kernel code using ownership methodology, LCI and ACSL specification language is demonstrated on examples of spinlock specification and a simplified specification of RCU (Read-copy-update) API.