Helmholtz Center for Information Security
CISPA – Helmholtz-Zentrum für InformationssicherheitNot a member yet
3406 research outputs found
Sort by
Optimal Clock Synchronization with Signatures
No full textCryptographic signatures can be used to increase the resilience of distributed systems against adversarial attacks, by increasing the number of faulty parties that can be tolerated. While this is well-studied for consensus, it has been underexplored in the context of fault-tolerant clock synchronization, even in fully connected systems. Here, the honest parties of an n-node system are required to compute output clocks of small skew (i.e., maximum phase offset) despite local clock rates varying between 1 and ϑ>1, end-to-end communication delays varying between d−u and d, and the interference from malicious parties. So far, it is only known that clock pulses of skew d can be generated with (trivially optimal) resilience of ⌈n/2⌉−1 (PODC `19), improving over the tight bound of ⌈n/3⌉−1 holding without signatures for \emph{any} skew bound (STOC `84, PODC `85). Since typically d≫u and ϑ−1≪1, this is far from the lower bound of u+(ϑ−1)d that applies even in the fault-free case (IPL `01).
We prove matching upper and lower bounds of Θ(u+(ϑ−1)d) on the skew for the resilience range from ⌈n/3⌉ to ⌈n/2⌉−1. The algorithm showing the upper bound is, under the assumption that the adversary cannot forge signatures, deterministic. The lower bound holds even if clocks are initially perfectly synchronized, message delays between honest nodes are known, ϑ is arbitrarily close to one, and the synchronization algorithm is randomized. This has crucial implications for network designers that seek to leverage signatures for providing more robust time. In contrast to the setting without signatures, they must ensure that an attacker cannot easily bypass the lower bound on the delay on links with a faulty endpoint
Security at the End of the Tunnel: The Anatomy of VPN Mental Models Among Experts and Non-Experts in a Corporate Context
Get PDFWith the worldwide COVID-19 pandemic in 2020 and 2021 necessitating working from home, corporate Virtual Private Networks (VPNs) have become an important item securing the continued operation of companies around the globe. However, due to their different use case, corporate VPNs and how users interact with them differ from public VPNs, which are now commonly used by end-users.
In this paper, we present a first explorative study of eleven experts' and seven non-experts' mental models in the context of corporate VPNs. We find a partial alignment of these models in the high-level technical understanding while diverging in important parameters of how, when, and why VPNs are being used. While, in general, experts have a deeper technical understanding of VPN technology, we also observe that even they sometimes hold false beliefs on security aspects of VPNs. In summary, we show that the mental models of corporate VPNs differ from those for related security technology, e.g., HTTPS.
Our findings allow us to draft recommendations for practitioners to encourage a secure use of VPN technology (through training interventions, better communication, and system design changes in terms of device management). Furthermore, we identify avenues for future research, e.g., into experts' knowledge and balancing privacy and security between system operators and users
Batch-OT with Optimal Rate
Get PDFWe show that it is possible to perform n independent copies of 1-out-of-2 oblivious transfer in two
messages, where the communication complexity of the receiver and sender (each) is n(1 + o(1)) for
sufficiently large n. Note that this matches the information-theoretic lower bound. Prior to this work,
this was only achievable by using the heavy machinery of rate-1 fully homomorphic encryption (Rate-1
FHE, Brakerski et al., TCC 2019).
To achieve rate-1 both on the receiver’s and sender’s end, we use the LPN assumption, with slightly
sub-constant noise rate 1/m� for any � > 0 together with either the DDH, QR or LWE assumptions.
In terms of efficiency, our protocols only rely on linear homomorphism, as opposed to the FHE-based
solution which inherently requires an expensive “bootstrapping” operation. We believe that in terms of
efficiency we compare favorably to existing batch-OT protocols, while achieving superior communication
complexity. We show similar results for Oblivious Linear Evaluation (OLE).
For our DDH-based solution we develop a new technique that may be of independent interest. We
show that it is possible to “emulate” the binary group Z2 (or any other small-order group) inside a
prime-order group Zp in a function-private manner. That is, Z2 operations are mapped to Zp operations
such that the outcome of the latter do not reveal additional information beyond the Z2 outcome. Our
encoding technique uses the discrete Gaussian distribution, which to our knowledge was not done before
in the context of DDH
ÆPIC Leak: Architecturally Leaking Uninitialized Data from the Microarchitecture
Get PDFCPU vulnerabilities undermine the security guarantees provided by software- and hardware-security improvements. While the discovery of transient-execution attacks increased the interest in CPU vulnerabilities on a microarchitectural level, architectural CPU vulnerabilities are still understudied.
In this paper, we systematically analyze existing CPU vulnerabilities showing that CPUs suffer from vulnerabilities whose root causes match with those in complex software. We show that transient-execution attacks and architectural vulnerabilities often arise from the same type of bug and identify the blank spots. Investigating the blank spots, we focus on architecturally improperly initialized data locations.
We discover ÆPIC Leak, the first architectural CPU bug that leaks stale data from the microarchitecture without using a side channel. ÆPIC Leak works on all recent SunnyCove-based Intel CPUs (i.e., Ice Lake and Alder Lake). It architecturally leaks stale data incorrectly returned by reading undefined APIC-register ranges. ÆPIC Leak samples data transferred between the L2 and last-level cache, including SGX enclave data, from the superqueue. We target data in use, e.g., register values and memory loads, as well as data at rest, e.g., SGX-enclave data pages. Our end-to-end attack extracts AES-NI, RSA, and even the Intel SGX attestation keys from enclaves within a few seconds. We discuss mitigations and conclude that the only short-term mitigations for ÆPIC Leak are to disable APIC MMIO or not rely on SGX
27 Years and 81 Million Opportunities Later: Investigating the Use of Email Encryption for an Entire University
No full textEmail is one of the main communication tools and has seen significant adoption in the past decades. However, emails are sent in plain text by default and allow attackers easy access. Users can protect their emails by end-to-end encrypting them using tools such as S/MIME or PGP. Although PGP had already been introduced in 1991, it is a commonly held belief that email encryption is a niche tool that has not seen widespread adoption to date.
Previous user studies identified ample usability issues with email encryption such as key management and user interface challenges, which likely contribute to the limited success of email encryption. However, so far ground truth based on longitudinal field data is missing in the literature.
Towards filling this gap, we measure the use of email encryption based on 27 years of data for 37,089 users at a large university. While attending to ethical and data privacy concerns, we were able to analyze the use of S/MIME and PGP in 81,612,595 emails.
We found that only 5.46% of all users ever used S/MIME or PGP. This led to 0.06% encrypted and 2.8% signed emails. Users were more likely to use S/MIME than PGP by a factor of six. We saw that using multiple email clients had a negative impact on signing as well as encrypting emails and that only 3.36% of all emails between S/MIME users who had previously exchanged certificates were encrypted on average.
Our results imply that the adoption of email encryption is indeed very low and that key management challenges negatively impact even users who have set up S/MIME or PGP previously
Synthesis of Strategies for Autonomous Surveillance on Adversarial Targets
No full textWe study the problem of synthesizing a controller for an agent with imperfect sensing and a quantitative surveillance objective, that is, an agent is required to maintain knowledge of the location of a moving, possibly adversarial target. We formulate the problem as a one-sided partial-information game with a winning condition expressed as a temporal logic specification. The specification encodes the quantitative surveillance requirement as well as any additional tasks. Solving a partial-information game typically involves transforming it into a perfect-information belief game using a belief-set construction. Such a transformation leads to a state-space explosion, rendering the belief game computationally intractable to solve for most realistic settings. We present a belief-set abstraction technique to transform the partial-information game to a provably sound abstract belief game that can be solved efficiently using off-the-shelf reactive synthesis tools. We introduce a counterexample-guided refinement approach to automatically achieve the abstraction precision sufficient to synthesize a strategy that is provably winning on the original partial-information game. We evaluate the proposed method on multiple case-studies, implemented on hardware as well as high-fidelity ROS/Gazebo simulations where the agent must respond in real-time to a human-controlled adversary
Model Stealing Attacks Against Inductive Graph Neural Networks
Get PDFMany real-world data come in the form of graphs. Graph neural networks (GNNs), a new family of machine learning (ML) models, have been proposed to fully leverage graph data to build powerful applications. In particular, the inductive GNNs, which can generalize to unseen data, become mainstream in this direction. Machine learning models have shown great potential in various tasks and have been deployed in many real-world scenarios. To train a good model, a large amount of data as well as computational resources are needed, leading to valuable intellectual property. Previous research has shown that ML models are prone to model stealing attacks, which aim to steal the functionality of the target models. However, most of them focus on the models trained with images and texts. On the other hand, little attention has been paid to models trained with graph data, i.e., GNNs. In this paper, we fill the gap by proposing the first model stealing attacks against inductive GNNs. We systematically define the threat model and propose six attacks based on the adversary’s background knowledge and the responses of the target models. Our evaluation on six benchmark datasets shows that the proposed model stealing attacks against GNNs achieve promising performance
Compositional synthesis of modular systems
No full textIn contrast to the breakthroughs in reactive synthesis of monolithic systems, distributed synthesis is not yet practical. Compositional approaches can be a key technique for scalable algorithms. Here, the challenge is to decompose a specification of the global system into local requirements on the individual processes. In this paper, we present and extend a sound and complete compositional synthesis algorithm that constructs for each process, in addition to the strategy, a certificate that captures the necessary interface between the processes. The certificates define an assume-guarantee contract that allows for formulating individual process requirements. By bounding the size of the certificates, we then bias the synthesis procedure towards solutions that are desirable in the sense that they have a small interface. We have implemented our approach and evaluated it on scalable benchmarks: It is much faster than standard methods for distributed synthesis as long as reasonably small certificates exist. Otherwise, the overhead of synthesizing additional certificates is small
Maliciously Circuit-Private FHE from Information-Theoretic Principles
Get PDFFully homomorphic encryption (FHE) allows arbitrary computations on encrypted data. The standard security requirement, IND-CPA security, ensures that the encrypted data remain private. However, it does not guarantee privacy for the computation performed on the encrypted data. Statistical circuit privacy offers a strong privacy guarantee for the computation process, namely that a homomorphically evaluated ciphertext does not leak any information on how the result of the computation was obtained. Malicious statistical circuit privacy requires this to hold even for maliciously generated keys and ciphertexts. Ostrovsky, Paskin and Paskin (CRYPTO 2014) constructed an FHE scheme achieving malicious statistical circuit privacy.
Their construction, however, makes non-black-box use of a specific underlying FHE scheme, resulting in a circuit-private scheme with inherently high overhead.
This work presents a conceptually different construction of maliciously circuit-private FHE from simple information-theoretical principles. Furthermore, our construction only makes black-box use of the underlying FHE scheme, opening the possibility of achieving practically efficient schemes. Finally, in contrast to the OPP scheme in our scheme, pre- and post-homomorphic ciphertexts are syntactically the same, enabling new applications in multi-hop settings
Prophecy Variables for Hyperproperty Verification
No full textTemporal logics for hyperproperties like HyperLTL use trace quantifiers to express properties that relate multiple system runs. In practice, the verification of such specifications is mostly limited to formulas without quantifier alternation, where verification can be reduced to checking a trace property over the self-composition of the system. Quantifier alternations like , can either be solved by complementation or with an interpretation as a two-person game between a -player, who incrementally constructs the trace , and an -player, who constructs in such a way that and together satisfy .
The game-based approach is significantly cheaper but incomplete, because the -player does not know the future moves of the -player. In this paper, we establish that the game-based approach can be made complete by adding (-regular) temporal prophecies. Our proof is constructive, yielding an effective algorithm for the generation of a complete set of prophecies. We have implemented this construction in a prototype model checker called HyPro