1 - 3 September | Vancouver, Canada BC View More Details & Registration The schedule is subject to change, so please check back before the event for the most up-to-date information.
Please note that all session times are listed below in Pacific Daylight Time (PDT), UTC-7.
Sign up or log in to add sessions to your schedule and sync them to your phone or calendar.
In prior work, we have verified the correctness of a C implementation of UDPv6 using AutoCorres2, a tool to facilitate the verification of C programs in Isabelle/HOL. To achieve high performance, it is common practice for implementations of such network layers to make repeated small mutations to heap state, using typed pointers with overlapping address ranges. This approach to network implementations presents additional challenges for the verification efforts.
In this talk, we describe some of these challenges and present our solutions. First, rather than showing direct refinement to a high-level specification, we prove important invariants at the level of the C specification—a monadic representation of the C code generated by AutoCorres2. Second, we analyze pointer aliasing manually. Third, we generalize some of our lemmas both to simplify proofs of the UDPv6 implementation but also to use them towards proving properties about other layer implementations. Fourth, we refactor code where appropriate, while preserving performance, to simplify our proofs. Finally, we describe how we use these invariants to show refinement.
