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

Mapping Threat Actor Behavior in the Ransomware Payment Ecosystem: A Mini-Pilot

Zoë Brammer

viewpdf

Reports

May 2023 Progress Report: Ransomware Task Force: Gaining Ground

Ransomware Task Force

viewpdf

Reports

Castles Built on Sand: Towards Securing the Open-Source Software Ecosystem

Zoë Brammer, Silas Cutler, Marc Rogers, Megan Stifel

viewpdf

Reports

Cyber Incident Reporting Framework: Global Edition

Cyber Threat Alliance, Institute for Security and Technology

viewpdf

Reports

AI-NC3 Integration in an Adversarial Context: Strategic Stability Risks and Confidence Building Measures

Alexa Wehsener, Andrew W. Reddie, Leah Walker, Philip Reiner

viewpdf

Op-ed

The Nuclear Risk Reduction Approach: A Useful Path Forward for Crisis Mitigation

Sylvia Mishra

view

Reports

Nuclear Crisis Communications: Mapping Risk Reduction Implementation Pathways

Sylvia Mishra

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

Formals 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