What if we told you there is a very concrete way of updating and securing the most complex NC3 systems? Adam Wick makes the case for future NC3 protocol descriptions “to include not only a broad description of the protocol and its goals, but also an executable specification of the protocol. He continues, “Given the sensitivity of these systems, we believe that the use of proof is critical.”
Formal methods, a precise mathematical description of a system’s function, is a crucial component to the design and implementation of CATALINK — a radically simple and secure nuclear crisis communications hotline. He dives into the substance of how formal proofs not only minimize language misunderstandings in a system as complex as NC3, but also provide a rigorous executable specification on how a system such as CATALINK is supposed to run.
About the author: Adam Wick is the Principal Scientist, Mobile Security & Systems Software at Galois. For the last several years, Dr. Wick has led the mobile security and systems software program at Galois. In that capacity, he works all aspects of the project spectrum: from business development and project inception to final delivery to the client. Adam has specialized in systems software: device drivers, embedded control systems, and other core operating system components.
To dive deeper into this discussion, listen to our accompanying The Fourth Leg podcast with Adam Wick: Formally Verified.
