One of the basic requirements for enterprise platform security is device attestation: trustworthy evidence of a device’s identity and security properties. The industry standard Security Protocol and Data Model (SPDM) addresses this need, defining message formats and session behaviors that device suppliers can implement for attestation.
This paper explains how AdaCore partnered with NVIDIA to capture and implement a subset of the SPDM 1.1.0 specification, using AdaCore’s RecordFlux product in conjunction with the SPARK/Ada programming language and the SPARK Pro toolsuite. The project successfully demonstrated that these technologies can address the vulnerabilities that communication protocols and complex data formats can bring, and the SPDM library that the project produced will be integrated into the firmware of microcontrollers and microprocessors that NVIDIA designs
