Security Analysis and System Verification

The security and reliability of a software system depends upon the correctness and robustness of its component parts and of the system behaviour as a whole. Our work in this theme has focused on formal techniques for characterising and verifying the system behaviour at design time but also within the context of web and cloud environments that rely on the sharing of programs. Our current research programme covers the following areas:

Static and Probabilistic analysis Our work on Classical Static Analysis has permitted to verify (and expose security flaws) in communication protocols using control flow analysis and we have developed sophisticated heap analyses techniques to verify the absence of buffer overflows. More recently we have developed probabilistic techniques that allow to investigate non-interference aspects and verify system behaviour in the presence of a trade-off between data leakage and computational cost.

Secure Web Programming Staying safe and doing business on-line requires web programming tools and techniques that are robust and allow migration of programs. We have built faithful formal models for key components of the web programming ecosystem  (JavaSCript, PhP, HTTP protocol, etc.) and developed tools and techniques to verify the information flow, privacy and authorization properties of web applications. Our work on JavaSCript subsets has shown some to be safe (e.g., Google Caja) and has uncovered vulnerabilities in others (e.g. Facebook).

Symbolic Execution We have designed several symbolic execution tools that analyse program behaviour and identify input values that may cause an error. This provides developers with the concrete inputs that can trigger and diagnose vulnerabilities. For example, our tools generated actual disk images that when mounted under various file systems cause the Linux kernel to panic, and actual network packets that either crash or abort security-critical network daemons. 

Protocol analysis and formal verification Whilst through classic protocol analysis we have been able to validate (and uncover often subtle bugs) in respect of the authentication properties of security protocols, distributed systems also require verification in respect to other properties such as anonymity, privacy, reliability, recoverability and diagnosability, that cannot be tackled by traditional approaches. We have therefore developed novel model checking approaches for non-standard temporal logics that have allowed the verification of several cryptographic protocols and concrete systems, including web-services and autonomous submarines.

Research areaName of contact
 Static and Probabilistic Analysis Professor Chris HankinDr Herbert Wiklicky  
 Secure Web Programming Dr Sergio Maffeis
Symbolic Execution Tools Dr Cristian Cadar
Protocol Analysis and Formal Verification Professor Michael HuthProfessor Alessio  Lomuscio
 
Summary of the table's contents

Operational Systems and Information Assurance

The security and resilience of a system does not solely depend on its design and implementation but also on its ability to enforce the security policy, to adapt to changes and react to attacks and on the increased level of automation of security management. In addition to detecting intrusions and anomalous behaviour, systems must be able to operate in their presence whilst taking into account risk trade-offs of damage vs functionality. Work in this area also includes techniques for hardware-based acceleration of policy enforcement, cryptographic algorithms, and security-aware mechanisms (Professor Wayne Luk). Our current research programme covers the following areas:

Access Control and Authorisation Management Work has focussed on the development of policy-based authorisation and privacy systems that can take into account the context (e.g., location) in which the access requests are made. We have developed such systems for varied platforms ranging from embedded sensors to mobile devices, distributed systems and networks. To cater for “systems of systems” and the compositionality inherent in many applications we have developed policy algebras based on Belnap logic. To cater for exceptions and “manual override” we have developed novel "break-the-glass" authorisation frameworks that can provide rationale and monitor policy overrides. To cater for disconnected environments and uncontrolled circumstances we have developed techniques for risk-based authorisation decisions where learned access control decisions are combined with notions of utility, damage and uncertainty and trust-models that allow to reason about security in the presence of unknown or partially trusted information. 

Secure System Adaptation In addition to authorisation aspects we have developed policy-based frameworks that can enforce adaptation policies which define how a system should react and be reconfigured in response to security relevant events. Adaptation is also essential in mobile and pervasive environments where the security configuration depends on continuously changing parameters. Our work has led to several systems (e.g., Ponder2) that have been used in collaborative projects such as the IBM led US-UK ITA and by others in both academia and industry. Critical to the use of policies is the ability to analyse policies for conflicts and anomalies, link the policies to the high-level security objectives and cater for legacy systems and human involvement. We have pioneered work on policy analysis and formal policy refinement from high-level requirements to enforceable policies, and automated learning of policies from decisions made by legacy systems or human administrators. 

Networks Protecting systems relies on the ability to analyse networks, detect patterns of intrusions, anomalies and reason about the graph structures underpinning interactions. Our work on statistical monitoring and anomaly detection is applied to both computer networks and to the analysis of social interactions where we have developed new algorithms and techniques to predict hidden links and nodes and identify community structures (including hierarchical and overlapping communities).  In computer networks we have developed new techniques for the characterisation of Distributed Denial of Service attacks, biological models for the spread of malware and characterised the accuracy and success of existing techniques such as deep packet inspection. The results from this work have been used to formulate new techniques for reacting to attacks, intrusions and compromises in order to ensure network resilience and preserve the network operation but also to cognitive packet network techniques and demonstrate their resilience to attacks.  

Information Centric Security Each year financial losses from data loss exceed those from organised crime or hacking. We have developed information-centric security models that track the data flow through syst ems end-to-end, i.e. across a complex processing workflow that involves multiple administrative domains, and automatically prevents data disclosures. Based on this work we have designed a secure middleware platform that is used by the NHS to protect medical records in a distributed event-processing environment. This approach is being extended to mitigate vulnerabilities in web applications through data tracking at runtime and in cloud environments. Following similar principles, we have developed novel frameworks for document-centric information disclosure based Data Sharing Agreements between organisations and rights management frameworks. Our work has addressed the problems stemming from intermittent connectivity in mobile environments and has been applied to information exchange between first level responders in crisis management scenarios. We have also addressed issues regarding the automated protection of derived data, i.e., data created from multiple sources with different protection requirements through well-defined transformations. This work has applications in many domains including healthcare, finance, environmental sensing etc. 

Research areaName of contact
 Access Control and Authorisation Management  Dr Naranker DulayProfessor Michael Huth, Dr Emil Lupu, Professor Morris Sloman, Professor Chris HankinDr Alessandra Russo
 Secure System Adaptation  Dr Emil Lupu, Professor Morris SlomanDr Naranker DulayDr Alessandra Russo
Network Analysis and Network Security Professor Erol GelenbeDr Cong Ling, Prof Morris SlomanDr Niall AdamsDr Naranker Dulay, Dr Emil Lupu
Information Centric Security Dr Peter Pietzuch, Dr Emil Lupu
 
Summary of the table's contents