Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “security verification”

Search indexed NASA NTRS and DOE OSTI research on propulsion, heat transfer, battery materials and energy systems. Follow report and document links to the original sources.

Quote a phrase for an exact phrase match. Source license links do not imply unrestricted reuse.

At least 109 records · Page 6

NAS Grid Benchmarks

We provide a paper-and-pencil specification of a benchmark suite for computational grids. It is based on the NAS (NASA Advanced Supercomputing) Parallel Benchmarks (NPB) and is called the NAS Grid Benchmarks (NGB). NGB problems are presented as data flow graphs encapsulating an instance of a slightly modified NPB task in each graph node, which communicates with other nodes by sending/receiving initialization data. Like NPB, NGB specifies several different classes (problem sizes). In this report we describe classes S, W, and A, and provide verification values for each. The implementor has the freedom to choose any language, grid environment, security model, fault tolerance/error correction mechanism, etc., as long as the resulting implementation passes the verification test and reports the turnaround time of the benchmark.

VanderWijngaart, Rob↗

Survey of Existing Tools for Formal Verification

Formal methods have come into wide use because of their effectiveness in verifying "safety and security" requirements of digital systems; a set of requirements for which testing is mostly ineffective. Formal methods are routinely used in the design and verification of high-consequence digital systems in industry. This report outlines our work in assessing the capabilities of commercial and open source formal tools and the ways in which they can be leveraged in digital design workflows.

Armstrong, Robert C.↗

Secure environment establishment for FPGA-based safety-critical systems: quality management system context - 159

The paper discusses importance of secure development and operational environment establishment process, its particular stages, including security-oriented analysis and assessment of safety-critical instrumentation and control (I and C) systems. Two particular aspects are covered - security assessment and security assurance related to processes established by Quality Management System (QMS). One of the underlying ideas for the security assessment approach is in performance of gap analysis. Such analysis considers influence of all different factors within I and C system development process, and further application of Intrusion Modes and Effect Criticality Analysis (IMECA) technique. It makes the approach applicable to various safety-critical systems, considering underlying technologies (for example, Field-Programmable Gate Arrays (FPGA). Nowadays FPGA technology is often used in wide spectrum of hardware devices - from personal devices to complex I and C systems for Nuclear Power Plants (NPPs). The problem of cyber security assessment and assurance for FPGA technology in general and its application in safety-critical I and C systems in particular is not completely solved due to several reasons that cover regulations, QMS processes, implementation of development and verification activities, etc. The paper overviews existing regulations, which cover various aspects of NPP I and C systems development and operation, FPGA technology implementation, and secure development and operational environment establishment and assurance. The paper also emphasizes that complex approach should be used to identify and mitigate all specific vulnerabilities thorough the whole life cycle on the basis on Intrusion Modes, Effect and Criticality Analysis technique. The paper also proposes approach to the development of safety-critical I and C systems in the scope of cyber security assurance process at developer site. Secure development environment is described as a key factor during the development process and the paper also discusses establishment and maintenance of such environment as a part of company's Nuclear Quality Assurance's QMS. (authors)

22 GENERAL STUDIES OF NUCLEAR REACTORS↗

Authentication Protocol for ICS without Encryption

Industrial control systems (ICS) describes the different types of control systems and associated instrumentation, which includes the devices, systems, networks, and controls used to operate and/or automate industrial processes. Depending on the industry, each ICS functions differently and are built to electronically manage tasks efficiently. Historically, industrial plants have included networking, and changes have been made over time without consideration for security. Many ICS devices currently have inadequate security features. Adding encryption in ICS is undesirable because many of the new detection method involves deep packet inspection. Therefore, we propose to develop a method of providing authentication between devices without encrypting the data. This testbed design will allow rapid development and experimentation with Cyber Physical Systems. Modbus connects to a supervisory computer with a Remote Terminal Unit (RTU) in Supervisory Control and Data Acquisition (SCADA) systems. Our project seeks to enhance security in the ICS environment by adding device authentication to the lower levels of the plant floor. This approach was selected as it allows verification of the sender of data from level 1/level 0 devices up to supervisory systems. This addition is desirable as it adds enhanced verification to the integrity of system data without obscuring (via encryption) the data being transmitted across the network. This is important because many ICS systems are real time critical (decryption adds to latency) and many other good security options require deep packet inspection (which encryption completely defeats). To accomplish this, a proof of concept of adding an authentication scheme was designed and will be tested with a common ICS protocol. The setup includes a single serial cable connecting the serial ports on two devices, a Master and a Minion. Authentication will occur in the following methods: - Data layer involving Transport Layer Security/Secure Socket Layer (TLS/SSL); - TCP/IP route implementation; - Key exchange algorithm; - Raspberry Pi programming for authentication. A portion of the setup includes adding Raspberry Pi into the system as the device is handling the authentication for the network traffic. Modbus is the chosen ICS protocol. It is used to transmit signals from instrumentation and control devices back to a main controller or data gathering system. Typically, the device identity is assumed but not verified. For verifying device identity, we constructed a digital signature architecture with TLS. A novel adaptation of this is to use only the digital signature that is provided and not the encryption capability. This allows ICS traffic to flow unobscured while still providing verification for the integrity of the data. Verification of this process will involve adding additional I/O level network devices with spoofed IP addresses and detecting the authenticated versus unauthenticated traffic. Our TLS implementation will have encryption disabled but should still allow for digital signing of data. This will enable our system to distinguish between real end devices and spoofed end devices. This experiment is presently building the test setup. It is focusing on a small setting to identify authenticated and unauthenticated devices on the network. This should allow for scaling to a larger network size after the initial proof of concept. One concern with this scheme is a certificate deployment has a large scale key management. Network size will thus increase the key management task for security. In addition, we believe that further research should be done on exploring the use of this method to defeat man-in-the-middle attacks.

42 ENGINEERING↗

Feasibility of Realizing a Universal Identifier Based on Fiber Bragg Grating Technology

Over the past year we have collected data on different fiber Bragg gratings (FBG) with the end goal of understanding their suitability for use in a new type of unique identifier (UID) that could be used in both tags and seals for high-value, high-risk assets. The ideal UID will have a complex signature that allows items to be uniquely identified by that signature. Tamper indication must be an integral part of the tag/seal process with measurable changes to the device signature indicative of any attempt to tamper with the monitored item. Further, the signature must be so difficult to reproduce that even state-actors with significant resources at their disposal will be discouraged from attempting it. Finally, readout verification of the product must be simple and secure, while providing red-light/green-light results in real time. To evaluate how well an FBG-based UID could meet these goals, we collected data on a large number of FBG samples from different vendors. Measurements included the response of the devices to uniform tension, tension when wrapped on a mandrel, and the response to changes in temperature and humidity, as well as the effect of simple potting in expanding and nonexpanding potting materials. We tested FBG samples written into single-mode fibers that were coated with the two commonly used materials, polyimide and acrylate and gratings that were both uniform and those with an apodized response (i.e., the intensity of the grating was varied to minimize sidelobes). The result of the work to date did not find any significant issues with the design concept for a UID based on this technology. Specific findings include a baseline design comprising five FBGs with distinct spectral returns analyzed using a difference-correlation approach. To realize this device, careful attention must be given to the impact of environmental factors on the UID response, limiting the properties of the potting compounds and FBG coating materials that can be used.

71 CLASSICAL AND QUANTUM MECHANICS, GENERAL PHYSIC↗

Risk and Vulnerability Assessment Using Cybernomic Computational Models: Tailored for Industrial Control Systems

There are many influencing economic factors to weigh from the defender-practitioner stakeholder point-of-view that involve cost combined with development/deployment models. Some examples include the cost of countermeasures themselves, the cost of training and the cost of maintenance. Meanwhile, we must better anticipate the total cost from a compromise. The return on investment in countermeasures is essentially impact costs (i.e., the costs from violating availability, integrity and confidentiality / privacy requirements). The natural question arises about choosing the main risks that must be mitigated/controlled and monitored in deciding where to focus security investments. To answer this question, we have investigated the cost/benefits to the attacker/defender to better estimate risk exposure. In doing so, it s important to develop a sound basis for estimating the factors that derive risk exposure, such as likelihood that a threat will emerge and whether it will be thwarted. This impact assessment framework can provide key information for ranking cybersecurity threats and managing risk.

Algorithms↗

Formally Verified ZTA Requirements for OT/ICS Environments with Isabelle/HOL

The clean energy transformation includes the integration of distributed energy resources with the power grid, which has led to a substantial increase in the complexity of power grids infrastructure and the underlying operational technology environment. Power grids infrastructure represents an operational technology environment that has become a system of systems, integrating heterogeneous devices which are both software-and hardware-intensive; as a result, there are increasing demands to exploit advances in the commodity of software-hardware infrastructures to improve energy systems requirements such as cybersecurity and resilience. In such a setting, system requirements at different levels mix, which leads to vulnerabilities and undesirable outcomes. The use of formal methods to characterize and prove system requirements removes ambiguity, increases automation, and provides high levels of assurance and reliability. In this paper, we contribute a methodology and a framework for the system-level verification of zero trust architecture requirements in operational technology environments. We define a formal specification for the core functionalities of operational technology environments, the corresponding invariants, and security proofs. Of particular note is our modular approach for the formal verification of asynchronous interactions in operational technology environments. The formal specification and the proofs have been mechanized using the interactive theorem proving environment Isabelle/HOL.

formal methods↗

Formally Verified ZTA Requirements for OT/ICS Environments with Isabelle/HOL: Preprint

The clean energy transformation led to the integration of distributed energy resources on a top of the grid, and so a substantial increase in the complexity of power grids infrastructure and the underlying operational technology environment. Operational technology environments are becoming a system of systems, integrating heterogeneous devices which are software/hardware intensive, have ever increasing demands to exploit advances in commodity of software/hardware infrastructures, and this for good reasons - improving energy systems requirements such as cybersecurity and resilience. In such a setting, system requirements at different levels mix, thus undesirable outcomes will surely happen. The use of formal methods will remove ambiguity, increase automation and provide high levels of assurance and reliability. In this paper, we contribute a methodology and a framework for the system level verification of zero trust architecture requirements in operational technology environments. We define a formal specification for the core functionalities of operational technology environments, the corresponding invariants, and security proofs. Of particular note is our modular approach for the formal verification of asynchronous interactions in operational technology environments. The formal specification and the proofs have been mechanized using the interactive theorem proving environment Isabelle/HOL.

formal methods↗

Formal verification and validation of run-to-completion style state charts using Event-B

State chart notations with ‘run to completion’ semantics are popular with engineers for designing controllers that react to environment events with a sequence of state transitions but lack formal refinement and rigorous verification methods. State chart models are typically used to design complex control systems that respond to environmental triggers with a sequential process. The model is usually constructed at a concrete level and verified and validated using animation techniques relying on human judgement. Event-B, on the other hand, is based on refinement from an initial abstraction and is designed to make formal verification by automatic theorem provers feasible. Abstraction and formal verification provide greater assurance that critical (e.g. safety or security) properties are not violated by the control system. In this paper, we introduce a notion of refinement into a ‘run to completion’ state chart modelling notation and leverage Event-B’s tool support for theorem proving. We describe the difficulties in translating ‘run to completion’ semantics into Event-B refinements and suggest a solution. We illustrate our approach and show how models can be validated at different refinement levels using our scenario checker animation tools. We show how critical invariant properties can be verified by proof despite the reactive nature of the system and how behavioural aspects of the system can be verified by testing the expected reactions using a temporal logic, model checking approach. To verify liveness, we outline a proof that the run to completion is deadlock-free and converges to complete the run.

97 MATHEMATICS AND COMPUTING↗

NCSP – AWE Collaboration [Slides]

Several points of collaboration between NCSP and AWE are noted, including the CIDAAS IS589 installation plan, CIDAAS testing, nuclear verification and detector physics, nuclear material control and nuclear security, and hands on criticality safety training.

73 NUCLEAR PHYSICS AND RADIATION PHYSICS↗

ACTS T1-VSAT - The intelligent earth station

The functional design of the software for NASA's Advanced Communication Technology Satellite (ACTS) T1-VSAT (Very Small Aperture Terminal) is described. The design provides a flexible interface to allow customized control of a satellite network and to provide external processes with access to network capabilities without requiring modification to the network hardware or software. Some of the envisioned features are: automatic number location; dynamic reconfiguration of the number plan tables; security features of call priority, call preemption, and remote verification; automatic reconfiguration of least cost routing tables; circuit availability verification prior to call setup; audio and video conferencing; on demand broadband dial-up service; on demand dial-up broadband broadcast service; and ISDN. A brief review is also given of the ACTS satellite and network, the network management, and the ACTS T1-VSAT earth station.

Manning, John R.↗

Quantifying Operational Drivers of Multimodal Biometric Verification in Aerial Surveillance

Multimodal biometric verification is increasingly applied across operational contexts ranging from close-range security cameras and building-mounted surveillance to long-range ground sensors and unmanned aerial system (UAS) imagery. Variations in acquisition conditions—such as image resolution, viewing geometry, and motion artifacts—pose significant challenges for cross-domain algorithmic generalization. This study evaluates two independent multimodal biometric verification systems developed under the Intelligence Advanced Research Projects Activity (IARPA) Biometric Recognition and Identification at Altitude and Range (BRIAR) program, comparing performance on close-range and aerial datasets. Close-range video served as a baseline to quantify the decline in verification performance on aerial footage. The dataset included six UAS platforms, spanning small quadcopters at 10m altitude to medium-sized fixed-wing aircraft at 360m. Mixed-effects logistic regression identified image resolution (head and body pixel counts), head height, sensor characteristics, and algorithm selection as primary determinants of verification success, whereas demographic attributes and mission gait were not significant predictors. Activity type and collection site influenced performance in close-range data but had negligible impact on UAS imagery. These results clarify modality-specific strengths and limitations and highlight opportunities to enhance cross-domain biometric verification.

Peluso, Alina [ORNL] (ORCID:0000000328950406)↗

Maintaining Continuity of Knowledge of Spent Fuel Pools: Tool Survey

This report examines supplemental tools that can be used in addition to optical surveillance cameras to maintain CoK in low-to-no light conditions, and increase the efficiency and effectiveness of spent fuel CoK, including item counting and ID verification, in challenging conditions.

11 NUCLEAR FUEL CYCLE AND FUEL MATERIALS↗

Light hydrocarbon and noble gas migration as an analogue for potential CO 2 leakage: numerical simulations and field data from three hydrocarbon systems

Abstract Sites where anthropogenic CO 2 captured from industrial sources is stored in deep geological formations for climate change mitigation are required to show secure retention of the injected CO 2 . Monitoring, reporting, and verification (MRV) plans are needed to indicate that no CO 2 release has occurred. We explored the degree to which direct comparison between a surface anomaly and reservoir geochemistry using various geochemical parameters can be used for attribution. We used data collected on light hydrocarbons and noble gases throughout the sedimentary column at three CO 2 enhanced oil recovery (EOR) sites to understand the processes that may cause fluid evolution. Light hydrocarbon and noble gases were sampled from reservoirs, gas‐bearing intervals above reservoirs, and groundwater. Vertical profiles indicated that lighter components are relatively enriched during migration (i.e. chromatographic separation). Static and numerical models were designed to simulate episodic gas migration and geochemical alteration of these geochemical parameters from solubility and sorption. The effects of hydrocarbon solubility were minimal (Bernard ratio changes within 5.2%) although field data were within the range of expected alterations from sorption. Forward models of CO 2 migration and noble gas interactions showed that CO 2 stripping causes an enrichment of crustal noble gases. In areas where natural fluxes of CO 2 from depth are non‐existent, the occurrence of crustal noble gas signature may distinguish fugitive CO 2 from the reservoir from natural near‐surface sources, and could be considered to explain apparent fluid anomalies. © 2019 Society of Chemical Industry and John Wiley & Sons, Ltd.

Anderson, Jacob↗

Applicative architectures for fault-tolerant multiprocessors

This paper proposes functional programming frameworks for the design of highly reliable multiprocessor systems. In contrast to imperative programming environments, a functional environment offers elegant, relatively simple, and efficient solutions to concurrent error detection and recovery problems in multiprocessors. Specific fault tolerance mechanisms for upset exposure, fault containment, secure task assignment, and recovery are developed for a class of applicative multiprocessor architectures. Verification of abstract behavioral characteristics of applicative tasks is used for exposing faults during the execution of tasks. The fault containment mechanism is based on isolation of stack and heap segments of tasks. A protocol for secure task assignment is defined between system components. The architecture permits incremental, distributed, and asynchronous backups of system state. Finally, recovery is accomplished, even in the worst cases, by reexecution of a small number of tasks.

Sharma, Madhumitra↗

Applicative architectures for fault-tolerant multiprocessors

Functional programming frameworks for the design of highly reliable multiprocessor systems are proposed. In contrast to imperative programming environments, a functional environment offers elegant, relatively simple, and efficient solutions to concurrent error detection and recovery problems in multiprocessors. Specific fault tolerance mechanisms for upset exposure, fault containment, secure task assignment, and recovery are developed for a class of applicative multiprocessor architectures. Verification of abstract behavioral characteristics of applicative tasks is used for exposing faults during the execution of tasks. The fault containment mechanism is based on isolation of stack and heap segments of tasks. A protocol for secure task assignment is defined between system components. The architecture permits incremental, distributed, and asynchronous backups of system state. Finally, recovery is accomplished, even in the worst cases, by re-execution of a small number of tasks.

Sharma, Madhumitra↗

BWR modernization project: installation of a new digital feedwater control system - 295

A European BWR plant carried out a relevant and pioneering modernization project regarding the Feedwater and Feed Pump Turbine Control System, replacing the legacy analogic control with the new General Electric MarkVIe digital system. This digital instrumentation and control modernization, motivated by obsolescence, had a great impact on the main control room and on the plant operation. Tecnatom collaborated with the nuclear power plant in the project performing the following activities: early installation of the system in the full scope and classroom simulators, Human Factors Engineering (HFE) Verification and Validation (V and V), Simulation Assisted Engineering (SAE), design and implementation of cyber secure communication with the Plant Process Computer (PPC), operating procedures modification and plant operators training. Those activities contributed to the success of the project that was completed during the refueling outage as planned. Scheduling HFE verification before the design freeze allowed the plant to modify the Human Machine Interface (HMI) to comply with the standards and increase safety without overcharging the project. SAE resulted in the reduction of costs and time during the system commissioning through the detection of discrepancies and improvements in the control, covering different plant scenarios. All the activities carried out in the simulators before the implementation of the system in the plant contributed to validate it and to build confidence in the new control among the plant personnel. New digital system communication interfaces with the PPC saved cable laying works and allowed future expansions. (authors)

21 SPECIFIC NUCLEAR REACTORS AND ASSOCIATED PLANTS↗

Technical Analysis of SSP-21 Protocol

As part of the California Energy Systems for the Twenty-First Century (CES-21) program, in December 2016 San Diego Gas and Electric (SDG&E) contracted with Lawrence Livermore National Laboratory (LLNL) to perform an independent verification and validation (IV&V) of a white paper describing their Secure SCADA Protocol for the Twenty-First Century (SSP-21) in order to analyze the effectiveness and propriety of cryptographic protocol use within the SSP-21 specification. SSP-21 is designed to use cryptographic protocols to provide (optional) encryption, authentication, and nonrepudiation, among other capabilities. The cryptographic protocols to be used reflect current industry standards; future versions of SSP-21 will use other advanced technologies to provide a subset of security services.

29 ENERGY PLANNING, POLICY, AND ECONOMY↗