Model Building
The VERDICT tool is implemented as a plug-in to the OSATE (Open Source AADL Tool Environment). The current version of VERDICT is delivered with OSATE 2.7.0. This document provides an introduction to creating an AADL model for analysis with VERDICT. The VERDICT tool currently supports the following AADL language elements.
system/abstract/device/process/thread type
- feature: ports, provides/requires data access
bus type
system/abstract/device/process/thread implementation
-
subcomponents
-
connections
- unidirectional
port
-
in/out (not both in and out port)
-
data/event
property set
- property
- with default value
- Boolean/string/integer/enumerated type
property definition
- actual connection bindings for bus
To create a model for a system to be analyzed by VERDICT one must first create an AADL model in OSATE that captures the system's architecture. This model can be later enriched with VERDICT specific information.
Part of this information is added as VERDICT-specific AADL properties as described below. The rest, specifically, behavioral information, is entered as a formal specification in the AGREE language for each computational component of the system. More details on how to model a system's architecture in AADL and add behavioral specifications can be found in a tutorial available as Appendix A: AADL Modeling Tutorial.
After your AADL model is created, you may add properties to it that will be used by the VERDICT tool during the analysis. VERDICT tools analyze a model based on a set of annotations contained in the VERDICT_Properties.aadl or CASE_Consolidatd_Properties.aadl file. There are six types of VERDICT Properties: 1) Mandatory Properties, 2) Port Properties, 3) Connection Properties, 4) Component Properties, 5) Connection Cyber Defense Properties and 6) Component Cyber Defense Properties. In addition to these standard VERDICT Properties, Cyber Attack Properties have been added for integration with CASE TA1 tools. VERDICT Properties are set in the "implementation" section of the model. This section of the document provides more information on the various property types and how to use them.
Mandatory Properties are those that must be set for every system in order to enable VERDICT tools to perform analysis. If no value is set, insecure default values are set for these properties.
canReceiveConfigUpdate is a property used to determine whether the system is susceptible to attacks attempting to tamper with the configuration of a system. Apply this property if the configuration of software or hardware within the system can be updated outside of the original manufacturer's facility. The line below shows the property being set to a default value of True and it applies to the list of aadl elements inside the parentheses.
canReceiveConfigUpdate: aadlboolean => True applies to (abstract, bus, device, system, process, processor, thread);
canReceiveSWUpdate is a property used to determine whether the system is susceptible to attacks attempting to install malicious software updates. Apply this property if the software within the system can be updated outside of the original manufacturer's facility.
canReceiveSWUpdate: aadlboolean => True applies to (abstract, bus, device, system, process, processor, thread);
componentType is a property used to determine whether the system is subject to attacks targeting software, hardware, humans, or hybrid (software and hardware). For example, systems that represent software only will not be subject to CAPEC-440 Hardware Integrity Attack.
componentType: enumeration (Software, Hardware, Human, SwHwHybrid, SwHumanHybrid, HwHumanHybrid, Hybrid) => Hybrid applies to (abstract, bus, device, system, process, processor, thread);
If a system contains the property hasSensitiveInfo it will be considered for attacks resulting in loss of confidentiality.
hasSensitiveInfo: aadlboolean => True applies to (abstract, bus, device, system, process, processor, thread);
insideTrustedBoundary designates a system that will be analyzed for their potential to be attacked. Also, systems where insideTrustedBoundary=TRUE will not be considered the initial source of attacks.
insideTrustedBoundary: aadlboolean => False applies to (abstract, bus, device, system, process, processor, thread);
pedigree is a property used to infer the level of trust in a system. A "COTS" component will be untrusted and considered a potential source of attacks, whereas "Sourced" and "InternallyDeveloped" components will be trusted. Both of these can be explicitly overridden by the insideTrustedBoundary property.
pedigree: enumeration (InternallyDeveloped, COTS, Sourced) => COTS applies to (abstract, bus, device, system, process, processor, thread);
The only port property is probe, and it signifies to CRV that the port is not part of the original architecture, but it is included just for the convenience of CRV's reasoning. When a system is modeled hierarchically, a probe port allows CRV to peek inside a component's behavior without needing to expose the behavior completely at a higher level.
Connections Properties are those that apply to connections but are optional for performing analysis. If not applied, VERDICT tools will default to the conservative values as defined.
connectionType is used by MBAA to make decisions around the level of trust for connections. An example Untrusted connectionType would be GPS, where the satelite and ground systems may be excluded from the model, but this could also be used for logical models where the physical connection passes outside of the trust boundary. An example Trusted connectionType would be a connection passing between two local systems, where the physical communications medium is entirely contained within the trust boundary indicating that the connection itself can be trusted. connectionType enables CRV to decide whether a certain connection can be susceptible to network injection attack or the component to which this connection is incident upon is susceptible to Remote code injection or other software attacks(e.g., virus, trojan, worm). Trusted connections are assumed to be free of attacks whereas Untrusted connections can be susceptible to attacks depending on the values of the following additional properties (authenticated/encryptedTransmission).
Component Properties are those that apply to systems but are optional for performing analysis. If not applied, VERDICT tools will default to the conservative values as defined.
The category property lets CRV know whether a certain component is one of the pre-defined ones (e.g., GPS, IMU, LIDAR). If it is one of the pre-defined components, then CRV decides it to be susceptible to a pre-defined set of attacks (e.g., Location spoofing).
If adversariallyTestedForTrojanOrLogicBomb property of a component is assigned an integer greater than '0', it suggests CRV that even if the component's pedigree is sourced/COTS, it is not susceptible to hardware trojan or logic bomb type of attacks.
Each cyber defense represents one or more NIST 800-53r4 controls that has been applied to the system and the relative level of rigor that is used to develop the implementation of that control. If the system does not have the property or the value is '0', it is assumed that this defense has not been applied. More information on NIST 800-53 controls can be found at: https://csrc.nist.gov/publications/detail/sp/800-53/rev-4/final.
encryptedTransmission
• SC-8 Transmission Confidentiality and Integrity
SC-8 generally covers protection of the confidentiality of communications between two components, which can include encryption of the data payload, protection of the header or protocol fields, and confidentiality of data just prior to sending and just after receipt.
deviceAuthentication
• IA-3 Device Identification and Authentication
• IA-3 (1) Cryptographic Bidirectional Authentication
IA-3 specifies general verification of the identity of other connected systems, while enhancement IA-3 (1) establishes requirements for mutual verification of identity through cryptographic algorithms.
sessionAuthenticity
• SC-23 Session Authenticity
SC-23 specifies technical means to maintain the authenticity of communications after establishing initial identity. Mitigations focus on unique randomly generated session identifiers.
Each cyber defense represents one or more NIST 800-53r4 controls that has been applied to the system and the relative level of rigor that is used to develop the implementation of that control. If the system does not have the property or the value is '0', it is assumed that this defense has not been applied. More information on NIST 800-53 controls can be found at: https://csrc.nist.gov/publications/detail/sp/800-53/rev-4/final.
antiJamming
• SC-40 Wireless Link Protection
• SC-40 (1) Electromagnetic Interference SC-40 specifies general protections for wireless links by directing protection on signal parameters, while SC-40 (1) specifies more specific techniques, such as cryptographic frequency hopping to prevent the adversary from jamming communications.
auditMessageResponses
• SI-11 Error Handling
SI-11 ensures that error messages are designed to provide only the minimal information necessary for informed authorized users to take the appropriate corrective actions and exclude any additional information that would reveal more about the systems to potential attackers.
dosProtection
• SC-5 Denial of Service Protection
• SC-5 (2) Excess Capacity/Bandwidth/Redundancy
SC-5 specifies general denial of service protections, including packet filtering and increased capacities to withstand attacks. Enhancement SC-5 (2) describes more specific solutions to manage capacities, which include usage priorities, quotas, and partitioning.
encryptedStorage
• SC-28 Protection of Information at Rest
SC-28 specifies means to protect sensitive information stored within the system, which can include encryption of stored data or stored configuration files.
failSafe
• SI-17 Fail-Safe Procedures
SI-17 specifies the implementation of logic within the system to follow a known procedure during attacks that result in sustained communication interruptions. Fail-Safe procedures can include shutdown process, alerts, or predefined operational paths to follow. heterogeneity
• SC-29 Heterogeneity
SC-29 promotes the use of a diverse set of technologies to defend against common mode failures, which prevent the same attack from successfully defeating two systems intended to be independent.
inputValidation
• SI-10 Information Input Validation
• SI-10 (5) Restrict Inputs to Trusted Sources and Approved Formats
SI-10 specifies checking of the validity of incoming communications. Validity checks can be performed based on a whitelisted character set, packet length, numerical ranges, or a list of acceptable values, as well as many other factors. Enhancement SI-10 (5) focuses on enforcing only known trusted sources and valid message formats.
logging
• AU-12 Audit Generation
• AU-12 (1) System-Wide/Time-Correlated Audit Trails
• AU-12 (3) Changes by Authorized Individuals
• AU-9 Protection of Audit Information
• AU-9 (3) Cryptographic Protection
AU-12 with enhancements (1) and (3) focuses on the implementation of auditable records that are time-synced across the broader system to aid in forensic activities and available only to authorized users. AU-9 with enhancement (3) ensures audit records are protected from tampering or deletion via signed hash functions or asymmetric encryption.
memoryProtection
• SI-16 Memory Protection
SI-16 describes protections from unauthorized code execution, including non-executable regions of memory and address space layout randomization.
physicalAccessControl
• PE-3 Physical Access Control
PE-3 is an operational control that describes elements of a program to physically secure a facility or site that containing a sensitive system. This includes verifying an individual's identity and authorization, logging physical accesses, escorting visitors, taking inventory of devices, and installing/maintaining physical access devices (e.g. locks, key readers, etc.).
remoteAttestation
• IA-3 (4) Device Attestation
Enhancement IS-3 (4) describes means for one system to assure to another system the authenticity of its configuration and operating state. This is often paired with secure boot, secure update, and other run-time mechanisms to maintain trusted authenticity and identity between interdependent systems.
removeIdentifyingInformation
• SI-15 Information Output Filtering
SI-15 requires validation of the output of the system to ensure that appropriate outputs are being sent given the context of the request. Mitigations satisfying this control could be to block unnecessary data or alert on anomalous behavior.
resourceAvailability
• SC-6 Resource Availability
SC-6 describes protections preventing an attacker from consuming the resources of a system, including prioritization or quotas.
resourceIsolation
• SC-4 Information in Shared Resources
SC-4 provides general protection mechanisms to prevent sensitive information from being leaked through shared registers, memory, or hard disk space.
secureBoot
• SI-7 (1) Integrity Checks
• SI-7 (5) Automated Response to Integrity Violations
• SI-7 (6) Cryptographic Protection
• SI-7 (9) Verify Boot Process
• SI-7 (15) Code Authentication
SI-7 Enhancement (1) specifies integrity checks of software, firmware, and information on a system. Enhancement SI-7 (5) defines the response to detected violations of these checks. Enhancement SI-7 (6) specifies cryptographic algorithms should be used to perform these checks. Enhancement SI-7 (9) specifies the checks be performed on the boot process to ensures the system is operating correctly prior to execution. Enhancement SI-7 (15) specifies the checks be performed on all new software prior to installation and execution to ensure no malicious code is injected.
staticCodeAnalysis
• SA-11 (1) Static Code Analysis
Enhancement SA-11 (1) is an organizational control specifying the use of software tools to look for common source code patterns that can be exploited by known attacks.
strongCryptoAlgorithms
• SC-13 Cryptographic Protection
SC-13 is an enhancement to controls specifying the use of cryptographic algorithms. Application of this control ensures only approved algorithms are used and their implementation is sufficient to protect against known attacks.
supplyChainSecurity
• SA-12 Supply Chain Protection
SA-12 is an organizational control listing best practices for acquiring services, systems, components securely. These best practices include supplier reviews, operational security, component validation, and component identification and traceability.
systemAccessControl
• PE-3 Physical Access Control
• PE-3 (1) Information System Access Control
PE-3 is an operational control that describes elements of a program to physically secure a facility or site that containing a sensitive system. This includes verifying an individual's identity and authorization, logging physical accesses, escorting visitors, taking inventory of devices, and installing/maintaining physical access devices (e.g. locks, key readers, etc.). PE-3 corresponds to the ”physicalAccessControl” defense. Enhancement PE-3 (1) improves the protection PE-3 as applied by the "physicalAccessControl" defense by additionally restricting physical access to each critical system beyond those applied to a site or facility, such that only authentic and authorized individuals for that system can gain physical access.
tamperProtection
• SA-18 (1) [Tamper Resistance and Detection] Multiple Phases of SDLC Enhancement SA-18 (1) describes multiple technical countermeasures to prevent reverse engineering or tampering with a component. These countermeasures can include obfuscation, self-checking, and customization.
zeroize
• MP-6 (8) Remote Purging / Wiping of Information
Enhancement MP-6 (8) specifies the purging or wiping of sensitive information either from a remote command or following some logic within the device to prevent unauthorized individuals from extracting that information.
Mission, Cyber & Safety Requirements, Cyber & Safety Relations, and Error Events are written in the AADL model using the VERDICT annex. Cyber, Safety and Mission Requirements may only be declared in a VERDICT annex within the top-level system type. Cyber Requirements can be aggregated and associated to a particular Mission Requirement. Cyber & Safety Relations may only be declared within a subcomponent system type, and they describe the vulnerability and failure flow, respectively, between the inputs and outputs of an individual component within the system. Safety relations model how faults or (erroneous) events or inputs affect the Integrity (I) and Availability (A) of the outputs. Cyber relations model how cyber-attacks affect the Confidentiality (C), Integrity (I), Availability (A) of the outputs.
All of the VERDICT architectural calculations roll up to Mission Requirements. Multiple Cyber and Safety Requirements can be associated with a Mission Requirement. VERDICT performs an analysis to determine if Mission Requirements are satisfied based on the Cyber and Safety Requirements that have been associated with the mission. If all the Cyber and Safety requirements associated with a mission satisfy their threshold, then the architecture is acceptable to meet the defined missions. The following figure shows the template for defining Mission Requirements in the VERDICT annex.
The following figure shows the template for defining Cyber Relations in the VERDICT annex. Cyber Relations are used to map component vulnerability of inputs to outputs. For example, the figure below shows that the Availability of out1 is impacted by the the Availability of in1 or in2.
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.
The following figure shows the template for defining Cyber Requirements in the VERDICT annex. Cyber Requirements must only be declared at the top most system level of the AADL project. It's a good practice to enter a message of the form "The <Confidentiality,Integrity,Availability> of the subject variable shall be <None, Minor, Major, Hazardous or Catastrophic> in the "description" field. For example - The Integrity of the estimated position signal input to the Navigator shall be Hazardous.
The following list shows the Acceptable Likelihood of Successful Attack value for each of the severity levels:
• Catastrophic = 1e-9
• Hazardous = 1e-7
• Major = 1e-5
• Minor = 1e-3
• None = 0
The following figure shows the template for defining Error Events in the VERDICT annex. Error events are defined in the declaration section of the AADL model using the VERDICT annex.
The following figure shows the template for defining Safety Relations in the VERDICT annex. Safety Relations are defined in the declaration section of the AADL model using the VERDICT annex.
The following figure shows the template for defining Safety Requirements in the VERDICT annex. Safety Requirements must only be declared at the top most system level of the AADL project.
