Biblio
The design of modern computer hardware heavily relies on third-party intellectual property (IP) cores, which may contain malicious hardware Trojans that could be exploited by an adversary to leak secret information or take control of the system. Existing hardware Trojan detection methods either require a golden reference design for comparison or extensive functional testing to identify suspicious signals. In this paper, we propose a new formal verification method to verify the security of hardware designs. The proposed solution formalizes fine grained gate level information flow model for proving security properties of hardware designs in the Coq theorem prover environment. Compare with existing register transfer level (RTL) information flow security models, our model only needs to translate a small number of logic primitives to their formal representations without the need of supporting the rich RTL HDL semantics or dealing with complex conditional branch or loop structures. As a result, a gate level information flow model can be created at much lower complexity while achieving significantly higher precision in modeling the security behavior of hardware designs. We use the AES-T1700 benchmark from Trust-HUB to demonstrate the effectiveness of our solution. Experimental results show that our method can detect and pinpoint the Trojan.
The security of image steganography is an important basis for evaluating steganography algorithms. Steganography has recently made great progress in the long-term confrontation with steganalysis. To improve the security of image steganography, steganography must have the ability to resist detection by steganalysis algorithms. Traditional embedding-based steganography embeds the secret information into the content of an image, which unavoidably leaves a trace of the modification that can be detected by increasingly advanced machine-learning-based steganalysis algorithms. The concept of steganography without embedding (SWE), which does not need to modify the data of the carrier image, appeared to overcome the detection of machine-learning-based steganalysis algorithms. In this paper, we propose a novel image SWE method based on deep convolutional generative adversarial networks. We map the secret information into a noise vector and use the trained generator neural network model to generate the carrier image based on the noise vector. No modification or embedding operations are required during the process of image generation, and the information contained in the image can be extracted successfully by another neural network, called the extractor, after training. The experimental results show that this method has the advantages of highly accurate information extraction and a strong ability to resist detection by state-of-the-art image steganalysis algorithms.
Secure information flow guarantees the secrecy and integrity of data, preventing an attacker from learning secret information (secrecy) or injecting untrusted information (integrity). Covert channels can be used to subvert these security guarantees, for example, timing and termination channels can, either intentionally or inadvertently, violate these guarantees by modifying the timing or termination behavior of a program based on secret or untrusted data. Attacks using these covert channels have been published and are known to work in practiceâ as techniques to prevent non-covert channels are becoming increasingly practical, covert channels are likely to become even more attractive for attackers to exploit. The goal of this paper is to understand the subtleties of timing and termination-sensitive noninterference, explore the space of possible strategies for enforcing noninterference guarantees, and formalize the exact guarantees that these strategies can enforce. As a result of this effort we create a novel strategy that provides stronger security guarantees than existing work, and we clarify claims in existing work about what guarantees can be made.