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

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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.

Original language	English
Title of host publication	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
Editors	Tomáš Vojnar, Lijun Zhang
Publisher	Springer Verlag
Pages	358-364
Number of pages	7
ISBN (Print)	9783030174613
DOIs	https://doi.org/10.1007/978-3-030-17462-0_22
Publication status	Published - 1 Jan 2019
Externally published	Yes
Event	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, Czech Republic Duration: 6 Apr 2019 → 11 Apr 2019

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	11427 LNCS
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	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
Country/Territory	Czech Republic
City	Prague
Period	6/04/19 → 11/04/19

Access to Document

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

Cite this

Robles, V., Kosmatov, N., Prevosto, V., Rilling, L., & Le Gall, P. (2019). Metacsl: specification and verification of high-level properties. In 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 (pp. 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. editor / Tomáš Vojnar ; Lijun Zhang. Springer Verlag, 2019. pp. 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. in 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, pp. 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, Czech Republic, 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).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

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.

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. In Vojnar T, Zhang L, editors, 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

Abstract

Publication series

Conference

Access to Document

Fingerprint

Cite this