Musard Balliu and Elena Troubitsyna Gave Talks at Ericsson Research

Title: Application Security for the Web and IoT Domain

Abstract: Society increasingly relies on applications that handle sensitive information: private individuals and businesses use software applications that manipulate confidential or untrusted data.
My research makes it easier to build applications that handle sensitive data securely and uncover vulnerabilities in existing applications. To achieve this, I use programming language
techniques to develop tools that allow programmers to express application-specific security policies and enforce those policies efficiently, ultimately providing security guarantees
that build on solid foundations.

In this talk, I will give an overview of my research interests with special focus on IoT and Web application security. I will first present some recent work on discovering vulnerabilities in
very popular IoT platforms along with countermeasures for short- and long-term protection. Then, I will show how to achieve end-to-end web application security, by tracking information flows
through the client, the server, and the database. Afterwards, I will discuss a combination of formal and empirical methods to find vulnerabilities in existing web applications.
Finally, I will conclude with a few highlights on my current research directions in the areas of security and privacy. The talk is self-contained and, for the most part, no prior knowledge is required.

Title: A Formal Approach to modelling and verifying security requirements

16 In my talk, I will discuss  formal and model-driven approaches to modelling and verifying security requirements. First, I will briefly overview a correct-by-construction development paradigm. Then I will present a join work with Nokia Security group on using formal modelling to analyse security vulnerabilities in the telecommunications domain. The number of security attacks on the telecommunication networks is constantly increasing. To prevent them, the telecom sector is looking for new automated techniques facilitating a discovery of potential network vulnerabilities and rectification of them. We propose an approach for identifying potential attack scenarios and defining recommendations for preventing them. The approach is formalised in the Event-B framework. It allows us to not only formalise the analysed part of the network architecture and verify consistency of the control and dataflow of the associated services but also employ model checking to generate and analyse attack scenarios. By applying the proposed approach, the designers can systematically explore network vulnerabilities and propose recommendations for attack prevention.

In the second part of the talk, I will discuss a a model-driven approach to analyzing security of REST API and its application to analyzing OpenStack components. The approach is tailored to RESTful architecture and enables a structured analysis and model-based testing of security constraints.