Скачать или смотреть 2f: Alain Kägi: Proving correctness of network stack implementation

Alain Kägi, in collaboration with Aubrey Birdwell, Caitlyn Wilde, Jens Mache and Richard Weiss, Lewis & Clark College

We are investigating the question of whether the field of software verification has matured enough to allow a small group of researchers at two undergraduate institutions to prove correctness properties of network protocols implemented in operating system distributions, in general, and IoT devices, in particular. As a proof of concept, we are designing a networked temperature sensor, to monitor incubators, built on top of the seL4 microkernel and seL4® core platform. In this talk, we will share our early experience building and proving some properties about such a system. In particular, we will describe our efforts developing our own UDP networking stack, testing IPv6-based protocols, proving properties about reassembly of network fragments, and finding possible inconsistencies in specifications published by the Internet Engineering Task Force.