Engineering Papers⌕ Search

SEARCH · Engineering Papers

Results for “Software trust”

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.

26 records · Page 2
All sourcesNASA NTRSDOE OSTI
DOE OSTI2024

The Essence of Cryptol: A Denotational Cryptol Interpreter in Coq for Foundational Assurances for Quantum Resistant Cryptosystems

Systems of the utmost consequence need a means to establish authenticity of software and data. Cryptosystems implement authentication, but can be vulnerable to cryptographic and implementation attacks. With the threat of quantum cryptographic attacks, “post-quantum” cryptosystems (PQCs) must be henceforth used in these systems. However, the new cryptography needs new ways to, rigorously and machine-checkably, prove systems free of vulnerabilities. We propose a retargetable capability to rapidly instantiate proven correct postquantum cryptosystems through novel proof-carrying synthesis and proof-automation technique, extending those proven successful on existing systems. This capability is crucial to meeting the cryptographic requirements for future high-consequence systems. Since specifications for high consequence cryptography are presently captured in a domain specific language known as Cryptol. While this can enable convenient fully automated reasoning about Cryptol specificaitons and implementations via the Software Analysis Workbench (SAW), Cryptol has expressivity gaps, so that cryptosystems with probabilistic programming features like Falcon cannot be fully expressed in the language. Moreover, SAW’s automation fails for programs and specificaitons with inductive and recursive structure, as in the Sphincs+ PQC. Finally, Cryptol and SAW together represent some 200,000 lines of unverified Haskell, so that the any guarantees about high consequence cryptography are presently contingent on a large, unverified, yet trusted computing base. The first step of the larger project of agile, assured crpytography is therefore to provide a formal, mechanized semantics for Cryptol, so that the specifications expressed by cryptographers in Cryptol can be reasoned about and compiled into performant implementations with a foundational, machine checkable certificate of correctness. This report describes our work on this first step, culminating in the design of a certified denotational interpreter, in Coq, for core Cryptol.

97 MATHEMATICS AND COMPUTING↗
DOE OSTI2025

Homotopy Solver

This software implements parallel versions of an interior-point solver, based on the publicly available ipopt solver. Here we have full control over the linear solver and our algorithm is fully parallel thus enabling scalability to large-scale optimization problems. This package also has a parallel implementation of a homotopy solver developed under the scalable methods for contact LDRD project 23-ERD-017. This solver is an mfem-based implementation of algorithm described in ``A filter trust-region Newton continuation method for nonlinear complementarity problems''. Cosmin G. Petra, Nai-Yuan Chiang, Jingyi Wang, Tucker Hartland, and Michael Puso (submitted), LLNL-JRNL-869761.

Hartland, Tucker [Lawrence Livermore National Labo↗
DOE OSTI2024

Hardware Fuzzing with An Emulator

Bugs in digital logic have led to some significant security vulnerabilities. Hardware bugs are particularly troublesome since they cannot be easily patched. Additionally, if the bug is in the root of trust, all trust built upon it can be vulnerable. Traditional testing either require a deep knowledge of the system, creative attack vectors and lots of human interaction. This is not scalable as there are very few engineers that can wear the hat of a designer, a verification engineer, and a cybersecurity expert. Hardware fuzzing is a relatively new research area in dynamic hardware testing. It has proven to be an effective method for discovering bugs, unexpected behaviors, and security vulnerabilities in software. While hardware fuzzing is new to the hardware domain, it has a strong track record in software testing. Fuzzing is a testing technique that randomly mutates the input data to uncover bugs or vulnerabilities in the design. It is especially good at finding corner cases that test engineers can not envision. Another advantage over other dynamic testing techniques is that, if done well, deep knowledge of the design is not required. Additionally, fuzzing scales well. If the system is set up correctly, it can run unsupervised for weeks if necessary. In this work, we propose using hardware fuzzing to improve the input vector generation for an information flow tracking tool. To get reasonable throughput of test vectors, an emulator is targeted as the execution platform. Efficient emulator execution has some specific requirements.

42 ENGINEERING↗
DOE OSTI2024

Zapiary: Creating Visibility in IOT Networks

Zigbee and Z-Wave are the main networking protocols used by low-power Internet of Things (IOT) devices. These protocols use low frequencies. Mesh architecture, and unique address formats that make them not compatible with traditional network traffic tools like IX-Discovery Tools. Zapiary is a software that takes CSV files with Zigbee and Z-Wave traffic and generates Structured Threat Information eXpression (STIX) JSON bundles illustrating the communication within IOT networks. The bundles can then be viewed within Structured Threat Intelligence Graph (STIG) or used with AI/ML models to provide deeper visibility into nodes that make up the network and the ability to trend the mesh network over time.

24 POWER TRANSMISSION AND DISTRIBUTION↗
DOE OSTI2025

Visualizing and analyzing 3D biomolecular structures using Mol* at RCSB.org: Influenza A H5N1 virus proteome case study

The easiest and often most useful way to work with experimentally determined or computationally predicted structures of biomolecules is by viewing their three-dimensional (3D) shapes using a molecular visualization tool. Mol* was collaboratively developed by RCSB Protein Data Bank (RCSB PDB, RCSB.org) and Protein Data Bank in Europe (PDBe, PDBe.org) as an open-source, web-based, 3D visualization software suite for examination and analyses of biostructures. It is capable of displaying atomic coordinates and related experimental data of biomolecular structures together with a variety of annotations, facilitating basic and applied research, training, education, and information dissemination. Across RCSB.org, the RCSB PDB research-focused web portal, Mol* has been implemented to support single-mouse-click atomic-level visualization of biomolecules (e.g., proteins, nucleic acids, carbohydrates) with bound cofactors, small-molecule ligands, ions, water molecules, or other macromolecules. RCSB.org Mol* can seamlessly display 3D structures from various sources, allowing structure interrogation, superimposition, and comparison. Using influenza A H5N1 virus as a topical case study of an important pathogen, we exemplify how Mol* has been embedded within various RCSB.org tools—allowing users to view polymer sequence and structure-based annotations integrated from trusted bioinformatics data resources, assess patterns and trends in groups of structures, and view structures of any size and compositional complexity. In addition to being linked to every experimentally determined biostructure and Computed Structure Model made available at RCSB.org, Standalone Mol* is freely available for visualizing any atomic-level or multi-scale biostructure at rcsb.org/3d-view.

3D biostructure↗
DOE OSTI2026

ReMU: regional minimal updating for model-based derivative-free optimization

Derivative-free optimization (DFO) problems are optimization problems where derivative information is unavailable or extremely difficult to obtain. Model-based DFO solvers have been applied extensively in scientific computing. Powell's NEWUOA (2004) [Powell, The NEWUOA software for unconstrained optimization without derivatives, in Large-Scale Nonlinear Optimization, Nonconvex Optimization and its Applications Vol. 83, G. Di Pillo and M. Roma, eds., Springer, 2006, pp. 255–297] and Wild's POUNDerS (2014) [Wild, Solving derivative-free nonlinear least squares problems with POUNDERS, in Advances and Trends in Optimization with Engineering Applications, T. Terlaky, M.F. Anjos, and S. Ahmed, eds., SIAM, 2017, pp. 529–540] explore the numerical power of the minimal norm Hessian (MNH) model for DFO and contributed to the open discussion on building better models with fewer data to achieve faster numerical convergence. Another decade later, we propose the regional minimal updating (ReMU) models, and extend the previous models into a broader class, including the H 2 norm models [Xie and Yuan, Least H 2 norm updating of quadratic interpolation models for derivative-free trust-region algorithms, IMA J. Numer. Anal. 46 (2025), pp. 21–50]. This paper shows motivation behind ReMU models, computational details, theoretical and numerical results on particular extreme points and the barycentre of ReMU's weight coefficient region, and the associated KKT matrix error and distance. Novel metrics, such as the truncated Newton step error, are proposed to numerically understand the new models' properties. A new algorithmic strategy, based on iteratively adjusting the ReMU model type, is also proposed, and shows numerical advantages by combining and switching between the barycentric model and the classic least Frobenius norm model in an online fashion.

derivative-free trust-region methods↗
DOE OSTI2025

Improving Cyber Situational Understanding

Effective cybersecurity operations require the ability to analyze large amounts of information to assess security risks and formulate defensive strategies against adversaries. This has become more complex in recent years as the sprawl and interconnectivity of devices grows through implementation of virtualization, cloud computing, and Internet of Things (IoT). The amount of data and analysis required for effective cybersecurity command and control decisions far exceeds humans’ capacity to perform manually. We characterize the analysis problem as cyber situational understanding. The research presented to improve cyber situational understanding focuses on vulnerability analysis and threat intelligence. Regarding vulnerabilities, entities must analyze and plan work for between thousands and tens of thousands of software vulnerabilities annually. Entities heavily use network firewalls to limit vulnerability exposure. As a result, some of these vulnerabilities permit exposure to adversarial exploitation, whereas others are inaccessible and therefore present negligible risk of exploitation. Distinguishing between high and low risk software vulnerabilities requires a deep understanding of the vulnerability, network firewall protection, and characteristics of the targeted device. This problem is solved by extracting network service features from vulnerability data features using both machine-learning and natural language processing. Then, the network firewall topology is parsed to determine which vulnerabilities are reachable by adversaries. Ultimately, a state-based safety analysis ascertains which vulnerabilities are unsafe. A related vulnerability analysis problem occurs in cybersecurity operations when associating an entity’s hardware and software assets to public vulnerability databases. Assets often reveal hardware and software through installation artifacts and network service identification, and entities store these artifacts in inventory databases. However, software and hardware vendors apply a standard Common Platform Enumeration (CPE) naming convention when publicly reporting vulnerabilities. Associating these two datasets often requires many hours to days of manual inspection. The proposed solution automates the mapping approach of human analysts using fuzzy matching techniques, natural language processing, and, ultimately, machine learning to present a small set of recommendations for mapping the two datasets. The result significantly reduces human analysis time and reduces the occurrence of false positives in vulnerability notifications. Finally, cyber threat intelligence (CTI) requires associating cyber observable artifacts, such as IP addresses, URIs, and file hashes, with cyber threat tactics, techniques, and procedures. Unfortunately, most CTI data is compartmentalized across multiple organizations and cannot be shared due to the legal and reputational risk with cyber threat being associated with the entity. The approach to solving this problem inovlves using a distributed ledger with anonymous token spending and authentication. This allows a consortium of semi-trusted entities to share the workload of curating CTI for a threat sharing community’s cooperative benefit.

Huff, Philip↗
DOE OSTI2026

EVs-at-RISC: A Secure and Resilient Interoperable SCM Control System Architecture for Electric Vehicle’s-at-Scale (Final Technical Report)

The EVs-at-RISC project was a five-year research, development, and demonstration initiative to create foundational tools for utility-scale fleet aggregation and Smart Charge Management (SCM) of Electric Vehicles (EV), Electric Vehicle Charging Infrastructure (EVCI), and related Distributed Energy Resources (DER). Rather than seeking to develop and demonstrate highly perfected SCM algorithms and control strategies, this project instead focused on creating foundational software solutions that enable unprecedented digital interoperability across the communications technologies and vendor platforms used to manage EV , EVCI, and DER, as well as existing energy management infrastructure operated by utilities, grid operators, and aggregators. This project then extends these novel interoperability capabilities to develop and deploy powerful middleware abstractions across grid edge networks and EVCI/DER fleet aggregations incorporating modern software tools and best practices, such as CI/CD, to bring the immense capabilities of infrastructure-as-code and policy-as-code to modern grid edge network environments. This addresses the foremost systemic issues preventing realization of any net operational benefits from scaled deployment of behind-the-meter EV, EVCI, and DER assets in electric power grids and markets today. The results of this approach and project unlock massive potential for new SCM capabilities to be easily prototyped, evaluated, and deployed at-scale within the existing grid edge network infrastructure and EVCI/DER technology ecosystem. The EVs-at-RISC project achieves this by extending Open Field Message Bus (OpenFMB), a conceptual model for digital interoperability and distributed intelligence in traditional front-of-meter utility SCADA networks, validating our hypothesis that OpenFMB could be similarly used to solve systemic digital interoperability issues in behind-the-meter environments and unlock real-world utility-scale SCM capabilities without requiring any new proprietary vendor solutions or significant infrastructure reconfiguration.

24 POWER TRANSMISSION AND DISTRIBUTION↗