Helmholtz Center for Information Security
CISPA – Helmholtz-Zentrum für InformationssicherheitNot a member yet
3406 research outputs found
Sort by
A Formal Security Analysis of the Signal Messaging Protocol
Get PDFThe Signal protocol is a cryptographic messaging protocol that provides end-to-end encryption for instant messaging in WhatsApp, Wire, and Facebook Messenger among many others, serving well over 1 billion active users. Signal includes several uncommon security properties (such as “future secrecy” or “post-compromise security”), enabled by a novel technique called ratcheting in which session keys are updated with every message sent.
We conduct a formal security analysis of Signal’s initial extended triple Diffie-Hellman (X3DH) key agreement and Double Ratchet protocols as a multi-stage authenticated key exchange protocol. We extract from the implementation a formal description of the abstract protocol, and define a security model which can capture the “ratcheting” key update structure as a multi-stage model where there can be a “tree” of stages, rather than just a sequence. We then prove the security of Signal’s key exchange core in our model, demonstrating several standard security properties. We have found no major flaws in the design, and hope that our presentation and results can serve as a foundation for other analyses of this widely adopted protocol
Secure Authentication in the Grid: A Formal Analysis of DNP3: SAv5
Get PDFMost of the world’s power grids are controlled remotely. Their control messages are sent over potentially insecure channels, driving the need for an authentication mechanism. The main communication mechanism for power grids and other utilities is defined by an IEEE standard, referred to as DNP3; this includes the Secure Authentication v5 (SAv5) protocol, which aims to ensure that messages are authenticated. We provide the first security analysis of the complete DNP3: SAv5 protocol. Previous work has considered the message-passing sub-protocol of SAv5 in isolation, and considered some aspects of the intended security properties. In contrast, we formally model and analyse the complex composition of the protocol’s three sub-protocols. In doing so, we consider the full state machine, and the possibility of cross-protocol attacks. Furthermore, we model fine-grained security properties that closely match the standard’s intended security properties. For our analysis, we leverage the Tamarin prover for the symbolic analysis of security protocols. Our analysis shows that the core DNP3: SAv5 design meets its intended security properties. Notably, we show that a previously reported attack does not apply to the standard. However, our analysis also leads to several concrete recommendations for improving future versions of the standard
Dachshund: Digging for and Securing (Non-)Blinded Constants in JIT Code
No full textModern browsers such as Chrome and Edge deploy
constant blinding to remove attacker-controlled constants from
the JIT-compiled code. Without such a defense, attackers can
encode arbitrary shellcode in constants that get compiled to
executable code. In this paper, we review the security and
completeness of current constant blinding implementations. We
develop DACHSHUND, a fuzzing-driven framework to find user-specified constants in JIT-compiled code.
DACHSHUND reveals several cases in which JIT compilers of modern browsers fail
to blind constants, ranging from constants passed as function
parameters to blinded constants that second-stage code optimizers
revert to a non-protected form. To tackle this problem, we
then propose a JavaScript rewriting mechanism that removes
all constants from JavaScript code. We prototype this cross-
browser methodology as part of a Web proxy and show that
it can successfully remove all constants from JavaScript code
Fairness Beyond Disparate Treatment & Disparate Impact: Learning Classification without Disparate Mistreatment
No full text
Stack Overflow Considered Harmful? The Impact of Copy&Paste on Android Application Security
No full textThe ART of App Compartmentalization: Compiler-based Library Privilege Separation on Stock Android
Get PDFThird-party libraries are commonly used by app developers for alleviating the development efforts and for monetizing their apps. On Android, the host app and its third-party libraries reside in the same sandbox and share all privileges awarded to the host app by the user, putting the users' privacy at risk of intrusions by third-party libraries. In this paper, we introduce a new privilege separation approach for third-party libraries on stock Android. Our solution partitions Android applications at compile-time into isolated, privilege-separated compartments for the host app and the included third-party libraries. A particular benefit of our approach is that it leverages compiler-based instrumentation available on stock Android versions and thus abstains from modification of the SDK, the app bytecode, or the device firmware. A particular challenge for separating libraries from their host apps is the reconstruction of the communication channels and the preservation of visual fidelity between the now separated app and its libraries. We solve this challenge through new IPC-based protocols to synchronize layout and lifecycle management between different sandboxes. Finally, we demonstrate the efficiency and effectiveness of our solution by applying it to real world apps from the Google Play Store that contain advertisements
