Verifying Security Properties in Modular Systems

Security is a huge concern in our digital society, especially with distributed systems like the Internet. Services deployed on such systems are frequently subject to malicious attacks; thus, verifying and enforcing its security is essential. One way of doing this is by using models like finite state automata. Past literature has explored how a system designer can easily verify and even enforce the security of a system: a supervisor can ensure that an outside observer cannot identify some secret in the system. Unfortunately, past research has been limited to single, autonomous systems, disregarding the distributed nature of modern systems. This project aims to find means of enforcing opacity (security) when there are multiple independent systems and supervisors, since opacity does not necessarily hold when the systems interact with one another. Additionally, this project aims to enforce opacity when there is a different attacker for each module of the system.

Faculty Supervisor:

Laurie Ricker

Student:

Partner:

Inria Rennes - Bretagne Atlantique Research Centre

Discipline:

Computer science

Sector:

Technology

University:

Mount Allison University

Program: