Helmholtz Center for Information Security
CISPA – Helmholtz-Zentrum für InformationssicherheitNot a member yet
3406 research outputs found
Sort by
AIGEN: Random Generation of Symbolic Transition Systems
Get PDFAIGEN is an open source tool for the generation of tran-
sition systems in a symbolic representation. To ensure diversity, it employs a uniform random sampling over the space of all Boolean functions with a given number of variables. AIGEN relies on reduced ordered binary decision diagrams (ROBDDs) and canonical disjunctive normal form (CDNF) as canonical representations that allow us to enumerate Boolean functions, in the former case with an encoding that is inspired by data structures used to implement ROBDDs. Several parameters allow the user to restrict generation to Boolean functions or transition systems with certain properties, which are then output in AIGER format. We report on the use of AIGEN to generate random benchmark problems for the reactive synthesis competition SYNTCOMP 2019, and present a comparison of the two encodings with respect to time and memory efficiency in practice
A11y and Privacy don’t have to be mutually exclusive: Constraining Accessibility Service Misuse on Android
Get PDFAccessibility features of Android are crucial in assisting people with disabilities or impairment to navigate their devices. However, the same, powerful features are commonly misused by shady apps for malevolent purposes, such as stealing data from other apps. Unfortunately, existing defenses do not allow apps to protect themselves and at the same time to be fully inclusive to users with accessibility needs.
To enhance the privacy protection of the user while preserving the accessibility features for assistive apps, we introduce an extension to Android’s accessibility framework. Our design is based on a study of how accessibility features are used in 95 existing accessibility apps of different types (malware, utility, and a11y). Based on those insights, we propose to model the usage of the accessibility framework as a pipeline of code modules, which are all sandboxed on the system-side. By policing the data flows of those modules, we achieve a more fine-grained control over the access to accessibility features and the way they are used in apps, allowing a balance between accessibility functionality for dependent users and reduced privacy risks. We demonstrate the feasibility of our solution by migrating two real-world apps to our privacy-enhanced accessibility framework
tHyENA: Making HyENA Even Smaller
Get PDFThis paper proposes a lightweight short-tweak tweakable blockcipher (tBC) based authenticated encryption (AE) scheme tHyENA, a tweakable variant of the high profile NIST LWC competition submission HyENA. tHyENA is structurally similar to HyENA, however, proper usage of short-tweaks for the purpose of domain separation, makes the design much simpler compact. We know that HyENA already achieves a very small hardware footprint, and tHyENA further optimizes it. To realize our claim, we provide NIST API compliant hardware implementation details and benchmark for tHyENA against HyENA and several other well-known sequential feedback-based designs. The implementation results depict that when instantiated with the tBC TweGIFT, tHyENA achieves an extremely low hardware footprint - consuming only around 680 LUTs and 260 slices while maintaining the full rate and the almost birthday bound security. To the best of our knowledge, this figure is significantly better than all the known implementation results of other lightweight ciphers with sequential structures
Modern Lower Bound Techniques in Database Theory and Constraint Satisfaction
Get PDFConditional lower bounds based on , the Exponential-Time Hypothesis (ETH), or similar complexity assumptions can provide very useful information about what type of algorithms are likely to be possible. Ideally, such lower bounds would be able to demonstrate that the best known algorithms are essentially optimal and cannot be improved further. In this tutorial, we overview different types of lower bounds, and see how they can be applied to problems in database theory and constraint satisfaction
Reactive Synthesis Beyond Realizability (Invited Tutorial)
Get PDFThe automatic synthesis of reactive systems from high-level specifications is a highly attractive and increasingly viable alternative to manual system design, with applications in a number of domains such as robotic motion planning, control of autonomous systems, and development of communication protocols. The idea of asking the system designer to describe what the system should do instead of how exactly it does it holds a great promise. However, providing the right formal specification of the desired behavior of a system is a challenging task in itself. In practice it often happens that the system designer provides a specification that is unrealizable, that is, there is no implementation that satisfies it. Such situations typically arise because the desired behavior represents a trade-off between multiple conflicting requirements, or because crucial assumptions about the environment in which the system will execute are missing. Addressing such scenarios necessitates a shift towards synthesis algorithms that utilize quantitative measures of system correctness. In this tutorial, I will discuss two recent advances in this research direction.
First, I will talk about the maximum realizability problem, where the input to the synthesis algorithm consists of a hard specification that must be satisfied by the synthesized system, and soft specifications which describe other desired, possibly prioritized properties, whose violation is acceptable. I will present a synthesis algorithm that maximizes a quantitative value associated with the soft specifications while guaranteeing the satisfaction of the hard specification. In the second half of the tutorial, I will present algorithms for synthesis in bounded environments, where a bound is associated with the sequences of input values produced by the environment. More concretely, these sequences consist of an initial prefix followed by a finite sequence repeated infinitely often, and satisfy the constraint that the sum of the lengths of the initial prefix and the loop does not exceed a given bound. I will also discuss the synthesis of approximate implementations from unrealizable specifications, which are guaranteed to satisfy the specification on at least a specified portion of the bounded-size input sequences. I will conclude by outlining some of the open avenues and challenges in quantitative synthesis from temporal logic specifications
A Systematic Literature Review of Empirical Methods and Risk Representation in Usable Privacy and Security Research
No full textUsable privacy and security researchers have developed a variety of approaches to represent risk to research participants. To understand how these approaches are used and when each might be most appropriate, we conducted a systematic literature review of methods used in security and privacy studies with human participants. From a sample of 633 papers published at five top conferences between 2014 and 2018 that included keywords related to both security/privacy and usability, we systematically selected and analyzed 284 full-length papers that included human subjects studies. Our analysis focused on study methods; risk representation; the use of prototypes, scenarios, and educational intervention; the use of deception to simulate risk; and types of participants. We discuss benefits and shortcomings of the methods, and identify key methodological, ethical, and research challenges when representing and assessing security and privacy risk. We also provide guidelines for the reporting of user studies in security and privacy
MLCapsule: Guarded Offline Deployment of Machine Learning as a Service
No full textMachine Learning as a Service (MLaaS) is a popular and convenient way to access a trained machine learning (ML) model trough an API. However, if the user's input is sensitive, sending it to the server is not an option. Equally, the service provider does not want to share the model by sending it to the client for protecting its intellectual property and pay-per-query business model. As a solution, we propose MLCapsule, a guarded offline deployment of MLaaS. MLCapsule executes the machine learning model locally on the user's client and therefore the data never leaves the client. Meanwhile, we show that MLCapsule is able to offer the service provider the same level of control and security of its model as the commonly used server-side execution. Beyond protecting against direct model access, we demonstrate that MLCapsule allows for implementing defenses against advanced attacks on machine learning models such as model stealing, reverse engineering and membership inference
CapablePtrs: Securely Compiling Partial Programs Using the Pointers-as-Capabilities Principle
Get PDFCapability machines such as CHERI provide memory capabilities that can be used by compilers to provide security
benefits for compiled code (e.g., memory safety). The existing
C to CHERI compiler, for example, achieves memory safety
by following a principle called “pointers as capabilities” (PAC).
Informally, PAC says that a compiler should represent a source
language pointer as a machine code capability. But the security
properties of PAC compilers are not yet well understood. We
show that memory safety is only one aspect, and that PAC compilers can provide significant additional security guarantees for
partial programs: the compiler can provide security guarantees
for a compilation unit, even if that compilation unit is later linked
to attacker-provided machine code.
As such, this paper is the first to study the security of PAC
compilers for partial programs formally. We prove for a model
of such a compiler that it is fully abstract. The proof uses a novel
proof technique (dubbed TrICL, read trickle), which should be
of broad interest because it reuses the whole-program compiler
correctness relation for full abstraction, thus saving work. We
also implement our scheme for C on CHERI, show that we can
compile legacy C code with minimal changes, and show that the
performance overhead of compiled code is roughly proportional
to the number of cross-compilation-unit function calls
Accountability in the Decentralised-Adversary Setting
Get PDFA promising paradigm in protocol design is to hold parties accountable for misbehavior, instead of postulating that they are trustworthy. Recent approaches in defining this property, called accountability, characterized malicious behavior as a deviation from the protocol that causes a violation of the desired security property, but did so under the assumption that all deviating parties are controlled by a single, centralized adversary. In this work, we investigate the setting where multiple parties can deviate with or without coordination in a variant of the applied-π calculus.
We first demonstrate that, under realistic assumptions, it is impossible to determine all misbehaving parties; however, we show that accountability can be relaxed to exclude causal dependencies that arise from the behavior of deviating parties, and not from the protocol as specified. We map out the design space for the relaxation, point out protocol classes separating these notions and define conditions under which we can guarantee fairness and completeness. Most importantly, we discover under which circumstances it is correct to consider accountability in the single-adversary setting, where this property can be verified with off-the-shelf protocol verification tools
Statically Detecting JavaScript Obfuscation and Minification Techniques in the Wild
Get PDFJavaScript is both a popular client-side programming language and an attack vector. While malware developers transform their JavaScript code to hide its malicious intent and impede detection, well-intentioned developers also transform their code to, e.g., optimize website performance. In this paper, we conduct an in-depth study of code transformations in the wild. Specifically, we perform a static analysis of JavaScript files to build their Abstract Syntax Tree (AST), which we extend with control and data flows. Subsequently, we define two classifiers, benefitting from AST-based features, to detect transformed samples along with specific transformation techniques.
Besides malicious samples, we find that transforming code is increasingly popular on Node.js libraries and client-side JavaScript, with, e.g., 90% of Alexa Top 10k websites containing a transformed script. This way, code transformations are no indicator of maliciousness. Finally, we showcase that benign code transformation techniques and their frequency both differ from the prevalent malicious ones