Publications

Abstract not provided.

Abstract not provided.

Abstract not provided.

Abstract not provided.

One of the greatest challenges facing designers of equipment to be used in a nuclear arms control treaty is how to convince the other party in the treaty to trust its results and functionality. Whether the host provides equipment meant to prove treaty obligations and the inspector needs to gain that trust (commonly referred to as authentication), or the inspector provides this equipment and the host needs to gain this trust (commonly considered to be included in certification), one party generally has higher confidence in the equipment at the start of a treaty regime and the other party needs to gain that confidence prior to use. While we focus on authentication in this document—that is, the inspector gaining confidence in host-provided equipment—our conclusions will likely apply to host certification of inspector-provided equipment.

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.

Abstract not provided.

The time-reversal beam-forming technique utilizes the multipath in a cluttered environment to focus beyond the Rayleigh limit. This method makes use of the reciprocity of wireless propagation channels. Time-reversal can also be used to null signals, either to reduce unintentional interference or to prevent eavesdropping. Previous analytical work has also shown the ability to focus a signal at a location while simultaneously nulling it at a different location. We now present experimental results showing time-reversal focus and nulling in a cluttered environment. © 2012 IEEE.

Formal methods describe a class of system analysis techniques that seek to prove specific properties about analyzed designs, or locate flaws compromising those properties. As an analysis capability,these techniques are the subject of increased interest from both internal and external customers of Sandia National Laboratories. Given this lab's other areas of expertise, Sandia is uniquely positioned to advance the state-of-the-art with respect to several research and application areas within formal methods. This research project was a one-year effort funded by Sandia's CyberSecurity S&T Investment Area in its Laboratory Directed Research & Development program to investigate the opportunities for formal methods to impact Sandia's present mission areas, more fully understand the needs of the research community in the area of formal methods and where Sandia can contribute, and clarify from those potential research paths those that would best advance the mission-area interests of Sandia. The accomplishments from this project reinforce the utility of formal methods in Sandia, particularly in areas relevant to Cyber Security, and set the stage for continued Sandia investments to ensure this capabilityis utilized and advanced within this laboratory to serve the national interest.

Time-reversal is a wave focusing technique that makes use of the reciprocity of wireless propagation channels. It works particularly well in a cluttered environment with associated multipath reflection. This technique uses the multipath in the environment to increase focusing ability. Time-reversal can also be used to null signals, either to reduce unintentional interference or to prevent eavesdropping. It does not require controlled geometric placement of the transmit antennas. Unlike existing techniques it can work without line-of-sight. We have explored the performance of time-reversal focusing in a variety of simulated environments. We have also developed new algorithms to simultaneously focus at a location while nulling at an eavesdropper location. We have experimentally verified these techniques in a realistic cluttered environment.

Abstract not provided.