Official websites use .gov
A .gov website belongs to an official government organization in the United States.
Secure .gov websites use HTTPS
A lock (
) or https:// means you’ve safely connected to the .gov website. Share sensitive information only on official, secure websites.
Click here for the FMCP Workshop Presentations
NIST hosted the Workshop on Formal Methods within Certification Programs (FMCP 2024) on July 23-25, 2024, at the National Cybersecurity Center of Excellence in Rockville, Maryland.
The goal of the workshop was to explore the use of formal methods within certification programs for cryptographic modules such as FIPS 140-3.
Topics for discussion included:
- Software formal methods of different families: model checking, interactive proof, use of SMT and SAT solvers, static analysis
- How formal methods can fit within existing validation programs and potential impacts on stakeholders, e.g., pragmatics of allowing some current testing-based requirements to be fulfilled by submitting machine-checkable proofs or running certain automated tool
- Approaches to reduce the requirement for NIST and other standards authorities to trust vendors to validate their systems correctly, e.g., thanks to rechecking of formal proof
- Opportunities to build community understanding of formal methods through discussion in NIST reports, e.g., on how to think about the trust consequences of different combinations of formal tools
- Pragmatic paths to adoption that use less rigorous methods with shallower learning curves
- Overviews of current and upcoming NIST programs and tools (like the Automated Cryptographic Validation Testing System [ACVTS] and Automated Cryptographic Module Validation Protocol [AMVP]) that may both be of direct interest to formal-methods researchers and serve as examples of current modes of interaction with vendors
NIST also solicited research and discussion papers, surveys, presentations, case studies, panel proposals, and participation from all interested parties.
Submissions
- Formal Verification of Cryptographic Software at AWS - Current Practices and Future Trends
Rod Chapman, Adam Petcher, Torben Hansen, Yan Peng, Tancrède Lepoint, Cameron Bytheway, Panos Kampanakis
- Towards formal verification of the confidential computing framework for RISC-V
Wojciech Ozga, Lennard Gäher, Guerney D.H. Hunt, Avraham Shinnar, Elaine R. Palmer, Michael V. Le, Silvio Dragone
- AI-assisted Formal Method Verifications on Cryptographic Designs and Implementations
Long Ngo
- A Comparison-Based Methodology for the Security Assurance of Novel Systems
Jelizaveta Vakarjuk, Peeter Laud
- Cryptographic Validation Beyond Implementation Correctness
Manuel Barbosa, François Dupressoir, Andreas Hülsing, Vincent Laporte, Pierre-Yves Strub
- Formal Specifications for Certifiable Cryptography
Manuel Barbosa, Karthikeyan Bhargavan, Franziskus Kiefer, Peter Schwabe, Pierre-Yves Strub, Bas Westerbaan
- Which one to apply: formal methods or machine learning?
Yi Mao
- Modernizing FIPS for safe languages and verified libraries
Jonathan Protzenko, Bas Spitters
Important Dates
Submission deadline: May 27, 2024Notification deadline: June 10, 2024Registration deadline extended to: July 15, 2024Workshop: July 23-25, 2024
*Visitor Access Requirement:
For Non-US Citizens: Please have your valid passport for photo identification.
For US Permanent Residents: Please have your green card for photo identification.
For US Citizens: Please have your state-issued driver's license. Regarding Real-ID requirements, all states are in compliance or have an extension through May 2025.
NIST also accepts other forms of federally issued identification in lieu of a state-issued driver's license, such as a valid passport, passport card, DOD's Common Access Card (CAC), Veterans ID, Federal Agency HSPD-12 IDs, and Military Dependents ID.