NIST only participates in the February and August reviews.
The Bugs Framework (BF) [1] is a classification of security bugs and related faults that features a formal language for the unambiguous specification of software and hardware security weaknesses and vulnerabilities. BF bug models, multidimensional weakness and failure taxonomies, and vulnerability models define the lexis, syntax, and semantics of the BF formal language and form the basis for the definition of secure coding principles. The BF formalism supports a deeper understanding of vulnerabilities as chains of weaknesses that adhere to strict causation, propagation, and composition rules. It enables the generation of comprehensively labeled weakness and vulnerability datasets and multidimensional vulnerability classifications. It also enables the development of new algorithms for code analysis and the use of AI models and formal methods to identify bugs and detect, analyze, prioritize, and resolve or mitigate vulnerabilities. The BF tools and APIs [2] support development of systems for the generation of weakness and vulnerability specifications, as well as for formal proofs of code correctness and existence of bugs/faults.
BF makes vulnerabilities machine-understandable and supports the development of BF-based systems that solve specific cybersecurity-related problems — bug identification and triaging, vulnerability detection, analysis, prioritization, reporting, and resolution or mitigation. BF-based systems could be traditional (rule-based) systems, or specialized ML/AI (model-based) or FM (formal methods) systems. The processes for the creation of BF datasets of BF definitions, taxonomies, secure coding principles/security rules, weakness specifications, vulnerability specifications, and vulnerability classifications are used to create the input data for a traditional BF-based system or the training and validating data for the process that transforms a generic AI model into a particular specialized AI system. The BF processes for the expression of the BF taxonomy and specifications create the output from the first two BF-based systems. A BF-based FM system, in turn, proves the correctness or existence of bugs/weaknesses and related vulnerabilities.
The scope of this NRC Research Project would be the creation of BF-Based Formal Methods (FM) Vulnerability Systems [2] that utilize FM-enabled capabilities to identify bugs and faults in software and hardware. 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.
The research would involve applying tools and techniques from mathematical logic and software science to these challenging problems in software security and safety. Program logics are a major component of software formal methods, and these involve grafting logic formalisms onto the syntax of a programming language to allow rigorous specifications and proofs about program behavior. The NRC Research Associate expected contributions would be in formalizing the BF security concepts definitions [1] and utilizing the BF security rules for proofs of software and hardware code correctness or existence of bugs/weaknesses and related vulnerabilities. The development of logical frameworks for reasoning about program misbehavior with respect to the NIST Bugs Framework (BF), MITRE Common Weakness Enumeration (CWE), and Common Vulnerabilities and Exposures (CVE) would also be part of this work.
A significant challenge in applying program logics and software formal methods to reasoning about CWE/CVE is that both enumerations are expressed in quite concrete terms that don't lend themselves to the levels of abstraction at which logic operates. We will leverage the Bugs Framework (BF) as a foundation for applying logic-based formal methods to hardware and software code security analysis. BF provides a necessary taxonomy and formal syntax and semantics (formal language) for precisely specifying software vulnerabilities, enabling rigorous reasoning about their underlying security weaknesses.
By integrating BF with logical techniques (e.g., O'Hearn's Incorrectness logic and tools such as the Coq theorem prover and automated property checkers like Z3), we will aim to develop methodologies for systematically identifying, specifying, and verifying weaknesses and vulnerabilities in software systems. Specifically, the NRC Research Associate will explore how logical formalisms-such as temporal logic, hybrid logic, and refinement types-can be used to express and check security invariants derived from BF security rules by BF classification. This research will help bridge the gap between high-level vulnerability classifications and formal verification, enabling developers to reason about hardware and software vulnerability and weakness properties in a structured, mathematically rigorous way.
The project tasks are as follows:
1. Investigate program logics for the BF formal language syntax and semantics.
2. Reframe BF Weakness to Vulnerability specifications in terms of these logics. Since BF organizes weaknesses by execution phase, investigate how formal logic techniques can track the causal flow of vulnerabilities from root causes to observable failures.
3. Express BF security rules (derived from the BF secure coding principles and based on the BF taxonomies and models) as inference rules in vulnerability/weakness program logics.
4. Explore toolchain integration, embedding BF-based formal specifications and BF-based tools into existing formal methods tools (e.g., SMT solvers like Z3 and proof assistants like Coq), and other static analysis frameworks.
5. Prove the existence of bugs/weaknesses and vulnerabilities in hardware/software code.
6. Prove correctness of hardware/software code.
References
[1] Bojanova I (July 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
[2] 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.
bug classification; software/hardware weakness taxonomy; vulnerability specification; secure coding; formal methods; proof of code correctness; proof of existence of bugs/faults; Bugs Framework (BF); Common Weakness Enumeration (CWE); Common Vulnerabilities and Exposures (CVE)
level
Open to Postdoctoral applicants