Verified Network Stack Synthesis for seL4

seL4 is a formally verified operating system microkernel, with proven separation and timing properties. It was developed by NICTA, now part of Data61, and can form the basis for highly secure systems for commercial and government use, including computer systems, control systems, machinery, vehicles and other cyber-physical systems, and Internet of Things devices. A major limitation preventing widespread use of seL4 is that it does not provide the typical POSIX interface that users expect of an operating system (files, processes, networking, etc.). Adding such features to seL4, and extending its assurance case to include them, would go a long way toward increasing its use in critical systems. Kestrel Technology will study the feasibility of building a verified, open-source implementation of TCP/IP networking on top of seL4, focusing on the network and transport layers. We will study the application of our APT tools for correct-by-construction (CxC) synthesis to create high assurance networking code with formal proofs of correctness and security. Our Phase I work will focus on scoping the effort, identifying risks, and determining feasibility. We will investigate the security properties needed to extend seL4's assurance case to systems built on top of it that use the network stack.