MetAcsl: Specification and Verification of High-Level Properties
This addresses a bottleneck in modular deductive verification for software engineers and security analysts, though it is incremental as it builds on existing tools.
The paper tackles the problem of verifying high-level properties like security in software modules, which is difficult with traditional function contracts, by proposing meta-properties as a new specification mechanism and an automatic transformation technique to integrate them into existing verification tools, successfully applied in case studies.
Modular deductive verification is a powerful technique capable to show that each function in a program satisfies its contract. However, function contracts do not provide a global view of which high-level (e.g. security-related properties of a whole software module are actually established, making it very difficult to assess them. To address this issue, this paper proposes a new specification mechanism, called meta-properties. A meta-property can be seen as an enhanced global invariant specified for a set of functions, and capable to express predicates on values of variables, as well as memory related conditions (such as separation) and read or write access constraints. We also propose an automatic transformation technique translating meta-properties into usual contracts and assertions, that can be proved by traditional deductive verification tools. This technique has been implemented as a Frama-C plugin called MetAcsl and successfully applied to specify and prove safety- and security-related meta-properties in two illustrative case studies.