MetAcsl: Specification and Verification of High-Level Properties
| Autor: | Virgile Prevosto, Virgile Robles, Pascale Le Gall, Nikolai Kosmatov, Louis Rilling |
|---|---|
| Přispěvatelé: | Laboratoire Sûreté des Logiciels (LSL), Département Ingénierie Logiciels et Systèmes (DILS), Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA)), Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Direction de Recherche Technologique (CEA) (DRT (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay-Laboratoire d'Intégration des Systèmes et des Technologies (LIST (CEA)), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay, Délégation générale de l'armement (DGA), Ministère de la Défense, Mathématiques et Informatique pour la Complexité et les Systèmes (MICS), CentraleSupélec, European Project: 731453, Laboratoire d'Intégration des Systèmes et des Technologies (LIST), Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Commissariat à l'énergie atomique et aux énergies alternatives (CEA)-Université Paris-Saclay-Laboratoire d'Intégration des Systèmes et des Technologies (LIST) |
| Jazyk: | angličtina |
| Rok vydání: | 2018 |
| Předmět: |
FOS: Computer and information sciences
Computer Science - Cryptography and Security Computer science [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] 02 engineering and technology computer.software_genre Frama-C Computer Science - Software Engineering Formal specification 0202 electrical engineering electronic engineering information engineering Plug-in Invariant (mathematics) meta-properties formal specification 060201 languages & linguistics business.industry Programming language 06 humanities and the arts Modular design deductive verification Software Engineering (cs.SE) Software modules 0602 languages and literature 020201 artificial intelligence & image processing business Cryptography and Security (cs.CR) computer |
| Zdroj: | 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, Prague, Czech Republic, April 6–11, 2019, Proceedings, Part I Tools and Algorithms for the Construction and Analysis of Systems ISBN: 9783030174613 TACAS (1) Lecture Notes in Computer Science Lecture Notes in Computer Science-Tools and Algorithms for the Construction and Analysis of Systems TACAS 2019 TACAS 2019, Apr 2019, Prague, Czech Republic. ⟨10.1007/978-3-030-17462-0_22⟩ |
| ISSN: | 0302-9743 1611-3349 |
| DOI: | 10.1007/978-3-030-17462-0_22⟩ |
| Popis: | 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. 7 pages, slightly extended camera-ready version |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|