Publications

Abstract not provided.

Abstract not provided.

Abstract not provided.

Abstract not provided.

Abstract not provided.

This note discusses aspects of fuzzy extraction: in particular, how the interplay between PUF entropy and the revelation of helper data affects the entropy of the underlying secret. We examine the theory behind a scheme by Dodis et alii to develop exact formulas for the entropy of the given seed, given that an adversary knows the helper data. We also give a simple lower bound on the security of the Dodis scheme that is achieved exactly in many instances. By way of several examples, we quantify the amount of entropy that can be lost due to interactions between imperfect PUF implementations and given error correction methods. We repeatedly show that understanding the details of the error correction scheme and the interaction with the PUF response is crucial to being able to estimate the entropy of the system.

DOE maintains an up-to-date documentation of the number of available full drawdowns of each of the caverns at the U.S. Strategic Petroleum Reserve (SPR). This information is important for assessing the SPR’s ability to deliver oil to domestic oil companies expeditiously if national or world events dictate a rapid sale and deployment of the oil reserves. Sandia was directed to develop and implement a process to continuously assess and report the evolution of drawdown capacity, the subject of this report. This report covers impacts on drawdown availability due to SPR operations during Calendar Year 2022. A cavern has an available drawdown if, after that drawdown, the long-term stability of the cavern, the cavern field, or the oil quality are not compromised. Thus, determining the number of available drawdowns requires the consideration of several factors regarding cavern and wellbore integrity and stability, including stress states caused by cavern geometry and operations, salt damage caused by dilatant and tensile stresses, the effect of enhanced creep on wellbore integrity, and the sympathetic stress effect of operations on neighboring caverns. Finite-element geomechanical models have been used to determine the stress states in the pillars following successive drawdowns. By computing the tensile and dilatant stresses in the salt, areas of potential structural instability can be identified that may represent red flags for additional drawdowns. These analyses have found that many caverns will maintain structural integrity even when grown via drawdowns to dimensions resulting in a pillar-to-diameter ratio of less than 1.0. The analyses have also confirmed that certain caverns should only be completely drawn down one time. As the SPR caverns are utilized and partial drawdowns are performed to remove oil from the caverns (e.g., for oil sales, purchases, or exchanges authorized by the Congress or the President), the changes to the cavern caused by these procedures must be tracked and accounted for so that an ongoing assessment of the cavern’s drawdown capacity may be continued. A methodology for assessing and tracking the available drawdowns for each cavern is reiterated. This report is the latest in a series of annual reports, and it includes the baseline available drawdowns for each cavern, and the most recent assessment of the evolution of drawdown expenditures. A total of 222 million barrels of oil were released in calendar-year 2022. A nearly-equal amount of raw water was injected, resulting in an estimated 34 million barrels of cavern leaching. Twenty caverns have now expended a full drawdown. Cavern BC 18 has expended all its baseline available drawdowns, and has no drawdowns remaining. Cavern BM 103 has expended one of its two baseline drawdowns, and is now a single-drawdown cavern. All other caverns with an expenditure went from at-least-5 to at-least-4 remaining drawdowns.

Abstract not provided.

Abstract not provided.

Abstract not provided.

Abstract not provided.

Abstract not provided.

Abstract not provided.

Abstract not provided.

Abstract not provided.

Abstract not provided.

Abstract not provided.

Abstract not provided.

Abstract not provided.

Abstract not provided.

The CompCert compiler represents a landmark effort in program verification as both a piece of verified software and as a compiler for verified C programs. A key shortcoming of CompCert however is that it does not support multithreaded programs. Prior work to add threads to CompCert has either required major rewrites of parts of the proof or only works for well synchronized programs. The problem is that CompCert’s backward simulation derives from a forward simulation via the determinism of the semantics of intermediate representation languages. This makes the proofs in CompCert easier but also makes them incompatible with standard models of multithreading which are non-deterministic. Here we propose an alternate formulation of CompCert’s proof structure that parameterizes the existing single threaded semantics with nondeterministic behavior generated at the multithreading level. While this is an old trick where program equivalence is concerned, performing it in the context of CompCert is quite subtle. Our approach allows for expressive concurrent semantics and does not require major proof rewrites but still results in a global backward simulation for multithreaded programs.

Abstract not provided.

Abstract not provided.

Abstract not provided.

In classical statistical thermodynamics, calculating the configuration integral is both vital and elusive. Analytic relations for configuration integrals are desirable for modeling purposes, but it is typically impossible to obtain them. Certain systems become analytically tractable after replacing steep potential energies with harmonic potentials or athermal rigid constraints, but these approximations are often inadequate, especially when modeling the stretching of molecules. It is therefore necessary to develop a systematic approach to improve upon the approximations provided by these reference systems. Here, a general asymptotic approach is introduced, where the configuration integral for the full system is obtained in terms of that of the reference system and several corrections. This asymptotic approach is first demonstrated using the simple example of a classical three-dimensional oscillator. Next, the approach is applied to modeling the stretching of single polymer chains and to modeling thermally assisted crack growth, where results are verified with respect to numerical calculations. Overall, this asymptotic approach is a valid and effective tool for statistical thermodynamics in general.