Helmholtz Center for Information Security
CISPA – Helmholtz-Zentrum für InformationssicherheitNot a member yet
3406 research outputs found
Sort by
Monitoring hyperproperties
No full textHyperproperties, such as non-interference and observational determinism, relate multiple system executions to each other. They are not expressible in standard temporal logics, like LTL, CTL, and CTL*, and thus cannot be monitored with standard runtime verification techniques. HyperLTL extends linear-time temporal logic (LTL) with explicit quantification over traces in order to express hyperproperties. We investigate the runtime verification problem of HyperLTL formulas for three different input models: (1) The parallel model, where a fixed number of system executions is processed in parallel. (2) The unbounded sequential model, where system executions are processed sequentially, one execution at a time. In this model, the number of incoming executions is a-priori unbounded and may in fact grow forever. (3) The bounded sequential model where the traces are processed sequentially and the number of incoming executions is bounded. We show that the existence of a bound in the parallel and bounded sequential models leads to a different notion of monitorability than in the unbounded sequential model. We show that deciding the monitoriability problem for alternation-free HyperLTL is PSPACE-complete while the problem is undecidable in general. For every input model, we provide monitoring algorithms along with run-time and storage optimizations. By recognizing properties of specifications such as reflexivity, symmetry, and transitivity, we reduce the number of comparisons between traces. For the sequential models, we present a technique that minimizes the number of traces that need to be stored. We evaluate our optimizations, showing that this leads to a more scalable monitoring and, in particular, a significantly lower memory consumption
StreamLAB: Stream-based Monitoring of Cyber-Physical Systems
No full textWith ever increasing autonomy of cyber-physical systems, monitoring becomes an integral part for ensuring the safety of the system at runtime. StreamLAB is a monitoring framework with high degree of expressibility and strong correctness guarantees. Specifications are written in RTLola, a stream-based specification language with formal semantics. StreamLAB provides an extensive analysis of the specification, including the computation of memory consumption and run-time guarantees. We demonstrate the applicability of StreamLAB on typical monitoring tasks for cyber-physical systems, such as sensor validation and system health checks
Memory Safety Preservation for WebAssembly
Get PDFWebAssembly (Wasm) is a next-generation portable compilation target for deploying applications written in high-level languages on the web. In order to protect their memory from untrusted code, web browser engines confine the execution of compiled Wasm programs in a memory-safe sandbox. Unfortunately, classic memory-safety vulnerabilities (e.g., buffer overflows and use-after-free) can still corrupt the memory within the sandbox and allow Wasm code to mount severe attacks. To prevent these attacks, we study a class of secure compilers that eliminate (different kinds of) of memory safety violations. Following a rigorous approach, we discuss memory safety in terms of hypersafety properties, which let us identify suitable secure compilation criteria for memory-safety-preserving compilers. We conjecture that, barring some restrictions at module boundaries, the existing security mechanisms of Wasm may suffice to enforce memory-safety preservation, in the short term. In the long term, we observe that certain features proposed in the design of a memory-safe variant of Wasm could allow compilers to lift these restrictions and enforce relaxed forms of memory safety
Temporal Stream Logic: Synthesis beyond the Bools
No full textReactive systems that operate in environments with complex data, such as mobile apps or embedded controllers with many sensors, are difficult to synthesize. Synthesis tools usually fail for such systems because the state space resulting from the discretization of the data is too large. We introduce TSL, a new temporal logic that separates control and data. We provide a CEGAR-based synthesis approach for the construction of implementations that are guaranteed to satisfy a TSL specification for all possible instantiations of the data processing functions. TSL provides an attractive trade-off for synthesis. On the one hand, synthesis from TSL, unlike synthesis from standard temporal logics, is undecidable in general. On the other hand, however, synthesis from TSL is scalable, because it is independent of the complexity of the handled data. Among other benchmarks, we have successfully synthesized a music player Android app and a controller for an autonomous vehicle in the Open Race Car Simulator (TORCS.
AccessiLeaks: Investigating Privacy Leaks Exposed by the Android Accessibility Service
Get PDFTo support users with disabilities, Android
provides the accessibility services, which implement
means of navigating through an app. According to the
Android developer’s guide: "Accessibility services should
only be used to assist users with disabilities in using
Android devices and apps". However, developers are
free to use this service without any restrictions, giving
them critical privileges such as monitoring user input
or screen content to capture sensitive information. In
this paper, we show that simply enabling the accessibility service leaves 72 % of the top finance and 80 %
of the top social media apps vulnerable to eavesdropping attacks, leaking sensitive information such as logins and passwords. A combination of several tools and
recommendations could mitigate the privacy risks: We
introduce an analysis technique that detects most of
these issues automatically, e.g. in an app store. We also
found that these issues can be automatically fixed in almost all cases; our fixes have been accepted by 70 % of
the surveyed developers. Finally, we designed a notification mechanism which would warn users against possible
misuses of the accessibility services; 50 % of users would
follow these notifications
HADES-IoT: A Practical Host-Based Anomaly Detection System for IoT Devices
Get PDFInternet of Things (IoT) devices have become ubiquitous and spread across many application domains including the industry, transportation, healthcare, and households.
However, the proliferation of the IoT devices has raised the concerns about their security - many manufacturers focus only on the core functionality of their products due to short time to market and low cost pressures, while neglecting security aspects.
Moreover, there is no established or standardized method for measuring and ensuring the security of IoT devices.
Consequently, vulnerabilities are left untreated, allowing attackers to exploit IoT devices for various purposes, such as compromising privacy, recruiting devices into a botnet, or misusing devices to perform cryptocurrency mining.
In this paper, we present a practical Host-based Anomaly DEtection System for IoT (HADES-IoT) as a novel last line of defense.
HADES-IoT has proactive detection capabilities, provides tamper-proof resistance, and can be deployed on a wide range of Linux-based IoT devices.
The main advantage of HADES-IoT is its low performance overhead, which makes it suitable for the IoT domain, where state-of-the-art approaches cannot be applied due to their high-performance demands.
We deployed HADES-IoT on seven IoT devices and demonstrated 100% effectiveness in the detection of current IoT malware such as VPNFilter and IoTReaper; while on average, requiring only 5.5% of available memory and causing only a low CPU load
simTPM: User-centric TPM for Mobile Devices (Technical Report)
Get PDFTrusted Platform Modules are valuable building blocks for security solutions and have also been recognized as beneficial for security on mobile platforms, like smartphones and tablets. However, strict space, cost, and power constraints of mobile devices prohibit an implementation as dedicated onboard chip and the incumbent implementations are software TPMs protected by Trusted Execution Environments.
In this paper, we present simTPM, an alternative implementation of a mobile TPM based on the SIM card available in mobile platforms. We solve the technical challenge of implementing a TPM2.0 in the resource-constrained SIM card environment and integrate our simTPM into the secure boot chain of the ARM Trusted Firmware on a HiKey960 reference board. Most notably, we address the challenge of how a removable TPM can be bound to the host device’s root of trust for measurement. As such, our solution not only provides a mobile TPM that avoids additional hardware while using a dedicated, strongly protected environment, but also offers promising synergies with co-existing TEE-based TPMs. In particular, simTPM offers a user-centric trusted module. Using performance benchmarks, we show that our simTPM has competitive speed with a reported TEE-based TPM and a hardware-based TPM
Deep Appearance Maps
No full textWe propose a deep representation of appearance, i. e., the relation of color, surface orientation, viewer position, material and illumination. Previous approaches have used deep learning to extract classic appearance representations relating to reflectance model parameters (e. g., Phong) or illumination (e. g., HDR environment maps). We suggest to directly represent appearance itself as a network we call a Deep Appearance Map (DAM). This is a 4D generalization over 2D reflectance maps, which held the view direction fixed. First, we show how a DAM can be learned from images or video frames and later be used to synthesize appearance, given new surface orientations and viewer positions. Second, we demonstrate how another network can be used to map from an image or video frames to a DAM network to reproduce this appearance, without using a lengthy optimization such as stochastic gradient descent (learning-to-learn). Finally, we show the example of an appearance estimation-and-segmentation task, mapping from an image showing multiple materials to multiple deep appearance maps