Table Recursion - Stacking Correspondence with Daniel P. Neshyba-Rowe

This is a monthly Haskell-related hangout for Haskellers, Functional Programmers, and nerds of all sorts!

This month we are excited to have Daniel P. Neshyba-Rowe present his thesis, Stacking Correspondence: Towards Formal Verification of a Network Stack, drawing on his work with Alain Kägi (description below).

Location is Kiln Portland in the Cactus Room. We should be visible from the front door, or text the phone number on the front door and we will let you in! There are also many food carts nearby for more dining options.

All are welcome!

Title:
Stacking Correspondence: Towards Formal Verification of a Network Stack

Abstract:
In 2009, the seL4 microkernel was released as the first industry-grade microkernel which was formally verified to be correct. In our work, we hypothesize that it is possible to leverage seL4 to create a fully-functional embedded system application running Internet Protocol version 6 (IPv6) that is verified at all software levels---something thought to be practically impossible prior to the release of seL4. In our previous work, we designed and built the C code for a networked fish tank thermometer as a proof-of-concept of nontrivial complexity. Much of the complexity lies in the network stack, which consists of a number of components. Here, we focus on the components of the network stack that constitute a particular layer (the UDP layer), continuing the verification process by formally defining specifications and refinement steps, and applying them to the UDP layer. More specifically, we define how we expect the UDP layer to work in an abstract specification, describing what behaviors are acceptable and which are not. Subsequently, we show that the design specification of our implementation conforms to these expectations.