Helmholtz Center for Information Security
CISPA – Helmholtz-Zentrum für InformationssicherheitNot a member yet
3406 research outputs found
Sort by
A Logic and an Interactive Prover for the Computational Post-Quantum Security of Protocols
Get PDFWe provide the first mechanized post-quantum sound security protocol proofs. We achieve this by developing PQ-BC, a computational first-order logic that is sound with respect to quantum attackers, and corresponding mechanization support in the form of the PQ-Squirrel prover. Our work builds on the classical BC logic [Bana,Comon,CCS14] and its mechanization in the Squirrel prover [BDJKM,S&P21]. Our development of PQ-BC requires making the BC logic sound for a single interactive quantum attacker. We implement the PQ-Squirrel prover by modifying Squirrel , relying on the soundness results of PQ-BC and enforcing a set of syntactic conditions; additionally, we provide new tactics for the logic that extend the tool’s scope. Using PQ-Squirrel , we perform several case studies, thereby giving the first mechanical proofs of their computational post- quantum security. These include two generic constructions of KEM based key exchange, two sub-protocols from IKEv1 and IKEv2, and a proposed post-quantum variant of Signal’s X3DH protocol. Additionally, we use PQ-Squirrel to prove that several classical Squirrel case-studies are already post-quantum sound. We provide the sources of PQ-Squirrel and all our models for reproducibility, as well as a long version of this paper with full details
Mental Models of the Internet and Its Online Risks: Children and Their Parent(s)
No full textToday, children have access to the Internet from an early age and are therefore considered digital natives. This paper investigates how children (aged five to eight) and their parents perceive and deal with the Internet and the privacy and security risks of being online. Therefore, we extended prior studies of Internet mental models of children. We used a two-fold study design by including drawing tasks in addition to a verbal interview. The drawings allowed us to uncover the tacit knowledge underlying children’s and parents’ mental models.
So far, research focused mainly on the threat models of “being online”, while our study has a more holistic view, investigating general perceptions of the Internet in-depth. In contrast to prior studies, which were mainly conducted outside of Europe with highly-educated participants, we recruited participants in Central Europe with a diverse educational background.
We found that children’s mental models start to take shape beyond physically tangible components between the age of seven to eight years. Hence, we argue that it is important to educate children about the Internet as well as security and privacy issues before that age. For younger children, we suggest using secure and privacy-preserving applications, as they are not yet able to grasp the bigger picture
B-Cos Networks: Alignment Is All We Need for Interpretability
No full textWe present a new direction for increasing the interpretability of deep neural networks (DNNs) by promoting weight-input alignment during training. For this, we propose to replace the linear transforms in DNNs by our B-cos transform. As we show, a sequence (network) of such transforms induces a single linear transform that faithfully summarises the full model computations. Moreover, the B-cos transform introduces alignment pressure on the weights during optimisation. As a result, those induced linear transforms become highly interpretable and align with task-relevant features. Importantly, the B-cos transform is designed to be compatible with existing architectures and we show that it can easily be integrated into common models such as VGGs, ResNets, InceptionNets, and DenseNets, whilst maintaining similar performance on ImageNet. The resulting explanations are of high visual quality and perform well under quantitative metrics for interpretability. Code available at github.com/moboehle/B-cos
A survey on the group of points arising from elliptic curves with a Weierstrass model over a ring
Get PDFWe survey the known group structures arising from elliptic curves defined by Weierstrass models over commutative rings with unity and satisfying a technical condition.
For every considered base ring, the groups that may arise depending on the curve coefficients are recalled.
When a complete classification is still out of reach, partial results about the group structure and relevant subgroups are provided.
Several examples of elliptic curves over the inspected rings are provided, and open questions regarding the structure of their points are highlighted
Convolutional and Residual Networks Provably Contain Lottery Tickets
Get PDFThe Lottery Ticket Hypothesis continues to have a profound practical impact on the quest for small scale deep neural networks that solve modern deep learning tasks at competitive performance. These lottery tickets are identified by pruning large randomly initialized neural networks with architectures that are as diverse as their applications. Yet, theoretical insights that attest their existence have been mostly focused on deep fully-connected feed forward networks with ReLU activation functions. We prove that also modern architectures consisting of convolutional and residual layers that can be equipped with almost arbitrary activation functions can contain lottery tickets with high probability
TyPro: Forward CFI for C-Style Indirect Function Calls Using Type Propagation
Get PDFMaliciously-overwritten function pointers in C programs often lead to arbitrary code execution. In principle, forward CFI schemes mitigate this problem by restricting indirect function calls to valid call targets only. However, existing forward CFI schemes either depend on specific hardware capabilities, or are too permissive (weakening security guarantees) or too strict (breaking compatibility).
We present TyPro, a Clang-based forward CFI scheme based on type propagation. TyPro uses static analysis to follow function pointer types through C programs, and can determine the possible target functions for indirect calls at compile time with high precision. TyPro does not underestimate possible targets and does not break real-world programs, including those relying on dynamically-loaded code. TyPro has no runtime overhead on average and does not depend on architecture or special hardware features
Automatic Detection of Speculative Execution Combinations
Get PDFModern processors employ different speculation mechanisms to
speculate over different kinds of instructions. Attackers can exploit these mechanisms simultaneously in order to trigger leaks
of speculatively-accessed data. Thus, sound reasoning about such
speculative leaks requires accounting for all potential speculation
mechanisms. Unfortunately, existing formal models only support
reasoning about fixed, hard-coded speculation mechanisms, with
no simple support to extend said reasoning to new mechanisms.
In this paper, we develop a framework for reasoning about composed speculative semantics that capture speculation due to different mechanisms and implement it as part of the Spectector
verification tool. We implement novel semantics for speculating
over store and return instructions and combine them with the semantics for speculating over branch instructions. Our framework
yields speculative semantics for speculating over any combination
of these instructions that are secure by construction, i.e., we obtain
these security guarantees for free. The implementation of our novel
semantics in Spectector let us verify programs that are vulnerable
to Spectre v1, Spectre v4, and Spectre v5 vulnerabilities as well
as new snippets that are only vulnerable to their compositions
Loki: Hardening Code Obfuscation Against Automated Attacks
Get PDFSoftware obfuscation is a crucial technology to protect intellectual property and manage digital rights within our society. Despite its huge practical importance, both commercial and academic state-of-the-art obfuscation methods are vulnerable to a plethora of automated deobfuscation attacks, such as symbolic execution, taint analysis, or program synthesis. While several enhanced obfuscation techniques were recently proposed to thwart taint analysis or symbolic execution, they either impose a prohibitive runtime overhead or can be removed in an automated way (e.g., via compiler optimizations). In general, these techniques suffer from focusing on a single attack vector, allowing an attacker to switch to other, more effective techniques, such as program synthesis.
In this work, we present Loki, an approach for software obfuscation that is resilient against all known automated deobfuscation attacks. To this end, we use and efficiently combine multiple techniques, including a generic approach to synthesize formally verified expressions of arbitrary complexity. Contrary to state-of-the-art approaches that rely on a few hardcoded generation rules, our expressions are more diverse and harder to pattern match against. Even the most recent state-of-the-art research on Mixed-Boolean Arithmetic (MBA) deobfuscation fails to simplify them. Moreover, Loki protects against previously unaccounted attack vectors such as program synthesis, for which it reduces the success rate to merely 19%. In a comprehensive evaluation, we show that our design incurs significantly less overhead while providing a much stronger protection level compared to existing works
Approximately Counting Answers to Conjunctive Queries with Disequalities and Negations
Get PDFWe study the complexity of approximating the number of answers to a small query \varphi in a large database D. We establish an exhaustive classification into tractable and intractable cases if \varphi is a conjunctive query possibly including disequalities and negations:
- If there is a constant bound on the arity of \varphi, and if the randomised Exponential Time Hypothesis (rETH) holds, then the problem has a fixed-parameter tractable approximation scheme (FPTRAS) if and only if the treewidth of \varphi is bounded.
- If the arity is unbounded and \varphi does not have negations, then the problem has an FPTRAS if and only if the adaptive width of \varphi (a width measure strictly more general than treewidth) is bounded; the lower bound relies on the rETH as well.
Additionally we show that our results cannot be strengthened to achieve a fully polynomial randomised approximation scheme (FPRAS): We observe that, unless NP =RP, there is no FPRAS even if the treewidth (and the adaptive width) is 1.
However, if there are neither disequalities nor negations, we prove the existence of an FPRAS for queries of bounded fractional hypertreewidth, strictly generalising the recently established FPRAS for conjunctive queries with bounded hypertreewidth due to Arenas, Croquevielle, Jayaram and Riveros (STOC 2021)
Finding MNEMON: Reviving Memories of Node Embeddings
Get PDFPrevious security research efforts orbiting around graphs have been exclusively focusing on either (de-)anonymizing the graphs or understanding the security and privacy issues of graph neural networks. Little attention has been paid to understand the privacy risks of integrating the output from graph embedding models (e.g., node embeddings) with complex downstream machine learning pipelines. In this paper, we fill this gap and propose a novel model-agnostic graph recovery attack that exploits the implicit graph structural information preserved in the embeddings of graph nodes. We show that an adversary can recover edges with decent accuracy by only gaining access to the node embedding matrix of the original graph without interactions with the node embedding models.
We demonstrate the effectiveness and applicability of our graph recovery attack through extensive experiments