I am happy to announce that Sakine Yalman will join the Software Assurance & Security Research Team as a PhD student.

Why formalize (e.g., developing a formal semantics) an existing standard (e.g., as we did with our formalization of the DOM standard)? Of course, there are obvious benefits such as identifying glitches or areas of (unwanted) under-specification, but what are the wider benefits?

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.

Quite often, we need to develop a detailed understanding how a system works, without having access to its internal implementation. For example, we might need to understand and old legacy system, which we want to connect to our brand-new infrastructure, or we want to do a security assessment of a third party system.

One approach to develop a better understanding of a “black-box” system is to infer a model (e.g., in form of a Finite State Machine) from system traces.

Usually, networks such as the Internet run many security protocols (e.g., TLS, IPSec, DNSSEC) in parallel. While the security properties of many of these protocols have been analyzed in great detail, much less research has been devoted to their parallel composition. It is far from self-evident that the parallel composition of secure protocols is still secure, in fact one can systematically construct counter-examples.

Software security vulnerabilities are a serious threat to software vendors and their customers: they can result in both monetary loss and loss of reputation. Thus, implementing a rigid secure software development life-cycle (SDLC) is a competitive advantage for a software vendor. Security testing is an important part of any SDLC. Moreover, it is commonly accepted that security testing should be applied as early as possible in software development.

Interested in applying Security Testing during development? We will offer a one-day continuous professional development (CDP) training on the 13th of September at The University of Sheffield.

Mentioning ontologies and Isabelle/HOL in one sentence, might sound weird for man of us. While both are somehow used for writing formal documents, the degree of formalization is, at least at the first glance, very much different.

We asked ourselves if it is possible to integrate ontologies into Isabelle, as the current document preparation system of Isabelle lacks a mechanism for ensuring the structure of different document types (as, e.g., required in certification processes) in general and, in particular, mechanism for linking informal and formal parts of a document.

The term “usable security” is on everyone’s lips and there seems to be a general agreement that, first, security controls should not unnecessarily affect the usability and unfriendliness of systems. And, second, that simple to use system should be preferred as they minimize the risk of handling errors that can be the root cause of security incidents such as data leakages.

But it also seems to be a general surprise (at least for security experts), why software developers always make so many mistakes that should be easy to avoid, and that lead to insecure software systems. In fact, many of the large security incidents of the last weeks/months/years are caused by “seemingly simple to fix” programming errors.