MetAcsl: Specification and Verification of High-Level Properties

Abstract : 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 on which high-level (e.g. security-related) properties of a whole software module are actually established, which makes it very difficult to express such properties. To address this issue, this paper proposes a new specification mechanism, called meta-properties, able to express a rich set of high-level properties. A meta-property can be seen as an enhanced global invariant specified for all or a subset 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 deductive verification tools in a usual way. This technique has been implemented as a Frama-C plugin called MetAcsl and successfully applied to specify and prove several safety-and security-related meta-properties in two illustrative case studies.
Type de document :
Communication dans un congrès
TACAS 2019, Apr 2019, Prague, Czech Republic
Liste complète des métadonnées

https://hal-cea.archives-ouvertes.fr/cea-02019790
Contributeur : Virgile Prevosto <>
Soumis le : jeudi 14 février 2019 - 17:27:44
Dernière modification le : dimanche 17 février 2019 - 01:13:34

Fichier

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : cea-02019790, version 1

Citation

Virgile Robles, Nikolai Kosmatov, Virgile Prévosto, Louis Rilling, Pascale Le Gall. MetAcsl: Specification and Verification of High-Level Properties. TACAS 2019, Apr 2019, Prague, Czech Republic. 〈cea-02019790〉

Partager

Métriques

Consultations de la notice

27

Téléchargements de fichiers

20