Helmholtz Center for Information Security
CISPA – Helmholtz-Zentrum für InformationssicherheitNot a member yet
3406 research outputs found
Sort by
Multiparty Cardinality Testing for Threshold Private Intersection
No full textThreshold Private Set Intersection (PSI) allows multiple parties to compute the intersection of their input sets if and only if the intersection is larger than ????−????, where n is the size of each set and t is some threshold. The main appeal of this primitive is that, in contrast to standard PSI, known upper-bounds on the communication complexity only depend on the threshold t and not on the sizes of the input sets. Current threshold PSI protocols split themselves into two components: A Cardinality Testing phase, where parties decide if the intersection is larger than some threshold; and a PSI phase, where the intersection is computed. The main source of inefficiency of threshold PSI is the former part.
In this work, we present a new Cardinality Testing protocol that allows N parties to check if the intersection of their input sets is larger than ????−????. The protocol incurs in ????̃(????????2) communication complexity. We thus obtain a Threshold PSI scheme for N parties with communication complexity ????̃(????????2)
Live Synthesis
Get PDFSynthesis automatically constructs an implementation that satisfies a given logical specification. In this paper, we study the live synthesis problem, where the synthesized implementation replaces an al- ready running system. In addition to satisfying its own specification, the synthesized implementation must guarantee a sound transition from the previous implementation. This version of the synthesis problem is highly relevant in “always-on” applications, where updates happen while the system is running. To specify the correct handover between the old and new implementation, we introduce an extension of linear-time temporal logic (LTL) called LiveLTL. A LiveLTL specification defines separate requirements on the two implementations and ensures that the new implementation satisfies, in addition to its own requirements, any obligations left unfinished by the old implementation. For specifications in LiveLTL, we show that the live synthesis problem can be solved within the same complexity bound as standard reactive synthesis, i.e., in 2EXPTIME. Our experiments show the necessity of live synthesis for LiveLTL specifications created from benchmarks of SYNTCOMP and robot control
Restoring Execution Environments of Jupyter Notebooks
Get PDFMore than ninety percent of published Jupyter notebooks do not state dependencies on external packages. This makes them non-executable and thus hinders reproducibility of scientific results. We present SnifferDog, an approach that 1) collects the APIs of Python packages and versions, creat- ing a database of APIs; 2) analyzes notebooks to determine candidates for required packages and versions; and 3) checks which packages are required to make the notebook executable (and ideally, reproduce its stored results). In its evaluation, we show that SnifferDog precisely restores execution environments for the largest majority of notebooks, making them immediately executable for end users
Discovering reliable causal rules
Get PDFWe study the problem of deriving policies, or rules, that when enacted on a complex system, cause a desired outcome. Absent the ability to perform controlled experiments, such rules have to be inferred from past observations of the system's behaviour. This is a challenging problem for two reasons: First, observational effects are often unrepresentative of the underlying causal effect because they are skewed by the presence of confounding factors. Second, naive empirical estimations of a rule's effect have a high variance, and, hence, their maximisation typically leads to spurious results.
To address these issues, we first identify conditions on the underlying causal system that—by correcting for the effect of potential confounders—allow estimating the causal effect from observational data. Importantly, we provide a criterion under which causal rule discovery is possible. Moreover, to discover reliable causal rules from a sample, we propose a conservative and consistent estimator of the causal effect, and derive an efficient and exact algorithm that maximises the estimator. Extensive experiments on a variety of real-world and synthetic datasets show that the proposed estimator converges faster to the ground truth than the naive estimator, recovers causal rules even at small sample sizes, and the proposed algorithm efficiently discovers meaningful rules
CTET+: A Beyond-Birthday-Bound Secure Tweakable Enciphering Scheme Using a Single Pseudorandom Permutation
No full textIn this work, we propose a construction of 2-round tweakable substitution-
permutation networks using a single secret S-box. This construction is based on
non-linear permutation layers using independent round keys, and achieves security
beyond the birthday bound in the random permutation model. When instantiated
with an n-bit block cipher with κ-bit keys, the resulting tweakable block cipher,
dubbed CTET+, can be viewed as a tweakable enciphering scheme that encrypts
wn-bit messages for any integer w ≥2 using 5n + κ-bit keys and n-bit tweaks,
providing 2n/3-bit security.
Compared to the 2-round non-linear SPN analyzed in [CDK+18], we both minimize
it by requiring a single permutation, and weaken the requirements on the middle
linear layer, allowing better performance. As a result, CTET+ becomes the first
tweakable enciphering scheme that provides beyond-birthday-bound security using
a single permutation, while its efficiency is still comparable to existing schemes
including AES-XTS, EME, XCB and TET. Furthermore, we propose a new tweakable
enciphering scheme, dubbed AES6-CTET+, which is an actual instantiation of CTET+
using a reduced round AES block cipher as the underlying secret S-box. Extensive
cryptanalysis of this algorithm allows us to claim 127 bits of security.
Such tweakable enciphering schemes with huge block sizes become desirable in the
context of disk encryption, since processing a whole sector as a single block significantly
worsens the granularity for attackers when compared to, for example, AES-XTS, which
treats every 16-byte block on the disk independently. Besides, as a huge amount
of data is being stored and encrypted at rest under many different keys in clouds,
beyond-birthday-bound security will most likely become necessary in the short term
Integrative analysis of epigenetics data identifies gene-specific regulatory elements
Get PDFUnderstanding how epigenetic variation in non-coding regions is involved in distal gene-expression regulation is an important problem. Regulatory regions can be associated to genes using large-scale datasets of epigenetic and expression data. However, for regions of complex epigenomic signals and enhancers that regulate many genes, it is difficult to understand these associations. We present StitchIt, an approach to dissect epigenetic variation in a gene-specific manner for the detection of regulatory elements (REMs) without relying on peak calls in individual samples. StitchIt segments epigenetic signal tracks over many samples to generate the location and the target genes of a REM simultaneously. We show that this approach leads to a more accurate and refined REM detection compared to standard methods even on heterogeneous datasets, which are challenging to model. Also, StitchIt REMs are highly enriched in experimentally determined chromatin interactions and expression quantitative trait loci. We validated several newly predicted REMs using CRISPR-Cas9 experiments, thereby demonstrating the reliability of StitchIt. StitchIt is able to dissect regulation in superenhancers and predicts thousands of putative REMs that go unnoticed using peak-based approaches suggesting that a large part of the regulome might be uncharted water
Degrees and Gaps: Tight Complexity Results of General Factor Problems Parameterized by Treewidth and Cutwidth
Get PDFIn the General Factor problem, we are given an undirected graph G and for each vertex v ∈ V(G) a finite set B_v of non-negative integers. The task is to decide if there is a subset S ⊆ E(G) such that deg_S(v) ∈ B_v for all vertices v of G. Define the max-gap of a finite integer set B to be the largest d ≥ 0 such that there is an a ≥ 0 with [a,a+d+1] ∩ B = {a,a+d+1}. Cornuéjols showed in 1988 that if the max-gap of all sets B_v is at most 1, then the decision version of General Factor is polynomial-time solvable. This result was extended 2018 by Dudycz and Paluch for the optimization (i.e. minimization and maximization) versions. We present a general algorithm counting the number of solutions of a certain size in time (M+1)^{tw}n^{O(1)}, given a tree decomposition of width tw, where M is the maximum integer over all B_v. By using convolution techniques from van Rooij (2020), we improve upon the previous (M+1)^{3tw}n^{O(1)} time algorithm by Arulselvan et al. from 2018.
We prove that this algorithm is essentially optimal for all cases that are not trivial or polynomial time solvable for the decision, minimization or maximization versions. Our lower bounds show that such an improvement is not even possible for B-Factor, which is General Factor on graphs where all sets B_v agree with the fixed set B. We show that for every fixed B where the problem is NP-hard, our (max B+1)^{tw}n^{O(1)} algorithm cannot be significantly improved: assuming the Strong Exponential Time Hypothesis (SETH), no algorithm can solve B-Factor in time (max B+1-ε)^{tw}n^{O(1)} for any ε > 0. We extend this bound to the counting version of B-Factor for arbitrary, non-trivial sets B, assuming #SETH.
We also investigate the parameterization of the problem by cutwidth. Unlike for treewidth, having a larger set B does not appear to make the problem harder: we give a 2^{cutw}n^{O(1)} algorithm for any B and provide a matching lower bound that this is optimal for the NP-hard cases
Artificial Fingerprinting for Generative Models: Rooting Deepfake Attribution in Training Data
No full textPhotorealistic image generation has reached a new level of quality due to the breakthroughs of generative adversarial networks (GANs). Yet, the dark side of such deepfakes, the malicious use of generated media, raises concerns about visual misinformation. While existing research work on deepfake detection demonstrates high accuracy, it is subject to advances in generation techniques and adversarial iterations on detection countermeasure techniques. Thus, we seek a proactive and sustainable solution on deepfake detection, that is agnostic to the evolution of generative models, by introducing artificial fingerprints into the models. Our approach is simple and effective. We first embed artificial fingerprints into training data, then validate a surprising discovery on the transferability of such fingerprints from training data to generative models, which in turn appears in the generated deepfakes. Experiments show that our fingerprinting solution (1) holds for a variety of cutting-edge generative models, (2) leads to a negligible side effect on generation quality, (3) stays robust against image-level and model-level perturbations, (4) stays hard to be detected by adversaries, and (5) converts deepfake detection and attribution into trivial tasks and outperforms the recent state-of-the-art baselines. Our solution closes the responsibility loop between publishing pre-trained generative model inventions and their possible misuses, which makes it independent of the current arms race
Robustness Certification for Point Cloud Models
Get PDFThe use of deep 3D point cloud models in safety-critical applications, such as autonomous driving, dictates the need to certify the robustness of these models to real-world transformations. This is technically challenging, as it requires a scalable verifier tailored to point cloud models that handles a wide range of semantic 3D transformations. In this work, we address this challenge and introduce 3DCertify, the first verifier able to certify the robustness of point cloud models. 3DCertify is based on two key insights: (i) a generic relaxation based on first-order Taylor approximations, applicable to any differentiable transformation, and (ii) a precise relaxation for global feature pooling, which is more complex than pointwise activations (e.g., ReLU or sigmoid) but commonly employed in point cloud models. We demonstrate the effectiveness of 3DCertify by performing an extensive evaluation on a wide range of 3D transformations (e.g., rotation, twisting) for both classification and part segmentation tasks. For example, we can certify robustness against rotations by ±60° for 95.7% of point clouds, and our max pool relaxation increases certification by up to 15.6%
QuickSilver: Modeling and Parameterized Verification for Distributed Agreement-Based Systems
Get PDFThe last decade has sparked several valiant efforts in deductive verification of distributed agreement protocols
such as consensus and leader election. Oddly, there have been far fewer verification efforts that go beyond
the core protocols and target applications that are built on top of agreement protocols. This is unfortunate, as
agreement-based distributed services such as data stores, locks, and ledgers are ubiquitous and potentially
permit modular, scalable verification approaches that mimic their modular design.
We address this need for verification of distributed agreement-based systems through our novel modeling
and verification framework, QuickSilver, that is not only modular, but also fully automated. The key enabling
feature of QuickSilver is our encoding of abstractions of verified agreement protocols that facilitates modular,
decidable, and scalable automated verification. We demonstrate the potential of QuickSilver by modeling
and efficiently verifying a series of tricky case studies, adapted from real-world applications, such as a data
store, a lock service, a surveillance system, a pathfinding algorithm for mobile robots, and more