Skip to Main content Skip to Navigation
Conference papers

Modular Verification of Programs with Effects and Effect Handlers in Coq

Thomas Letan 1, 2 Yann Régis-Gianas 3, 4 Pierre Chifflier 1 Guillaume Hiet 2
2 CIDRE - Confidentialité, Intégrité, Disponibilité et Répartition
CentraleSupélec, Inria Rennes – Bretagne Atlantique , IRISA-D1 - SYSTÈMES LARGE ÉCHELLE
4 PI.R2 - Design, study and implementation of languages for proofs and programs
UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique, IRIF (UMR_8243) - Institut de Recherche en Informatique Fondamentale, Inria de Paris
Abstract : Modern computing systems have grown in complexity, and the attack surface has increased accordingly. Even though system components are generally carefully designed and even verified by different groups of people, the composition of these components is often regarded with less attention. This paves the way for " architectural attacks " , a class of security vulnerabilities where the attacker is able to threaten the security of the system even if each of its components continues to act as expected. In this article, we introduce FreeSpec, a formalism built upon the key idea that components can be modelled as programs with algebraic effects to be realized by other components. FreeSpec allows for the modular modelling of a complex system, by defining idealized components connected together, and the modular verification of the properties of their composition. In addition, we have implemented a framework for the Coq proof assistant based on FreeSpec.
Complete list of metadatas

Cited literature [26 references]  Display  Hide  Download

https://hal.inria.fr/hal-01799712
Contributor : Thomas Letan <>
Submitted on : Friday, May 25, 2018 - 9:50:01 AM
Last modification on : Wednesday, June 24, 2020 - 4:19:46 PM
Document(s) archivé(s) le : Sunday, August 26, 2018 - 12:54:53 PM

File

main.pdf
Files produced by the author(s)

Identifiers

Citation

Thomas Letan, Yann Régis-Gianas, Pierre Chifflier, Guillaume Hiet. Modular Verification of Programs with Effects and Effect Handlers in Coq. FM 2018 - 22nd International Symposium on Formal Methods, Jul 2018, Oxford, United Kingdom. pp.338-354, ⟨10.1007/978-3-319-95582-7_20⟩. ⟨hal-01799712⟩

Share

Metrics

Record views

1596

Files downloads

4807