Methodology for Specification and Verification of High-Level Requirements with MetAcsl

Specification and formal verification of high-level properties (such as security properties, like data integrity or confidentiality) over a large software product remains an important challenge for the industrial practice. Recent work introduced METACSL, a plugin of the FRAMA-C verification platform, that allows the user to specify high-level properties, called HIgh-Level ACSL REquirements or HILARE, for C programs and transform them into assertions that can then be verified by classic deductive verification. This paper presents a methodology of specification and verification of a wide range of high-level properties with METACSL and illustrates it on several examples. The goal is to provide verification practitioners with detailed methodological guidelines for common patterns of properties in order to facilitate their everyday work and to avoid some frequent pitfalls. The illustrating examples are inspired by very usual kinds of properties and illustrated on two use cases. One of them - on the real-life code of the bootloader module of the secure storage device Wookey - was fully verified using the described approach, demonstrating its capacity to scale to real-life code. The other one - on a microkernel of an OS - was added to illustrate other common properties, where the description of the system was intentionally left very generic.