Security-Hardening Software Libraries with Ada and SPARK -- A TCP Stack Use Case

Kyriakos Georgiou, Guillaume Cluzel, Paul Butcher +1

This white paper demonstrates how the assurance, reliability, and security of an existing professional-grade, open-source embedded TCP/IP stack implementation written in the C prog…