PhD Title: Securing Microservices with Just-In-Time Model Verification
Description: Most software companies have or are in the process of migrating into the microservice architectural style. Examples of companies that have already migrated are Amazon and Netflix. In this architectural style, software is developed by many small and independent functionalities called microservices. Advantages of microservices are that they are scalable, release software quicker, developed by different teams using different technologies and standards. However, ensuring they are secure is problematic. For example, a wrong integration of an authorization protocol led to the potential leak of the data of 90 million facebook users (https://about.fb.com/news/2018/09/security-update/). Traditional homogenous security policies are not applicable for microservice verification, because microservices within a single system often utilise different security protocols or mechanisms. Moreover, there is neither a single point for security enforcement, nor a holistic view of the system.
This project aims to provide an innovative approach for verifying security policies. Software engineers will be able to define security policies and then verify at runtime, while the system is executing, whether these policies are compliant in the microservice software or not. To abstract away the technologies used in different microservices and provide a holistic view of the software system, an architectural model will be obtained from the executing system using architecture recovery techniques.
The project will answer the following Research Questions (RQ) and produce the corresponding Outputs (O):
RQ1) What are the foundational theories required to define and check security policies on architectural models? O1) A security policy language and formalism to reason about security
RQ2) What verification and algorithmic theories are suitable, in practice, for monitoring the security behaviour of the microservice system at runtime? O2) A supervisory system to monitor security behaviour at runtime.
RQ3) How can we evaluate the efficiency of the security verification? O3) A tool for security verification and O4) Experimental evaluation
Application Guidelines: Please click here to download.
Eligibility Guidelines: Applicants must be eligible for home tuition fees either through nationality, residency (living in the UK for at least three years and not wholly for educational purposes) or other connection to the UK. Applicants will have or be expected to receive a first or upper-second class honours degree in an Engineering, Computer Science, Design, Mathematics, Physics or a similar discipline.
Application deadline: 26/06/2020 by Noon
Call for Position: Please click here to view the call for position