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
Times are displayed in time zone: (GMT-06:00) Saskatchewan, Central America change

15:35 - 16:40: Research Papers - Verified & Secure Compilation at Ile de France III (IDF III)
Chair(s): Andrew AppelPrinceton
POPL-2020-Research-Papers15:35 - 15:56
Gilles BartheMPI for Security and Privacy (MPI-SP) and IMDEA Software Institute, Sandrine BlazyUniv Rennes- IRISA, Benjamin GregoireINRIA, Rémi HutinIRISA / ENS Rennes, Vincent LaporteInria, David PichardieUniv Rennes, ENS Rennes, IRISA, Alix TrieuAarhus University
Link to publication DOI Media Attached File Attached
POPL-2020-Research-Papers15:56 - 16:18
Youngju SongSeoul National University, Minki ChoSeoul National University, Dongjoo KimSeoul National University, Yonghyun KimSeoul National University, South Korea, Jeehoon KangKAIST, Chung-Kil HurSeoul National University
Link to publication DOI Media Attached File Attached
POPL-2020-Research-Papers16:18 - 16:40
Timothy BourkeInria / École normale supérieure, Lélio BrunENS/Inria, Marc PouzetÉcole normale supérieure
Link to publication DOI Media Attached File Attached