Abstract:
In a certified code system, a code producer wishes to convince a code
consumer that her program is safe to execute.  To that end, the
producer provides to the consumer a certificate --- a
machine-checkable proof --- of safety of her program in some formal
language.  The code consumer no longer has to trust the code producer,
instead, the consumer only needs to trust the implementer of the
certificate checker and the runtime facilities.  Typically, a
certified code system does not provide a way for the code producer to
manually allocate and deallocate memory.  Instead, a garbage collector
is provided as part of the trusted computing base, without proof.
Recently, formal proofs of correctness for the Cheney copying
collector have been tackled in separation and linear logic.  Expanding
on this work, I propose to reason about garbage collection in a
dependent, higher order, linear logic with few unusual connectives and
in the setting of a machine model that is closer to real machine code
and to produce machine-verifiable proofs of safety for garbage
collector implementations.  As a concrete example, I propose to prove
the safety of an implementation of reference counting garbage
collection.