Avatar

Michael Herzberg

PhD Candidate

Sheffield, UK


Hello!

I am Michael Herzberg, PhD Candidate in the Security of Advanced Systems Research Group at the University of Sheffield. Together with Dr. Achim D. Brucker, I build formal methods to make it easier to build secure software systems.

My areas of interest include static and dynamic analyses of (web) programs, building formal models of semi-formal standards in Isabelle/HOL, and finding new ways of assessing the security of programs.

For my PhD, I use formal methods to ensure that the core of web browsers is secure. In particular, I build formal models of the Document Object Model (DOM) and its extensions (Shadow DOM, HTML) with focus on the security of its component mechanisms in Isabelle/HOL.

If you see anything that interests you, feel free to send me an email!

Publications

Achim D. Brucker, Michael Herzberg. A Formal Semantics of the Core DOM in Isabelle/HOL. In WWW'18 Companion: The 2018 Web Conference Companion.

Abstract | Full Text (PDF) | DOI


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.


Achim D. Brucker, Michael Herzberg. On the Static Analysis of Hybrid Mobile Apps - A Report on the State of Apache Cordova Nation. Engineering Secure Software and Systems (ESSoS) 2016.

Abstract | Full Text (PDF) | DOI


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

Tony Ohmann, Michael Herzberg, Sebastian Fiss, Armand Halbert, Marc Palyart, Ivan Beschastnikh, Yuriy Brun. Behavioral resource-aware model inference. Automated Software Engineering (ASE) 2014.

Abstract | Full Text (PDF) | DOI


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.

Presentations

Achim D. Brucker, Michael Herzberg. The Evil Friend in Your Browser. SteelCon, 8. July 2017.

Abstract | Video


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.


Achim D. Brucker, Michael Herzberg. The Evil Friend in Your Browser. OWASP AppSec EU, 11. May 2017.

Abstract | Video


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.


Achim D. Brucker, Michael Herzberg. Combining the Security Risks of Native and Web Development: Hybrid Apps. OWASP AppSec EU, 11. May 2017.

Abstract | Video


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.


Achim D. Brucker, Michael Herzberg. On the Static Analysis of Hybrid Mobile Apps. University of Sheffield 2016 (Poster).

Education

University of Sheffield, UK
2016 - current

Ph.D in Computer Science.


University of Massachusetts Amherst, MA, USA
2013 - 2014

Year abroad in the Graduate School. During my time there, I took various courses related to algorithms and software engineering. Additionally, I contributed to Perfume, a tool for inferring resource-aware behavioural models.


Karlsruhe Institute of Technology, Germany
2011 - 2015

B.Sc. in Computer Science. Title of thesis: Static Code Analysis for Securing Cordova Applications, supervised by Dr. Achim D. Brucker at SAP Research.

Work Experience

The University of Sheffield, UK
Teaching Assisant for COM3501 Computer Security and Forensics
2016 - current

We host two lab sessions per semester. One lab involves using the Open-Source Fixed-Point Model-Checker OFMC to analyze the security of network protocols such as the Needham-Schroeder protocol. The other using web application security scanners such as Brakeman and Wapiti to assess the security of a vulnerable Ruby on Rails application that I wrote for this lab.

Teaching Assisant for COM3420 Software Hut
2016 - 2016

We take on the role of project managers towards groups of students that work on software projects from start to end for this module.


P&I ACES, SAP Research CEC Karlsruhe, Germany
Research Intern
2014 - 2016

We developed a static dataflow analysis algorithm for applications consisting of multiple programming languages, esp. Cordova applications with SAP Kapsel on Android which use a combination of Java and Javascript.


1&1 Internet AG, Karlsruhe, Germany
Software Engineering Intern
2013 - 2013

We migrated a large internal software project from Ant to Maven and from Java 5 to Java 7. Also, I contributed to planning and implementing a new database system for pre-purchasing domains. We improved and maintained existing software systems as well as participated in the agile Scrum process across multiple locations.

Projects

Damn Vulnerable Hybrid Mobile App (DVHMA), a hybrid mobile app for Android that intentionally contains vulnerabilities


ExtensionCrawler, a Python crawler for extensions from the Chrome Web Store.


DASCA, a tool that combines dynamic and static techniques for analysing code for finding security (i.e., vulnerabilities), safety, or reliability problems.