---

Most popular technologies are based on informal or semi- formal standards that lack a rigid formal semantics. Typical examples include web technologies such as the DOM or HTML, which are de- fined by the Web Hypertext Application Technology Working Group (WHATWG) and the World Wide Web Consortium (W3C). While there might be API specifications and test cases meant to assert the compli- ance of implementations, the actual standard is rarely accompanied by a formal model that would lend itself for, e. g., verifying the security or safety properties of real systems.

Even when such a formalization of a standard exists, two important questions arise: first, to what extent does the formal model comply with the standard and, second, to what extent does a concrete implementation comply with the formal model and the assumptions made during the verification of certain properties?

In this paper, we present an approach that brings all three involved artifacts—the (semi-)formal standard, the formalization of the standard, and the implementations—closer together by combining verification, sym- bolic execution, and specification-based testing.

---

At its core, the Document Object Model (DOM) defines a tree-like data structure for representing documents in general and HTML documents in particular. It is the heart of any modern web browser.

Formalizing the key concepts of the DOM is a prerequisite for the formal reasoning over client-side JavaScript programs and for the analysis of security concepts in modern web browsers.

We present a formalization of the core DOM, with focus on the node-tree and the operations defined on node-trees, in Isabelle/HOL. We use the formalization to verify the functional correctness of the most important functions defined in the DOM standard. Moreover, our formalization is 1. extensible, i.e., can be extended without the need of re-proving already proven properties and 2. executable, i.e., we can generate executable code from our specification.

---

Developing mobile applications is a challenging business: developers need to support multiple platforms and, at the same time, need to cope with limited resources, as the revenue generated by an average app is rather small. This results in an increasing use of cross-platform development frameworks that allow developing an app once and offering it on multiple mobile platforms such as Android, iOS, or Windows.

Apache Cordova is a popular framework for developing multi-platform apps. Cordova combines HTML5 and JavaScript with native application code. Combining web and native technologies creates new security challenges as, e.g., an XSS attacker becomes more powerful.

In this paper, we present a novel approach for statically analysing the foreign language calls. We evaluate our approach by analysing the top Cordova apps from Google Play. Moreover, we report on the current state of the overall quality and security of Cordova apps.

Keywords: Static program analysis, Static application security testing, Android, Cordova, Hybrid mobile apps

---

Software bugs often arise because of differences between what developers think their system does and what the system actually does. These differences frustrate debugging and comprehension efforts. We describe Perfume, an automated approach for inferring behavioral, resource-aware models of software systems from logs of their executions. These finite state machine models ease understanding of system behavior and resource use.

Perfume improves on the state of the art in model inference by differentiating behaviorally similar executions that differ in resource consumption. For example, Perfume separates otherwise identical requests that hit a cache from those that miss it, which can aid understanding how the cache affects system behavior and removing cache-related bugs. A small user study demonstrates that using Perfume is more effective than using logs and another model inference tool for system comprehension. A case study on the TCP protocol demonstrates that Perfume models can help understand non-trivial protocol behavior. Perfume models capture key system properties and improve system comprehension, while being reasonably robust to noise likely to occur in real-world executions.

---

On the one hand, browser extensions, e.g., for Chrome, are very useful, as they extend web browsers with additional functionality (e.g., blocking ads). On the other hand, they are the most dangerous code that runs in your browsers: extension can read and modify both the content displayed in the browser. As they also can communicate with any web-site or web-service, they can report both data and metadata to external parties.

The current security model for browser extensions seems to be inadequate for expressing the security or privacy needs of browser users. Consequently, browser extensions are a “juice target” for attackers targeting web users.

We present results of analysing thousands of browser extensions on how they use the current security model and discuss examples of extensions that are potentially of high risk. Based on the results of our analysis of real world browser extensions as well as our own threat model, we discuss the limitations of the current security model form a user perspective.

---

On the one hand, browser extensions, e.g., for Chrome, are very useful, as they extend web browsers with additional functionality (e.g., blocking ads). On the other hand, they are the most dangerous code that runs in your browsers: extension can read and modify both the content displayed in the browser. As they also can communicate with any web-site or web-service, they can report both data and metadata to external parties. The current security model for browser extensions seems to be inadequate for expressing the security or privacy needs of browser users. Consequently, browser extensions are a "juice target" for attackers targeting web users.

We present results of analysing over 2500 browser extensions on how they use the current security model and discuss examples of extensions that are potentially of high risk. Based on the results of our analysis of real world browser extensions as well as our own threat model, we discuss the limitations of the current security model from a user perspective.

---

Cross-platform frameworks, such as Apache Cordova, are becoming increasingly popular. They promote the development of hybrid apps that combine native, i.e., system specific, code and system independent code, e.g., HTML5/JavaScript. Combining native with platform independent code opens Pandora's box: all the the security risks for native development are multiplied with the security risk of web applications.

In the first half of our talk, we start our talk with short introduction into hybrid app development, present specific attacks followed by a report on how Android developers are using Apache Cordova. In the second half of the talk, we will focus on developing secure hybrid apps: both with hands-on guidelines for defensive programming as well as recommendations for hybrid app specific security testing strategies.