Helmholtz Center for Information Security
CISPA – Helmholtz-Zentrum für InformationssicherheitNot a member yet
3406 research outputs found
Sort by
Deep Learning for Temporal Logics
Get PDFTemporal logics are a well established formal specification paradigm to specify the behavior of systems, and serve as inputs to industrial-strength verification tools. We report on current advances in applying deep learning to temporal logical reasoning tasks, showing that models can even solve instances where competitive classical algorithms timed out
Monitoring with Verified Guarantees
Get PDFRuntime monitoring is generally considered a light-weight alternative to formal verification. In safety-critical systems, however, the monitor itself is a critical component. For example, if the monitor is responsible for initiating emergency protocols, as proposed in a recent aviation standard, then the safety of the entire system critically depends on guarantees of the correctness of the monitor. In this paper, we present a verification extension to the Lola monitoring language that integrates the efficient specification of the monitor with Hoare-style annotations that guarantee the correctness of the monitor specification. We add two new operators, assume and assert, which specify assumptions of the monitor and expectations on its output, respectively. The validity of the annotations is established by an integrated SMT solver. We report on experience in applying the approach to specifications from the avionics domain, where the annotation with assumptions and assertions has led to the discovery of safety-critical errors in the specifications. The errors range from incorrect default values in offset computations to complex algorithmic errors that result in unexpected temporal patterns
Convolutional Dynamic Alignment Networks for Interpretable Classifications
No full textWe introduce a new family of neural network models called Convolutional Dynamic Alignment Networks (CoDA-Nets), which are performant classifiers with a high degree of inherent interpretability. Their core building blocks are Dynamic Alignment Units (DAUs), which linearly transform their input with weight vectors that dynamically align with task-relevant patterns. As a result, CoDA-Nets model the classification prediction through a series of input-dependent linear transformations, allowing for linear decomposition of the output into individual input contributions. Given the alignment of the DAUs, the resulting contribution maps align with discriminative input patterns. These model-inherent decompositions are of high visual quality and outperform existing attribution methods under quantitative metrics. Further, CoDA-Nets constitute performant classifiers, achieving on par results to ResNet and VGG models on e.g. CIFAR-10 and TinyImagenet
Investigating Car Drivers’ Information Demand after Safety and Security Critical Incidents
Get PDFModern cars include a vast array of computer systems designed to remove the burden on drivers and enhance safety. As cars are evolving towards autonomy and taking over control, e.g. in the form of autopilots, it becomes harder for drivers to pinpoint the root causes of a car's malfunctioning. Drivers may need additional information to assess these ambiguous situations correctly. However, it is yet unclear which information is relevant and helpful to drivers in such situations.
Hence, we conducted a mixed-methods online survey N=60 on Amazon MTurk where we exposed participants to two security- and safety-critical situations with one of three different explanations.
We applied Thematic and Correspondence Analysis to understand which factors in these situations moderate drivers’ information demand. We identified a fundamental information demand across scenarios that is expanded by error-specific information types. Moreover, we found that it is necessary to communicate error sources, since drivers might not be able to identify them correctly otherwise. Thereby, malicious intrusions are typically perceived as more critical than technical malfunctions
COTS Drone Detection Using Video Streaming Characteristics
Get PDFCheap commercial off-the-shelf (COTS) drones have become widely available for consumers in recent years. Unfortunately, they also provide low-cost capabilities for attackers. Therefore, effective methods to detect the presence of non-cooperating rogue drones within a restricted area are highly required. Approaches based on detection of control traffic have been proposed but were not yet shown to work against other benign traffic, such as that generated by wireless security cameras.
In this work, we propose a novel drone detection framework based on a Random Forest classification model. In essence, the framework leverages specific patterns in video traffic transmitted by drones. The patterns consist of repetitive synchronization packets (denoted as pivots) which we use as features in the proposed machine learning classifier. We show that our framework can achieve up to 99% detection accuracy over an encrypted WiFi channel using only 20 packets originated from the drone. Our system is able to identify drone transmissions even among very similar WiFi transmission (such as a security camera video stream) and in a noisy scenario with background traffic
A Web Interface for Petri Nets with Transits and Petri Games
Get PDFDeveloping algorithms for distributed systems is an error-prone task. Formal models like Petri nets with transits and Petri games can prevent errors when developing such algorithms. Petri nets with transits allow us to follow the data flow between components in a distributed system. They can be model checked against specifications in LTL on both the local data flow and the global behavior. Petri games allow the synthesis of local controllers for distributed systems from safety specifications. Modeling problems in these formalisms requires defining extended Petri nets which can be cumbersome when performed textually. In this paper, we present a web interface that allows an intuitive, visual definition of Petri nets with transits and Petri games. The corresponding model checking and synthesis problems are solved directly on a server. In the interface, implementations, counterexamples, and all intermediate steps can be analyzed and simulated. Stepwise simulations and interactive state space generation support the user in detecting modeling errors
Explanation Beats Context: The Effect of Timing & Rationales on Users’ Runtime Permission Decisions
Get PDFCurrent mobile platforms leave it up to the app developer to decide when to request permissions (timing) and whether to provide explanations why and how users' private data are accessed (rationales). Given these liberties, it is important to understand how developers should use timing and rationales to effectively assist users in their permission decisions. While guidelines and recommendations for developers exist, no study has systematically investigated the actual influence of timing, rationales, and their combinations on users' decision-making process. In this work, we conducted a comparative online study with 473 participants who were asked to interact with mockup apps drawn from a pool of 120 variations of 30 apps. The study design was guided by developers' current permission request practices derived from a dynamic analysis of the top apps on Google Play. Our results show that there is a clear interplay between timing and rationales on users' permission decisions and the evaluation of their decisions, making the effect of rationales stronger when shown upfront and limiting the effect of timing when rationales are present. We therefore suggest adaptation to the available guidelines. We also find that permission decisions depend on the individuality of users, indicating that there is no one-fits-all permission request strategy, upon we suggest better individual support and outline one possible solution
Counting Homomorphisms to K4-minor-free Graphs, modulo 2
Get PDFWe study the problem of computing the parity of the number of homomorphisms from an input graph G to a fixed graph H. Faben and Jerrum [ToC'15]
introduced an explicit criterion on the graph H and conjectured that, if satisfied, the problem is solvable in polynomial time and, otherwise, the problem is complete for the complexity class #P of parity problems.
We verify their conjecture for all graphs H that exclude the complete graph on 4 vertices as a minor. Further, we rule out the existence of a subexponential-time algorithm for the #P-complete cases, assuming the randomised Exponential Time Hypothesis.
Our proofs introduce a novel method of deriving hardness from globally defined substructures of the fixed graph H. Using this, we subsume all
prior progress towards resolving the conjecture (Faben and Jerrum [ToC'15]; Göbel, Goldberg and Richerby [ToCT'14,'16]).
As special cases, our machinery also yields a proof of the conjecture for graphs
with maximum degree at most 3, as well as a full classification for the problem of counting list homomorphisms, modulo 2
Differentiable Pattern Set Mining
Get PDFPattern set mining has been successful in discovering small sets of highly informative and useful patterns from data. To find good models, existing methods heuristically explore the twice-exponential search space over all possible pattern sets in a combinatorial way, by which they are limited to data over at most hundreds of features, as well as likely to get stuck in local minima. Here, we propose a gradient based optimization approach that allows us to efficiently discover high-quality pattern sets from data of millions of rows and hundreds of thousands of features.
In particular, we propose a novel type of neural autoencoder called BinaPs, using binary activations and binarizing weights in each forward pass, which are directly interpretable as conjunctive patterns. For training, optimizing a data-sparsity aware reconstruction loss, continuous versions of the weights are learned in small, noisy steps. Hence, this formulation of our problem provides a link between the discrete search space and continuous optimization, thus allowing for a gradient based strategy to discover sets of high-quality and noise-robust patterns. Through extensive experiments on both synthetic and real world data, we show that BinaPs discovers high quality and noise robust patterns, and unique among all competitors, easily scales to real supermarket transaction and biological variant call data
A Large-Scale Interview Study on Information Security in and Attacks against Small and Medium-sized Enterprises
No full textCybercrime is on the rise. Attacks by hackers, organized crime and nation-state adversaries are an economic threat for companies world-wide. Small and medium-sized enterprises (SMEs) have increasingly become victims of cyberattacks in recent years. SMEs often lack the awareness and resources to deploy extensive information security measures.
However, the health of SMEs is critical for society: For example, in Germany, 38.8% of all employees work in SMEs, which contributed 31.9% of the German annual gross domestic product in 2018. Many guidelines and recommendations encourage companies to invest more into their information security measures. However, there is a lack of understanding of the adoption of security measures in SMEs, their risk perception with regards to cybercrime and their experiences with cyberattacks.
To address this gap in research, we performed 5,000 computer-assisted telephone-interviews (CATIs) with representatives of SMEs in Germany. We report on their experiences with cybercrime, management of information security and risk perception. We present and discuss empirical results of the adoption of both technical and organizational security measures and risk awareness in SMEs. We find that many technical security measures and basic awareness have been deployed in the majority of companies. We uncover differences in reporting cybercrime incidences for SMEs based on their industry sector, company size and security awareness. We conclude our work with a discussion of recommendations for future research, industry and policy makers