Skip to main content

Joannes VeTSS

VeTSS grant awarded to Johannes Kinder

  • Date07 December 2017

The grant aims to improve the applicability of dynamic symbolic execution for JavaScript code and develop a flexible specification and testing methodology for security properties.

Johannes

So-called dynamic languages like JavaScript and Python are immensely popular and are frequently cited as making programming accessible to a much broader audience. From origins as mostly toy languages these evolved to become essential building blocks of the modern IT infrastructure. Dynamic languages drive complex client applications, web frameworks, cloud infrastructure, and embedded devices, often handling security-sensitive data and even implementing cryptographic protocols. However, dynamic types and the often surprising semantics of languages like JavaScript make it difficult to spot subtle security bugs as long as they do not directly impact functionality.

Our main research hypothesis is that an inherently dynamic language is best served by a dynamic approach to verification that points to errors in the code without restricting the freedom of the developer. In this project, we will use test generation by dynamic symbolic execution (DSE) to systematically cover paths through programs and check security properties along those paths. On one hand, this means that we will not obtain any proofs over the entire program unless DSE terminates; on the other hand, all paths executed are guaranteed to be real (feasible) paths with respect to the execution environment. We see this project as an initial phase in a longer effort, to be continued in a follow-up project as part of VeTSS. We will initially focus on JavaScript as our target dynamic language, but are aiming to eventually generalise our work to other languages.

The Research Institute on Verified Trustworthy Software Systems (VeTSS) is a UK Academic Research Institute in Cyber Security at Imperial College London that is funded by the Engineering and Physical Sciences Research Council.

 

Related topics

Explore Royal Holloway

Get help paying for your studies at Royal Holloway through a range of scholarships and bursaries.

There are lots of exciting ways to get involved at Royal Holloway. Discover new interests and enjoy existing ones.

Heading to university is exciting. Finding the right place to live will get you off to a good start.

Whether you need support with your health or practical advice on budgeting or finding part-time work, we can help.

Discover more about our academic departments and schools.

Find out why Royal Holloway is in the top 25% of UK universities for research rated ‘world-leading’ or ‘internationally excellent’.

Royal Holloway is a research intensive university and our academics collaborate across disciplines to achieve excellence.

Discover world-class research at Royal Holloway.

Discover more about who we are today, and our vision for the future.

Royal Holloway began as two pioneering colleges for the education of women in the 19th century, and their spirit lives on today.

We’ve played a role in thousands of careers, some of them particularly remarkable.

Find about our decision-making processes and the people who lead and manage Royal Holloway today.