Authors
Chunxiao Lin
Andrew McCreight
Zhong Shao
Yiyun Chen
Yu Guo
Abstract
Type-directed certifying compilation and typed assembly language (TAL)
aim to minimize the trusted computing base of safe languages by
directly type-checking low-level machine code. However, the safety of
TAL still heavily relies on its safe interaction with the underlying
garbage collector. Based on a recent variant of foundational
proof-carrying code (FPCC), we introduce a general methodology for
combining foundational TAL with a certified garbage collector. We
demonstrate the practicality of this approach by linking a typical TAL
with a conservative garbage collector. This includes proving the
safety of the collector, the soundness of TAL, and the safe
interaction between TAL programs and the garbage collector. Our work
is fully mechanized in the Coq proof assistant and the certified
programs can be shipped immediately as FPCC packages.
Published