BF Formal Language
Irena Bojanova, Inventor/Creator, PI & Lead, NIST Bugs Framework (BF), 2014 – ~~~~
The BF formal language is generated by the BF left-to-right leftmost derivation one-symbol lookahead (LL(1)) attribute context-free grammar (ACFG) derived from the BF CFG. Since it is based on an LL(1) grammar, the BF formal language is guaranteed to be unambiguous, and the BF weakness and vulnerability specifications are guaranteed to be clear and precise.[^1] The BF lexis, syntax, and semantics are based on the BF structured causal taxonomies (e.g., see BF MUS), bugs models (e.g., see BF _MEM model), and vulnerability models (e.g., see BF Vulnerability State Model and BF Vulnerability Specification Model). Lexis refers to the vocabulary (i.e., words and symbols) used by a specification language. Syntax is about validating the grammatical structure (i.e., the form) of a specification. Semantics is about verifying the logical structure (i.e., the meaning) of a specification.
BF Syntax
The BF formal language syntax is about validating the grammatical structure of a BF specification. It adheres to the BF production rules (i.e., nonterminals) for constructing (producing) valid specifications of the language that correspond to the BF Vulnerability Specification Model structure and flow (see BF Vulnerability Specification Model), including the converging and chaining rules (see BF Vulnerability State Model) defined by the BF Vulnerability State Model.
The BF CFG syntax defines a vulnerability that possibly converges with other vulnerabilities, leading to one or more failures.
BF Semantics
The BF formal language semantics is about verifying the logical structure of a BF specification. It is defined by extending the BF LL(1) CFG to a BF LL(1) ACFG with static semantic rules that adhere to the BF Vulnerability Models causation and propagation rules (see BF Vulnerability State Model and BF Vulnerability Specification Model). The static semantic rules are expressed via a set of grammar attributes (i.e., properties to which values can be assigned), a set of semantic functions for computing the attribute values, and a possibly empty set of predicate functions for each production rule (e.g., Donald Knuth’s attribute grammars.
The following Listing presents the BF LL(1) ACFG syntax and semantic rules. If a nonterminal appears in more than one rule, it gets subscripted. The semantic rules prevent invalid within weaknesses relations and error $\curvearrowright$ fault by value between weaknesses propagation and check for valid flow by operation.
The BF LL(1) ACFG adds the Type synthesized attribute for the nonterminals Fault and Error to store the operand types (i.e., Name, Data, Type, Address, or Size) and FinalError to store the final error types (e.g., Injection, Memory Corruption/Disclosure, Access, and Type Compute). The predicates express propagation by error type and fault type.