Secure-by-Construction Automation of Low-level Deserialization and Serialization (SCALDS)

When connecting legacy and other non-standard systems, insecurities in the encoding and decoding processes of messages within and between systems presents an expanding cyber-attack surface for U.S. Air Force (USAF) operations. This project, SCALDS, will build on existing capabilities to support the process to automatically generating communication binaries that are efficient and correct (i.e. formally-verified), starting from human-friendly specifications for deserialization and serialization operations within system communications. This project will focus on top-to-bottom correctness, generating provably correct, high-performance low-level implementations.