Metacsl: specification and verification of high-level properties

Virgile Robles; Nikolai Kosmatov; Virgile Prevosto; Louis Rilling; Pascale Le Gall

doi:10.1007/978-3-030-17462-0_22

Metacsl: specification and verification of high-level properties

Virgile Robles
, Nikolai Kosmatov
, Virgile Prevosto
, Louis Rilling
, Pascale Le Gall

Université Paris-Saclay
DGA-MI

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

Résumé

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.

langue originale	Anglais
titre	Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings
rédacteurs en chef	Tomáš Vojnar, Lijun Zhang
Editeur	Springer Verlag
Pages	358-364
Nombre de pages	7
ISBN (imprimé)	9783030174613
Les DOIs	https://doi.org/10.1007/978-3-030-17462-0_22
état	Publié - 1 janv. 2019
Modification externe	Oui
Evénement	25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019 - Prague, République tchcque Durée: 6 avr. 2019 → 11 avr. 2019

Série de publications

Nom	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	11427 LNCS
ISSN (imprimé)	0302-9743
ISSN (Electronique)	1611-3349

Une conférence

Une conférence	25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019
Pays/Territoire	République tchcque
La ville	Prague
période	6/04/19 → 11/04/19

Accès au document

10.1007/978-3-030-17462-0_22

Autres fichiers et liens

Lien vers la publication dans Scopus

Contient cette citation

Robles, V., Kosmatov, N., Prevosto, V., Rilling, L., & Le Gall, P. (2019). Metacsl: specification and verification of high-level properties. Dans T. Vojnar, & L. Zhang (eds.), Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings (p. 358-364). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol 11427 LNCS). Springer Verlag. https://doi.org/10.1007/978-3-030-17462-0_22

Robles, Virgile ; Kosmatov, Nikolai ; Prevosto, Virgile et al. / Metacsl : specification and verification of high-level properties. Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. Editeur / Tomáš Vojnar ; Lijun Zhang. Springer Verlag, 2019. p. 358-364 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{4a0bb61b33284a4e9016d3afc1e7b4bb,

title = "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 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.",

author = "Virgile Robles and Nikolai Kosmatov and Virgile Prevosto and Louis Rilling and \{Le Gall\}, Pascale",

note = "Publisher Copyright: {\textcopyright} The Author(s) 2019.; 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019 ; Conference date: 06-04-2019 Through 11-04-2019",

year = "2019",

month = jan,

day = "1",

doi = "10.1007/978-3-030-17462-0\_22",

language = "English",

isbn = "9783030174613",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "358--364",

editor = "Tom{\'a}{\v s} Vojnar and Lijun Zhang",

booktitle = "Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings",

}

Robles, V, Kosmatov, N, Prevosto, V, Rilling, L & Le Gall, P 2019, Metacsl: specification and verification of high-level properties. Dans T Vojnar & L Zhang (eds), Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), VOL. 11427 LNCS, Springer Verlag, p. 358-364, 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Prague, République tchcque, 6/04/19. https://doi.org/10.1007/978-3-030-17462-0_22

Metacsl: specification and verification of high-level properties. / Robles, Virgile; Kosmatov, Nikolai; Prevosto, Virgile et al.
Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. Ed. / Tomáš Vojnar; Lijun Zhang. Springer Verlag, 2019. p. 358-364 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol 11427 LNCS).

Résultats de recherche: Le chapitre dans un livre, un rapport, une anthologie ou une collection › Contribution à une conférence › Revue par des pairs

TY - GEN

T1 - Metacsl

T2 - 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems conference series, TACAS 2019 held as part of the 22nd European Joint Conferences on Theory and Practice of Software, ETAPS 2019

AU - Robles, Virgile

AU - Kosmatov, Nikolai

AU - Prevosto, Virgile

AU - Rilling, Louis

AU - Le Gall, Pascale

PY - 2019/1/1

Y1 - 2019/1/1

N2 - 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.

AB - 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.

UR - https://www.scopus.com/pages/publications/85064892373

U2 - 10.1007/978-3-030-17462-0_22

DO - 10.1007/978-3-030-17462-0_22

M3 - Conference contribution

AN - SCOPUS:85064892373

SN - 9783030174613

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 358

EP - 364

BT - Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings

A2 - Vojnar, Tomáš

A2 - Zhang, Lijun

PB - Springer Verlag

Y2 - 6 April 2019 through 11 April 2019

ER -

Robles V, Kosmatov N, Prevosto V, Rilling L, Le Gall P. Metacsl: specification and verification of high-level properties. Dans Vojnar T, Zhang L, rédacteurs en chef, Tools and Algorithms for the Construction and Analysis of Systems - 25th International Conference, TACAS 2019, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2019, Proceedings. Springer Verlag. 2019. p. 358-364. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/978-3-030-17462-0_22

Metacsl: specification and verification of high-level properties

Résumé

Série de publications

Une conférence

Accès au document

Autres fichiers et liens

Empreinte digitale

Contient cette citation