Write a Blog >>
Fri 24 Jan 2020 15:56 - 16:18 at Ile de France III (IDF III) - Verified & Secure Compilation Chair(s): Andrew Appel

Supporting multi-language linking such as linking C and handwritten assembly modules in the verified compiler CompCert requires a more compositional verification technique than that used in CompCert just supporting separate compilation. The two extensions, CompCertX and Compositional CompCert, supporting multi-language linking take different approaches. The former simplifies the problem by imposing restrictions that the source modules should have no mutual dependence and be verified against certain well-behaved specifications. On the other hand, the latter develops a new verification technique that directly solves the problem but at the expense of significantly increasing the verification cost.

In this paper, we develop a novel lightweight verification technique, called RUSC (Refinement Under Self-related Contexts), and demonstrate how RUSC can solve the problem without any restrictions but still with low verification overhead. For this, we develop CompCertM, a full extension of the latest version of CompCert supporting multi-language linking. Moreover, we demonstrate the power of RUSC as a program verification technique by modularly verifying interesting programs consisting of C and handwritten assembly against their mathematical specifications.

Fri 24 Jan

Displayed time zone: Saskatchewan, Central America change

15:35 - 16:40
Verified & Secure CompilationResearch Papers at Ile de France III (IDF III)
Chair(s): Andrew Appel Princeton
15:35
21m
Talk
Formal Verification of a Constant-Time Preserving C Compiler
Research Papers
Gilles Barthe MPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Sandrine Blazy Univ Rennes- IRISA, Benjamin Gregoire INRIA, Rémi Hutin IRISA / ENS Rennes, Vincent Laporte Inria, David Pichardie Univ Rennes, ENS Rennes, IRISA, Alix Trieu Aarhus University
Link to publication DOI Media Attached File Attached
15:56
21m
Talk
CompCertM: CompCert with C-Assembly Linking and Lightweight Modular Verification
Research Papers
Youngju Song Seoul National University, Minki Cho Seoul National University, Dongjoo Kim Seoul National University, Yonghyun Kim Seoul National University, South Korea, Jeehoon Kang KAIST, Chung-Kil Hur Seoul National University
Link to publication DOI Media Attached File Attached
16:18
21m
Talk
Mechanized Semantics and Verified Compilation for a Dataflow Synchronous Language with Reset
Research Papers
Timothy Bourke Inria / École normale supérieure, Lélio Brun ENS/Inria, Marc Pouzet École normale supérieure
Link to publication DOI Media Attached File Attached