Helmholtz Center for Information Security
CISPA – Helmholtz-Zentrum für InformationssicherheitNot a member yet
3406 research outputs found
Sort by
A Novel Approach for Reasoning about Liveness in Cryptographic Protocols and its Application to Fair Exchange
No full textIn this paper, we provide the first methodology for reasoning about liveness properties of cryptographic protocols in a machine-assisted manner without imposing any artificial, finite bounds on the protocols and execution models. To this end, we design an extension of the SAPiC process calculus so that it supports key concepts for stating and reasoning about liveness properties, along with a corresponding translation into the formalism of multiset rewriting that the state-of-the-art theorem prover Tamarin relies upon. We prove that this translation is sound and complete and can thereby automatically generate sound Tamarin specifications and automate the protocol analysis. Second, we applied our methodology to two widely investigated fair exchange protocols -- ASW and GJM -- and to the Secure Conversation Protocol standard for industrial control systems, deployed by major players such as Siemens, SAP and ABB. For the fair exchange protocols, we not only re-discovered known attacks, but also uncovered novel attacks that previous analyses based on finite models and restricted number of sessions did not detect. We suggest fixed versions of these protocols for which we prove both fairness and timeliness, yielding the first automated proofs for fair exchange protocols that rely on a general model without restricting the number of sessions and message size. For the Secure Conversation Protocol, we prove several strong security properties that are vital for the safety of industrial systems, in particular that all messages (e.g., commands) are eventually delivered in order
Efficient and Flexible Discovery of PHP Application Vulnerabilities
Get PDFThe Web today is a growing universe of pages and applications teeming with interactive content. The security of such applications is of the utmost importance, as exploits can have a devastating impact on personal and economic levels. The number one programming language in Web applications is PHP, powering more than 80% of the top ten million websites. Yet it was not designed with security in mind, and, today, bears a patchwork of fixes and inconsistently designed functions with often unexpected and hardly predictable behavior that typically yield a large attack surface. Consequently, it is prone to different types of vulnerabilities, such as SQL Injection or Cross-Site Scripting. In this paper, we present an interprocedural analysis technique for PHP applications based on code property graphs that scales well to large amounts of code and is highly adaptable in its nature. We implement our prototype using the latest features of PHP 7, leverage an efficient graph database to store code property graphs for PHP, and subsequently identify different types of Web application vulnerabilities by means of programmable graph traversals. We show the efficacy and the scalability of our approach by reporting on an analysis of 1,854 popular open-source projects, comprising almost 80 million lines of code
Data flow oriented UI testing: exploiting data flows and UI elements to test Android applications
No full textTesting user interfaces (UIs) is a challenging task. Ideally, every sequence of UI elements should be tested to guarantee that the application works correctly. This is, however, unfeasible due to the number of UI elements in an application. A better approach is to limit the evaluation to UI elements that affect a specific functionality. In this paper I present a novel technique to identify the relation between UI elements using the statically extracted data flows. I also present a method to refine these relations using dynamic analysis, in order to ensure that relations extracted from unreachable data flows are removed. Using these relations it is possible to more efficiently test a functionality. Finally, I present an approach to evaluate how these UI-aware data flows can be used as an heuristic to measure test coverage
