  Lighthouse projects such as CompCert, seL4, IronFleet, and DeepSpec have
demonstrated that full verification of entire systems is feasible by
establishing a refinement relation between an abstract system specification and
an executable implementation. Existing approaches however impose severe
restrictions on either the abstract system specifications due to their limited
expressiveness or versatility, or on the executable code due to their reliance
on suboptimal code extraction or inexpressive program logics. We propose a
novel methodology that combines the compositional refinement of abstract,
event-based models of distributed systems with the verification of full-fledged
program code using expressive separation logics, which support features of
realistic programming languages like mutable heap data structures and
concurrency. The main technical contribution of our work is a formal framework
that soundly relates event-based system models to program specifications in
separation logics, such that successful verification establishes a refinement
relation between the model and the code. We formalized our framework, Igloo, in
Isabelle/HOL. Our framework enables the sound combination of tools for protocol
development with existing program verifiers. We report on three case studies, a
leader election protocol, a replication protocol, and a security protocol, for
which we refine formal requirements into program specifications (in
Isabelle/HOL) that we implement in Java and Python and prove correct using the
VeriFast and Nagini tools.
