skip to main content
US FlagAn official website of the United States government
dot gov icon
Official websites use .gov
A .gov website belongs to an official government organization in the United States.
https lock icon
Secure .gov websites use HTTPS
A lock ( lock ) or https:// means you've safely connected to the .gov website. Share sensitive information only on official, secure websites.


Title: Static Evaluation of Noninterference Using Approximate Model Counting
Noninterference is a definition of security for secret values provided to a procedure, which informally is met when attacker-observable outputs are insensitive to the value of the secret inputs or, in other words, the secret inputs do not "interfere" with those outputs. This paper describes a static analysis method to measure interference in software. In this approach, interference is assessed using the extent to which different secret inputs are consistent with different attacker-controlled inputs and attacker-observable outputs, which can be measured using a technique called model counting. Leveraging this insight, we develop a flexible interference assessment technique for which the assessment accuracy quantifiably grows with the computational effort invested in the analysis. This paper demonstrates the effectiveness of this technique through application to several case studies, including leakage of: search-engine queries through auto-complete response sizes; secrets subjected to compression together with attacker-controlled inputs; and TCP sequence numbers from shared counters.  more » « less
Award ID(s):
1718084
PAR ID:
10119362
Author(s) / Creator(s):
; ; ;
Date Published:
Journal Name:
IEEE Symposium on Security and Privacy
Page Range / eLocation ID:
514 to 528
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. With the rapid growth in the number of IoT devices that have wireless communication capabilities, and sensitive information collection capabilities, it is becoming increasingly necessary to ensure that these devices communicate securely with only authorized devices. A major requirement of this secure communication is to ensure that both the devices share a secret, which can be used for secure pairing and encrypted communication. Manually imparting this secret to these devices becomes an unnecessary overhead, especially when the device interaction is transient. In this paper, we empirically investigate the possibility of using an out-of-band communication channel -- vibration, generated by a custom smart ring, to share a secret with a smart IoT device. This exchanged secret can be used to bootstrap a secure wireless channel over which the devices can communicate. We believe that in future IoT devices can use such a technique to seamlessly connect with authorized devices with minimal user interaction overhead. In this paper, we specifically investigate (a) the feasibility of using vibration generated by a custom wearable for communication, (b) the effect of various parameters on this communication channel, and (c) the possibility of information manipulation by an adversary or information leakage to an adversary. For this investigation, we conducted a controlled study as well as a user study with 12 participants. In the controlled study, we could successfully share messages through vibrations with a bit error rate of less than 2.5%. Additionally, through the user study we demonstrate that it is possible to share messages with various types of objects accurately, quickly and securely as compared to several existing techniques. Overall, we find that in the best case we can exchange 85.9% messages successfully with a smart device. 
    more » « less
  2. Camouflage is a strategy that animals utilize for concealment in their habitat, making themselves invisible to their predators and preys. In RF systems, steganography or stealth transmission is the camouflage of information – a technology of hiding and transmitting secret messages in public media. Steganography conceals the secret message in publicly available media such that the eavesdropper or attacker will not be able to tell if there is a secret message to look for. Marine hatchetfish have two effective camouflage skills to help them hide from their predators – silvering and counterillumination. Silvering in marine hatchetfish uses its microstructured skin on its sides to achieve destructive interference at colors that could indicate the presence of the fish, while they also emit light at their bottom part to match its color and intensity to its surrounding, making it invisible from below, referred to as counterillumination. In this work, we borrow the two underwater camouflage strategies from marine hatchetfish, mimic them with photonic phenomena, and apply the camouflage strategies for physical stealth transmission of a 200 MBaud/s 16QAM OFDM secret signal at 5 GHz over a 25-km of optical fiber. The proposed bio-inspired steganography strategies successfully hid the secret signal in plain sight in temporal, RF spectral, and optical spectral domains, by blending in using counterillumination and turning invisible using silvering techniques. The stealth signal can only be retrieved with the precise and correct parameter for constructive interference at the secret signal frequency to unmask the silvering. 
    more » « less
  3. null (Ed.)
    This paper presents a framework to refine identified artificial neural networks (ANN) based state-space linear parametervarying (LPV-SS) models with closed-loop data using online transfer learning. An LPV-SS model is assumed to be first identified offline using inputs/outputs data and a model predictive controller (MPC) designed based on this model. Using collected closed-loop batch data, the model is further refined using online transfer learning and thus the control performance is improved. Specifically, fine-tuning, a transfer learning technique, is employed to improve the model. Furthermore, the scenario where the offline identified model and the online controlled system are “similar but not identitical” is discussed. The proposed method is verified by testing on an experimentally validated high-fidelity reactivity controlled compression ignition (RCCI) engine model. The verification results show that the new online transfer learning technique combined with an adaptive MPC law improves the engine control performance to track requested engine loads and desired combustion phasing with minimum errors. 
    more » « less
  4. Logic locking has been proposed to safeguard intellectual property (IP) during chip fabrication. Logic locking techniques protect hardware IP by making a subset of combinational modules in a design dependent on a secret key that is withheld from untrusted parties. If an incorrect secret key is used, a set of deterministic errors is produced in locked modules, restricting unauthorized use. A common target for logic locking is neural accelerators, especially as machine-learning-as-a-service becomes more prevalent. In this work, we explore how logic locking can be used to compromise the security of a neural accelerator it protects. Specifically, we show how the deterministic errors caused by incorrect keys can be harnessed to produce neural-trojan-style backdoors. To do so, we first outline a motivational attack scenario where a carefully chosen incorrect key, which we call a trojan key, produces misclassifications for an attacker-specified input class in a locked accelerator. We then develop a theoretically-robust attack methodology to automatically identify trojan keys. To evaluate this attack, we launch it on several locked accelerators. In our largest benchmark accelerator, our attack identified a trojan key that caused a 74% decrease in classification accuracy for attacker-specified trigger inputs, while degrading accuracy by only 1.7% for other inputs on average. 
    more » « less
  5. null (Ed.)
    Abstract This paper presents a framework to refine identified artificial neural networks (ANN) based state-space linear parameter-varying (LPV-SS) models with closed-loop data using online transfer learning. An LPV-SS model is assumed to be first identified offline using inputs/outputs data and a model predictive controller (MPC) designed based on this model. Using collected closed-loop batch data, the model is further refined using online transfer learning and thus the control performance is improved. Specifically, fine-tuning, a transfer learning technique, is employed to improve the model. Furthermore, the scenario where the offline identified model and the online controlled system are “similar but not identitical” is discussed. The proposed method is verified by testing on an experimentally validated high-fidelity reactivity controlled compression ignition (RCCI) engine model. The verification results show that the new online transfer learning technique combined with an adaptive MPC law improves the engine control performance to track requested engine loads and desired combustion phasing with minimum errors. 
    more » « less