BF–Based Formal Methods (FM) Systems
Irena Bojanova, Inventor/Creator, PI & Lead, NIST Bugs Framework (BF), 2014 – ~~~

  • FM can reinvent Secure Programming R&D — but only if we do it right.

A BF-Based Formal Methods (FM) Vulnerability System utilizes FM-enabled capabilities to identify bugs and detect, analyze, prioritize, and resolve or mitigate vulnerabilities (i.e., fix the bug or a fault of each vulnerability). Automated analysis via formal methods requires formal definitions of the weakness and vulnerability concepts. Given the formal specification of code and the BF definitions of weakness and vulnerability, formal methods could be applied to Prove Correctness or Prove the Existence of Bugs/ Weaknesses and related Vulnerabilities.

Figure 1. BF- and Secure Coding Principles-Based FM Vulnerability System.

The steps from the dashed rectangle are BF specific.

  • Utilize the BF Formal Language (via the BFFL APIs) and ready BF Vulnerability Specifications to define BF FM Vulnerability Model (see also Figure 14 and Figure 15).
  • Utilize the BF Security Rules (via the BF Security APIs) and BF Backward State Tree generation (via the BF Partial API) to express BF FM security invariants and inference rules (e.g., via Hoare Logic and O’Hearn logic).
  • Analyze potentially vulnerable code and descriptions (CWE, CVE, NVD, etc.) to extract formal model.
  • Prove correctness or prove the existence of bugs/weaknesses and related vulnerabilities/

BF PATENT PENDING
U.S. Patent Application No. PCT/US2025/038662 Bugs Framework (BF): A System for Formal Specification of Cybersecurity Weaknesses and Vulnerabilities, Definition of Secure Coding Principles, and Generation of Weakness and Vulnerability Datasets and Vulnerability Classifications. Inventor: Irena Bojanova, NIST.

BF CITATION:
Bojanova I (2024) Bugs Framework (BF): Formalizing Cybersecurity Weaknesses and Vulnerabilities. (National Institute of Standards and Technology, Gaithersburg, MD), NIST Special Publication (SP), NIST SP 800-231. https://doi.org/10.6028/NIST.SP.800-231