Systems and software security

We develop state-of-the-art algorithms, methods and protocols to address security and privacy in networked and distributed system environments, and tools to build verifiable, trustworthy software systems. Our expertise covers a broad span of topics, including digital trust, security, and privacy.

The systems and software security members have research interests, which include:

• Developing security algorithms, methods, protocols, and architecture to protect data and information-based resources to ensure trustworthiness and privacy.
• Developing the mathematics of software and system computational behaviour through the study and development of system design, verification and validation methods.
• Developing privacy protection mechanisms for secure computation (homomorphic encryption and multiparty computation), anonymisation, differential privacy, obfuscation, anonymous credentials and zero-knowledge proofs.

Trustworthy software systems

We have strengths in the automation of reasoning to formally build verifiable, trustworthy software systems. Members of our research group have a world-leading reputation in malware and attack technologies, adversarial behaviour, security operations and incident management, cryptography, software, hardware and network security, privacy-enhancing technologies, software quality assurance, and how these are applied to the governance, risk management and compliance in cyber-security. Other areas of interest include distributed and cyber-physical systems security.

Award-winning software

We have developed award-winning software verification and testing tools, including ESBMC (Efficient SMT-based Bounded Model Checker) and JBMC (Java Bounded Model Checker). Over the last ten years, these tools have consistently won international competitions in software verification and testing, focusing on security. We have made significant contributions to software and systems verification and security: theory and implementation techniques.

Collaboration

We collaborate with other research groups in the Department of Computer Science, including the Formal Methods (FM), Information Management (IMG), Machine Learning and Robotics (MLR) and Advanced Processor Technologies (APT) groups. Our members are also affiliated with the UoM Centre for Digital Trust and Society.

We have also collaborated with industry partners such as Intel, ARM and Amazon Web Services (AWS).

Research focus

Our research is focused on the following specialist areas:

• 
  

  Cryptography

  Cryptography investigates the theory and practice of ensuring secure communication of computer-based systems by constructing and analysing protocols to prevent adversaries from reading private messages. We focus on formally verifying security properties of both abstract models and code implementing cryptographic protocols by combining abstract interpretation, symbolic execution and fuzzing.

  We apply advanced cryptographic techniques to design and evaluate secure and privacy-enhancing solutions for various application domains, including smart grid, e-health, e-banking, smart city and sharing economy.

• 
  

  Networked and distributed system security

  We are interested in designing intelligent security solutions for smart systems, including cryptographic methods, security protocols and system architectures to protect networks, devices, services and data from security attacks or unauthorised access in networked and distributed systems and to facilitate authorised access to resources with privacy preservation.

  Our work settings include wireless sensor networks, mobile ad hoc networks, ubiquitous computing, electronic commerce, Internet of Things, Fog and Cloud computing, focusing on threat identification, risk assessment, and countermeasure designs.

• 
  

  Data and identity privacy

  Data and identity privacy protection are of paramount importance. We have a broad interest and expertise in designing, analysing and implementing privacy-enhancing technologies.

  We do theoretical research on the nature of data and identity privacy protection and applied work related to a wide range of application domains such as smart grid, smart city, sharing economy, connected vehicles and the Internet of things (IoT).

• 
  

  Systems and Software Verification

  We investigate the theory and practice of automatically analysing software systems’ behaviour for any given security or safety property. In particular, we develop methods, algorithms and tools to demonstrate correctness with solid mathematical guarantees of software systems using model checking, abstract interpretation, theorem proving, and runtime verification.

  We focus on security applications for smart contracts, punishment (not reward) blockchain architecture, cyber-controls, robotics, industrial control systems and the Internet of things (IoT).

• 
  

  Systemic view of governance in cyber resilience

  We learn from the limited integration of historic sociotechnical approaches, which tend to favour user awareness and training, to the tacit, anthropotechnical balance of whole systems based on situational awareness and forensic readiness that will enable them to act on feedback to cope with attack and other failures.