Methodology for Specification and Verification of High-Level Properties 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 proposed meta, a plugin of the Frama-C verification platform, that allows the user to specify high-level properties 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 meta 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 frequent 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 kinds of properties, where the description of the system was intentionally left as generic as possible.
Tue 18 MayDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 15:00
|Methodology for Specification and Verification of High-Level Properties with MetAcsl|
Virgile Robles CEA List, Software Reliability and Security Lab, Nikolai Kosmatov CEA List, Virgile Prevosto CEA Tech List, Louis Rilling DGA Maîtrise de l'Information, Pascale Le Gall CentraleSupelecPre-print Media Attached
|How much Specification is Enough? Mutation Analysis for Software Contracts|
FormaliSE 2021Media Attached