Helmholtz Center for Information Security
CISPA – Helmholtz-Zentrum für InformationssicherheitNot a member yet
3406 research outputs found
Sort by
From LTL to rLTL Monitoring: Improved Monitorability Through Robust Semantics
Get PDFRuntime monitoring is commonly used to detect the violation of desired properties in safety critical systems by observing run prefixes of the system. Bauer et al. introduced an influential framework for monitoring Linear Temporal Logic (LTL) properties, which is based on a three-valued semantics: the formula is already satisfied by the given prefix, it is already violated, or it is still undetermined, i.e., it can be satisfied and violated. However, a wide range of formulas are not monitorable under this approach, meaning that every prefix is undetermined. In particular, Bauer et al. report that 44% of the formulas they consider in their experiments fall into this category. Recently, robust semantics for LTL were introduced to capture degrees of violation of universal properties. Here, we define robust semantics for run prefixes and show its potential in monitoring: every formula considered by Bauer et al. is monitorable under our approach. Furthermore, we show that properties expressed with the robust semantics can be monitored by deterministic automata
SentiNet: Detecting Localized Universal Attack Against Deep Learning Systems
Get PDFSentiNet is a novel detection framework for localized universal attacks on neural networks. These attacks restrict adversarial noise to contiguous portions of an image and are reusable with different images—constraints that prove useful for generating physically-realizable attacks. Unlike most other works on adversarial detection, SentiNet does not require training a model or preknowledge of an attack prior to detection. Our approach is appealing due to the large number of possible mechanisms and attack-vectors that an attack-specific defense would have to consider. By leveraging the neural network’s susceptibility to attacks and by using techniques from model interpretability and object detection as detection mechanisms, SentiNet turns a weakness of a model into a strength. We demonstrate the effectiveness of SentiNet on three different attacks—i.e., data poisoning attacks, trojaned networks, and adversarial patches (including physically realizable attacks)—and show that our defense is able to achieve very competitive performance metrics for all three threats. Finally, we show that SentiNet is robust against strong adaptive adversaries, who build adversarial patches that specifically target the components of SentiNet’s architecture
Validation of Abstract Side-Channel Models for Computer Architectures
Get PDFObservational models make tractable the analysis of information flow properties by providing an abstraction of side channels. We introduce a methodology and a tool, Scam-V, to validate observational models for modern computer architectures. We combine symbolic execution, relational analysis, and different program generation techniques to
generate experiments and validate the models. An experiment consists of a randomly generated program together with two inputs that are observationally equivalent according to the model under the test. Validation is done by checking indistinguishability of the two inputs on real hardware
by executing the program and analyzing the side channel. We have evaluated our framework by validating models that abstract the data-cache side channel of a Raspberry Pi 3 board with a processor implementing the ARMv8-A architecture. Our results show that Scam-V can identify bugs in the implementation of the models and generate test programs
which invalidate the models due to hidden microarchitectural behavior
Modular Black-box Runtime Verification of Security Protocols
Get PDFVerification techniques have been applied to the design of secure protocols for decades. However, relatively few efforts have been made to ensure that verified designs are also implemented securely. Static code verification techniques offer one way to bridge the verification gap between design and implementation, but require substantial expertise and manual labor to realize in practice. In this short paper, we propose black-box runtime verification as an alternative approach to extend the security guarantees of protocol designs to their implementations. Instead of instrumenting the complete protocol implementation, our approach only requires instrumenting common cryptographic libraries and network interfaces with a runtime monitor that is automatically synthesized from the protocol specification. This lightweight technique allows the effort for instrumentation to be shared among different protocols and ensures security with presumably minimal performance overhead
Clone Detection in Secure Messaging: Improving Post-Compromise Security in Practice
Get PDFWe investigate whether modern messaging apps achieve the strong post-compromise security guarantees offered by their underlying protocols. In particular, we perform a black-box experiment in which a user becomes the victim of a clone attack; in this attack,the user’s full state (including identity keys) is compromised by an attacker who clones their device and then later attempts to impersonate them, using the app through its user interface.Our attack should be prevented by protocols that offer post-compromise security, and thus, by all apps that are based on Signal’s double-ratchet algorithm (for instance, the Signal app, WhatsApp,and Facebook Secret Conversations). Our experiments reveal that this is not the case: most deployed messaging apps fall far short of the security that their underlying mechanisms suggest. We conjecture that this security gap is a result of many apps trading security for usability, by tolerating certain forms of desynchronization. We show that the tolerance of desynchronization necessarily leads to loss of post-compromise security in the strict sense, but we also show that more security can be retained than is currently offered in practice. Concretely, we present a modified version of the double-ratchet algorithm that tolerates forms of desynchronization while still being able to detect cloning activity.Moreover, we formally analyze our algorithm using the Tamarin prover to show that it achieves the desired security properties
Complex Security Policy? A Longitudinal Analysis of Deployed Content Security Policies.
Get PDFThe Content Security Policy (CSP) mechanism was developed as a mitigation against script injection attacks in 2010. In this paper, we leverage the unique vantage point of the Internet Archive to conduct a historical and longitudinal analysis of how CSP deployment has evolved for a set of 10,000 highly ranked domains. In doing so, we document the long-term struggle site operators face when trying to roll out CSP for content restriction and highlight that even seemingly secure whitelists can be bypassed through expired or typo domains. Next to these new insights, we also shed light on the usage of CSP for other use cases, in particular, TLS enforcement and framing control. Here, we find that CSP can be easily deployed to fit those security scenarios, but both lack wide-spread adoption. Specifically, while the underspecified and thus inconsistently implemented X-Frame-Options header is increasingly used on the Web, CSP’s well-specified and secure alternative cannot keep up. To understand the reasons behind this, we run a notification campaign and subsequent survey, concluding that operators have often experienced the complexity of CSP (and given up), utterly unaware of the easy-to-deploy components of CSP. Hence, we find the complexity of secure, yet functional content restriction gives CSP a bad reputation, resulting in operators not leveraging its potential to secure a site against the non-original attack vectors
Assessing the Impact of Script Gadgets on CSP at Scale
Get PDFThe Web, as one of the core technologies of modern society, has profoundly changed the way we interact with people and data through social networks or full-fledged office Web applications. One of the worst attacks on the Web is Cross-Site Scripting (XSS), in which an attacker is able to inject their malicious JavaScript code into a Web application, giving this code full access to the victimized site. To mitigate the impact of markup injection flaws that cause XSS, support for the Content Security Policy (CSP) is nowadays shipped in all browsers. Deploying such a policy enables a Web developer to whitelist from where script code can be loaded, essentially constraining the capabilities of the attacker to only be able to execute injected code from said whitelist. As recently shown by Lekies et al., injecting script markup is not a necessary prerequisite for a successful attack in the presence of so-called script gadgets. These small snippets of benign JavaScript code transform non-script markup contained in a page into executable JavaScript, opening the door for bypasses of a deployed CSP. Especially in combination with CSP’s logic in handling redirected resources, script gadgets enable attackers to bypass an otherwise secure policy. In this paper, we therefore ask the question: is deploying CSP in a secure fashion even possible without a priori knowledge of all files hosted on even a partially trusted origin?To answer this question, we investigate the severity of the findings of Lekies et al., showing real-world Web sites on which, even in the presence of CSP and without code containing such gadgets being added by the developer, an attacker can sideload libraries with known script gadgets, as long as the hosting site is whitelisted in the CSP. In combination with the aforementioned redirect logic, this enables us to bypass 10% of otherwise secure CSPs in the wild. To further answer our main research question, we conduct a hypothetical what-if analysis. Doing so, we automatically generate sensible CSPs for all of the Top 10,000 sites and show that around one-third of all sites would still be susceptible to a bypass through script gadget sideloading due to heavy reliance on third parties which also host such libraries
Towards Post-Quantum Security for Signal's X3DH Handshake
Get PDFModern key exchange protocols are usually based on the Diffie–Hellman (DH) primitive. The beauty of this primitive, among other things, is its potential reusage of key shares: DH shares can be either used a single time or in multiple runs. Since DH-based protocols are insecure against quantum adversaries, alternative solutions have to be found when moving to the post-quantum setting. However, most post-quantum candidates, including schemes based on lattices and even supersingular isogeny DH, are not known to be secure under key reuse. In particular, this means that they cannot be necessarily deployed as an immediate DH substitute in protocols.
In this paper, we introduce the notion of a split key encapsulation mechanism (split KEM) to translate the desired key-reusability of a DH-based protocol to a KEM-based flow. We provide the relevant security notions of split KEMs and show how the formalism lends itself to lifting Signal’s X3DH handshake to the post-quantum KEM setting without additional message flows.
Although the proposed framework conceptually solves the raised issues, instantiating it securely from post-quantum assumptions proved to be non-trivial. We give passively secure instantiations from (R)LWE, yet overcoming the above-mentioned insecurities under key reuse in the presence of active adversaries remains an open problem. Approaching one- sided key reuse, we provide a split KEM instantiation that allows such reuse based on the KEM introduced by Kiltz (PKC 2007), which may serve as a post-quantum blueprint if the underlying hardness assumption (gap hashed Diffie–Hellman) holds for the commutative group action of CSIDH (Asiacrypt 2018).
The intention of this paper hence is to raise awareness of the challenges arising when moving to KEM-based key exchange protocols with key-reusability, and to propose split KEMs as a specific target for instantiation in future research
Updates-Leak: Data Set Inference and Reconstruction Attacks in Online Learning
Get PDFMachine learning (ML) has progressed rapidly during the past decade and the major factor that drives such development is the unprecedented large-scale data. As data generation is a continuous process, this leads to ML model owners updating their models frequently with newly-collected data in an online learning scenario. In consequence, if an ML model is queried with the same set of data samples at two different points in time, it will provide different results.
In this paper, we investigate whether the change in the output of a black-box ML model before and after being updated can leak information of the dataset used to perform the update, namely the updating set. This constitutes a new attack surface against black-box ML models and such information leakage may compromise the intellectual property and data privacy of the ML model owner. We propose four attacks following an encoder-decoder formulation, which allows inferring diverse information of the updating set. Our new attacks are facilitated by state-of-the-art deep learning techniques. In particular, we propose a hybrid generative model ({\UGAN}) that is based on generative adversarial networks (GANs) but includes a reconstructive loss that allows reconstructing accurate samples. Our experiments show that the proposed attacks achieve strong performance
≪ I Know Where You Parked Last Summer ≫ Automated Reverse Engineering and Privacy Analysis of Modern Cars
No full textNowadays, cars are equipped with hundreds of sensors and dozens of computers that process data. Unfortunately, due to the very secret nature of the automotive industry, there is no official nor objective source of information as to what data exactly their vehicles collect. Anecdotal evidence suggests that OEMs are collecting huge amounts of personal data about their drivers, which they suddenly reveal when requested in court.
In this paper, we present our tool AutoCAN for privacy and security analysis of cars that reveals what data cars collect by tapping into in-vehicle networks and extracting time series of data and automatically making sense of them by establishing relationships based on laws of physics. These algorithms work irrespective of make, model or used protocols. Our results show that car makers track the GPS position, the number of occupants, their weight, usage statistics of doors, lights, and AC. We also reveal that OEMs embed functions to remotely disable the car or get an alert when the driver is speeding