New Release - Isabelle/DOF 1.0.0

We are proud to announce the first public release of Isabelle/DOF. Isabelle/DOF is a Document Ontology Framework (DOF) allowing annotating text elements in formal developments with structured, typed meta-information. Developers can define this meta-information according to their needs, e.g., to enable semantic queries (in the sense of semantic web), tool interaction, or document generation.

A New Life - Cybersecurity @ Exeter

After three and a half years in Sheffield, it is, again, time for new challenges. After starting the security group in Sheffield by both making the business case for a security group and being its first member, I am doing it again: I am building a new Cybersecurity Group in Exeter: This time as Professor and Head of Group.

A Screening Test for Software Vulnerabilities

Software vendors that consume thousands of Free and Open Source Software (FOSS) components and offer more than a decade of support and security fixes are expected to react quickly on disclosed vulnerabilities—in some case such as Heartbleed, within hours.

This seems to be infeasible, in particular given that software vendors need to know rather precisely, if their product is affected by a vulnerability in a third party component or not: if they are not affected, they want to be able to re-assure their customers that they are not affected as well. If they are affected, they want to be able to fix the security vulnerability quickly and with the least possible impact on existing functionality (and the least effort for both the software vendor as well as its customers). So, how can we solve this problem?

Formalizing the Core DOM in Isabelle/HOL

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.