Virtual Library

Our virtual library is an online repository of all of the reports, papers, and briefings that IST has produced, as well as works that have influenced our thinking.

Submit your Content

Reports

Enhancing Cyber Resilience through Insurance: Revisiting Anti-Bundling Regulation

Sophia Mauro and Taylor Grossman

viewpdf

Op-ed

ROOST Reminds Us Why Open Source Tools Matter

view

Reports

Navigating AI Compliance, Part 2: Risk Mitigation Strategies for Safeguarding Against Future Failures

Mariami Tkeshelashvili, Tiffany Saade

viewpdf

Reports

Deterring the Abuse of U.S. IaaS Products: Recommendations for a Consortium Approach

Steve Kelly, Tiffany Saade

viewpdf

Podcasts

TechnologIST Talks: Looking Back and Looking Ahead: Deep Dive on the New Cybersecurity Executive Order

Carole House, Megan Stifel, and Steve Kelly

view

Podcasts

TechnologIST Talks: The Offense-Defense Balance

Philip Reiner and Heather Adkins

view

Reports

The Generative Identity Initiative: Exploring Generative AI’s Impact on Cognition, Society, and the Future

Gabrielle Tran, Eric Davis

viewpdf

Contribute to our Library!

We also welcome additional suggestions from readers, and will consider adding further resources as so much of our work has come through crowd-sourced collaboration already. If, for any chance you are an author whose work is listed here and you do not wish it to be listed in our repository, please, let us know.

SUBMIT CONTENT

Formal Methods for NC3 Systems

Adam Wick

SUMMARY

What if we told you there is a very concrete way of updating and securing the most complex NC3 systems? Joining us is Adam Wick, Principal Scientist, Mobile Security & Systems Software for Galois, and one of the world’s leading experts on secure operating systems design and implementation. In this paper and call to action, Wick discusses how 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. We dive deep further into the substance of how formal proofs not only minimize language misunderstandings in a system as complex as NC3, they provide a rigorous executable specification on how a system such as CATALINK is supposed to run.

To dive deeper into this discussion, listen to our accompanying The Fourth Leg podcast with Adam Wick: Formally Verified.

download pdf