Virtual Library

Our research repositories present a collection of open-source resources that showcase research and analysis that has directly influenced our initiatives. Non-IST publications are copyrighted by external authors not affiliated with IST.

Submit your Content

Reports

Combatting Ransomware: A Comprehensive Framework for Action: Key Recommendations from the Ransomware Task Force

viewpdf

Reports

Future Digital Threats to Democracy – Trends and Drivers

Vera Zakem, Alexa Wehsener, Nina M. Miller

viewpdf

Reports

Hotline Between Two Koreas: Status, Limitations and Future Tasks

Dr. Chung-in Moon and Boo Seung-Chan

viewpdfpodcast icon

Reports

Building Communications Norms Across Nuclear C2

Dr. Salma Shaheen

viewpdf

Reports

Nuclear Hotlines: Origins, Evolution, Applications

Steven E. Miller

viewpdfpodcast icon

Reports

Formals Methods for NC3 Systems

Adam Wick

viewpdfpodcast icon

Reports

Pay Attention

Alexa Wehsener

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
Playing now

Virtual Event and Live Q&A with Mr. Nand Mulchandani, Acting Director of the U.S. Department of Defense Joint Artificial Intelligence Center

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