VERDICT Modeling Style Guide and User Manual V0 to support VERDICT VM19.0 PI Meeting
This Wiki provides a technical description of the Verification Evidence and Resilient Design in Anticipation of Cybersecurity Threats (VERDICT) project which is part of the DARPA Cyber Assured Systems Engineering (CASE) program. The VERDICT team is composed of researchers and engineers from General Electric Research (GRC) and General Electric Aviation Systems (GEAS), and the University of Iowa. The team is creating the VERDICT tool to generate a Attack-Defense tree with quantifiable likelihood of successful attack metrics, prove behavioral models meet formal cyber properties, identify the need for and place run time monitors, and generate cyber test cases. This Wiki is intended to help end users of the tool understand how to create models and run the tool.
The Overall DARPA CASE Toolchain is shown below is designed to enable System Engineers to analyze security along with other desired properties (e.g., safety, performance, cost, weight) at design time.
The program has seven Technical Areas (TA). TA 6 are the System Providers. They provide the systems to analyze including requirements, models, and code. TA 5 are the Systems Integrators. They facilitate integration of all the tools into a tool-chain. TA 4 is focused on Explainable Formal Methods. They are developing technology and tools that enables system engineers to benefit from formal methods technology without being formal methods experts. TA 3 supports Legacy Components such as binary and source code. TA 3 is working on tools that will extract models and properties from legacy code, so that it may be understood more clearly and reused. TA 2 is Design for Resiliency. The TA 2 performers are developing design tools to model, analyze and verify improvements in cyber-resiliency properties. The TA 1 performers are generating cyber-resiliency properties from the content provided to them by the TA 6 system providers.
The GE team is working on TA 2, Design for Resiliency. The GE VERDICT tool has two major functions. The first is the Model Based Architecture Synthesis (MBAS). The MBAS tool, takes in architecture models, mission and cyber-resiliency requirements, then generates attack-defense trees with resiliency metrics. The MBAS tool uses the attack-defense tree information along with cybersecurity requirements and constraints as inputs to a synthesis function that in Phase 2 of the program will generate an architecture that meets predefined resiliency design constraints. The MBAS tool is built as an extension to a Fault Tree modeling and synthesis tool named SOTERIA that was developed previously for NASA. The MBAS tool enables the system engineer to model components, then synthesize architectures that meet both safety (based on fault tree analysis) and security (based on attack-defense tree analysis) design goals.
The second major function in the GE TA 2 Design for Resiliency project is the Cyber-Resiliency Verifier (CRV). The CRV takes in cyber-resiliency properties/requirements, architecture, design and code models - performs a formal analysis using an improved version of the Kind2 model checker developed at the University of Iowa, then returns design proof evidence, localized design errors, suggested run time monitors, and test cases.
This section of the document introduces the critical content required in the AADL model in order to use the VERDICT MBAS analysis capability. See OpenAADL for general modeling in AADL guidelines. The VERDICT analysis engine requires: 1) Properties, 2) Mission Requirements, and 3) Cyber Relations to be defined in the AADL model.
VERDICT uses Properties associated with architectural components and connections to identify cyber vulnerabilities. Properties are defined by the system engineers in the AADL models. There are 3 Property types - 1) General Component and Connections, 2) Cyber Attack and 3) Cyber Defense. The following figure shows an example of properties declared in the VERDICT_Properties.aadl file.
All Properties MUST be declared in the VERDICT_Properties.aadl file before they are used. As shown in the figure below, VERDICT Properties are applied in the component implementation section of the AADL model.
The figure below shows VERDICT Properties being set on connections in the AADL model.
VERDICT generates Attack-Defense Trees and calculates Likelihood of Successful Attack based on Mission Requirements. The Mission Requirements represent the top of the Attack-Defense(AD) Tree. The AD Tree shows all the attacks and defenses that impact the ability to successfully achieve the Mission Requirement. VERDICT calculates the Likelihood of Successful Attack that would prevent the Mission Requirement.
As shown below, Mission Requirements are placed in the System declaration section of the AADL model. VERDICT created an AADL annex to capture Mission Requirements. The system engineer modeler includes a description of the Mission Requirement, the condition (connection impacted by CIA), and the severity. The figure below shows a Mission Requirement that impacts the Integrity of the system at a Hazardous level. The severity level is used by VERDICT as an acceptance criteria for the Likelihood of Successful Attack.
VERDICT requires the user to declare the Cyber Relations for each of the components in the AADL model. Cyber Relations represent the relationship of the input and output signals of a component. Cyber Relations are defined in the declaration section of the AADL model using the verdict annex. The figure below shows the the Cyber Relations for a Radio component. The comm_out integrity is impacted by the plan_in integrity, etc. VERDICT has a Wizard to automatically generate Cyber Relations and place them in the AADL model.
Connections at the outer edges of the AADL need to be "terminated". The following figure shows how to capture Cyber Relations for connections at the outer edges of an AADL model to support VERDICT analysis.
At the time of the 2019 PI Meeting VERDICT 19.0 Release, the VERDICT tool supported a subset of the AADL language which is shown in the following list.
- system
- in data port
- out data port
- No support for hierarchical models
The VERDICT team created the Delivery Drone model to demonstrate the tool functionality. The figure below shows an AADL model diagram of a delivery drone that may be used to deliver packages to residential locations.
The Delivery Drone Model is available to download in a VM
- Select the Model and call the MBAS function from the VERDICT menu
- Explore the Results
- Cyber Resiliency Metric (Likelihood of Successful Attack)
The Acceptable and Calculated Likelihood of Successful Attack (Failure Likelihood) are shown in the figures below.The acceptable metric is based on the Mission Requirement "severity" parameter defined in the AADL model. VERDICT calculates the Calculated number. When the calculated number is equal to or below the acceptable number the design passes and the tool shows a green check mark. When the calculated value is higher than the acceptable number, the tool shows a red "X". If the user right clicks on the red "X", the tool shows the specific CAPEC's and NIST 800-53 suggested defenses.
- Identified Cyber Threats (CAPEC's)
- Recommended Cyber Defense Patterns (NIST 800 - 53)
The following figure shows the Cyber Defense Properties commented out in the AADL model. This explains why the analysis failed.
The next figure shows the Cyber Defenses after they have been uncommented out.
The next figure shows the results passing now that the Cyber Defense Properties have been applied.
Cyber requirements and relations are written in verdict annexes within an AADL model. Requirements are placed only in the top-level system and relations only in subcomponents. Verdict annexes outside of components are not supported. The Eclipse extension automatically validates Verdict annexes. On top of validating the grammar (as described in the "Formal Grammar" section below), the validator checks that cyber requirements and relations are only placed in valid locations, that ids are non-empty and unique, and that all input/output ports are valid for the given system. The Verdict annex supports content assist, i.e. the Eclipse auto-completion feature activated by pressing Ctrl+Space. Invoking this command will supply a list of possible completions that can be selected for ease of input. The Verdict annex supplies completions for keywords (e.g. CyberRel, id, and Hazardous) and available ports. The Verdict annex also supports template insertion. When invoked at the root of an annex clause (i.e. outside of a CyberReq or CyberRel), content assist (Ctrl+Space) provides options for inserting CyberReq and CyberRel templates. Eclipse provides sensible default values for each field and allows tabbing through the fields with arrow keys used to select possible values. Using templates is the most efficient way to input cyber properties. Finally, the Verdict annex supports auto-formatting by pressing Ctrl+Shift+F, although be warned that OSATE does not appear to support formatting, so doing so on the entire file may cause OSATE to crash. Instead, select only the Verdict annex clause before invoking the formatter. Syntax and Semantics The most fundamental concept in VERDICT is a port security concern. For example, to say "output_a has an availability concern", we write output_a:A. The three available security concerns are Confidentiality (C), Integrity (I), and Availability (A), collectively known as CIA. Expressions are composed of ports as described above and the logical connectives and, or, and not, with parentheses used for grouping. Here is the same AADL example from above, but using the Verdict annex instead of AGREE:
-- this is a subsystem system MySubsystem features input_a: in data port MyDataType; output_b: out data port MyDataType;
annex verdict {**
-- Cyber relation: "output_b has an integrity concern if
-- input_a has an integrity concern or input_a has an
-- availability concern."
-- Option #1:
CyberRel {
id = "my_cyber_relation"
inputs = input_a:I or input_a:A
output = output_b:I
}
-- Option #2:
CyberRel "my_cyber_relation" =
input_a:I or input_a:A => output_b:I
**}
end MySubsystem;
-- this is the top-level system system MyTopLevelSystem features output_a: out data port MyDataType;
annex verdict {**
-- Cyber requirement: "There is a hazardous integrity concern
-- if output_a has an integrity concern or output_a has an
-- availability concern."
CyberReq {
id = "my_cyber_requirement"
condition = output_a:I or output_a:A
cia = I
severity = Hazardous
}
**}
end MyTopLevelSystem;
First, it was decided to rename "cyber formulas" as "cyber relations" (hence the CyberRel keyword) because we found the concept to be better-described as a relationship between inputs and outputs than as a "formula". A cyber requirement is declared with the keyword CyberReq and contains a list of fields inside curly brackets. Cyber relations are defined similarly with the CyberRel keyword. The ordering of the fields has no semantic value. Each field is written as the field keyword (e.g. id) followed by = and the value. CyberReq fields are: • id (in quotes), a unique identifier • condition, an expression describing the condition under which the cyber requirement is active • cia, the security concern (C, I, or A) • severity, the severity level (Catastrophic, Hazardous, Major, Minor, or None) • comment (optional, in quotes), an additional note with no semantic value CyberRel fields are: • id (in quotes), a unique identifier • output, a single port security concern that becomes active under the input condition • inputs (optional), an expression describing the condition under which the relation is active; if absent, signifies that the output condition is always active • comment (optional, in quotes), an additional note with no semantic value There is also a condensed syntax for cyber relations (option #2 in the AADL example) that is intended for ease of input and concision. The syntax is as follows: CyberRel "[id]" = [input condition] => [output port]
If there is no input condition, i.e. the output is always active, then the input condition may be omitted as follows: CyberRel "[id]" => [output port]
Note that there is no condensed syntax for cyber requirements.
Formal Grammar The following is a simplified and annotated version of the Xtext grammar. Note that there are many instances of redundancy for added flexibility beyond what is described above; for example, && may be used instead of and. Notation details: • The Kleene star (*) denotes zero or more of the preceding element • ? denotes zero or one of the preceding element • ! denotes any token other than the following element • & separates elements in an unordered group, i.e. each element must be included once and only once, except for those elements followed by ?, which may be included zero or one times • .. represents the range of values between A and Z
Verdict: Statement*
// Every statement is optionally followed by a semicolon Statement: (CyberReq | CyberRel) ';'?
CyberReq: 'CyberReq' CyberReqBlock
// Every field is optionally followed by a semicolon CyberReqBlock: '{' ( ( 'id' '=' STRING ';'? ) & ( 'cia' '=' CIA ';'? ) & ( 'severity' '=' Severity ';'? ) & ( 'condition' '=' LExpr ';'? ) & ( 'comment' '=' STRING ';'? )? ) '}'
// There are two ways to write a cyber relation CyberRel: 'CyberRel' (CyberRelBlock | CyberRelShort)
// Every field is optionally followed by a semicolon CyberRelBlock: '{' ( ( 'id' '=' STRING ';'? ) & ( 'output' '=' LPort ';'? ) & ( 'inputs' '=' LExpr ';'? )? & ( 'comment' '=' STRING ';'? )? ) '}'
// "=>" and "->" are semantically equivalent CyberRelShort: STRING ('=' LExpr)? ('=>' | '->') LPort
// Expression grammar is left-factored LExpr: LOr
// Parentheses, curly brackets, and square brackets are all // semantically equivalent (only in expressions) LExprTerm: | LPort | LNot | '(' LExpr ')' | '{' LExpr '}' | '[' LExpr ']'
LPort: ID ':' CIA
LOr: LAnd (OR LAnd)*
LAnd: LExprTerm (AND LExprTerm)*
LNot: NOT LExprTerm
// All semantically equivalent to "or" OR: | 'or' | '|' | '||' | '/'
// All semantically equivalent to "and" AND: | 'and' | '&' | '&&' | '/'
// Both semantically equivalent to "not" NOT: | 'not' | '!'
// "Confidentiality" is semantically equivalent to "C", etc. CIA: | 'C' | 'I' | 'A' | 'Confidentiality' | 'Integrity' | 'Availability'
Severity: | 'None' | 'Minor' | 'Major' | 'Hazardous' | 'Catastrophic'
// Provided by AADL ID: ( 'a'..'z' | 'A'..'Z' ) ( '_'? ( 'a'..'z' | 'A'..'Z' | '0'..'9' ))*
// Provided by AADL STRING: | '"' ( STRING_ESC | !( '' | '"' ) )* '"' | "'" ( STRING_ESC | !( '' | "'" ) )* "'"
// Provided by AADL STRING_ESC: '' ( 'b'|'t'|'n'|'f'|'r'|'u'|'"'|"'"|'' )