Many state-of-the-art information-flow control (IFC) tools are implemented as Haskell libraries. A distinctive feature of this language is lazy evaluation. In his influencal paper on why functional programming matters John Hughes proclaims: "Lazy evaluation is perhaps the most powerful tool for modularization in the functional programmer’s repertoire”. Unfortunately, lazy evaluation makes IFC libraries vulnerable to leaks via the internal timing covert channel. The problem arises due to sharing, the distinguishing feature of lazy evaluation, which ensures that results of evaluated terms are stored for subsequent re-utilization. In this sense, the evaluation of a term in a high context represents a side-effect that eludes the security mechanisms of the libraries. A naïve approach to prevent that consists in forcing the evaluation of terms before entering a high context. However, this is not always possible in lazy languages, where terms often denote infinite data structures. Instead, we propose a new language primitive, lazyDup, which duplicates terms lazily. By using lazyDup to duplicate terms manipulated in high contexts, we make the security library MAC robust against internal timing leaks via lazy evaluation. We show that well-typed programs satisfy progress-sensitive non-interference in our lazy calculus with non-strict references. Our security guarantees are supported by mechanized proofs in the Agda proof assistant.

The Internet of Things has begun to touch the lives of many already, and we are reaping benefits in convenience and economic value.  Much has been invested in IoT security - and yet examples of insecure IoT devices and configurations are reported almost daily.  Relatively few of these reports have come from tangible examples of loss or disruption by malice so far.  Is this the calm before the storm?  Will the threats be contained, or will they overwhelm the IoT venture?  We will consider some of the possible future scenarios, and the possible professional responses to these.  It is clear that some profound improvement is needed: but is effort best focussed on engineering, design, law, regulation, consumer awareness, or all of these?  We will ask what can realistically be achieved, and whether that will be enough.

The proliferation of algorithms and AI systems is accelerating across the public (e.g. healthcare and criminal justice) and the private (e.g. finance and insurance) sectors. Automated decision-making systems are being more and more frequently used to make assessments or predictions about people. This new trend could lead to less biased and more accurate decisions, but also lead to inadvertent discrimination and privacy violations. Further, the decision-making process and effects of algorithmic decisions are often unclear, owing to the inherent opacity and inaccessibility of systems. There is increasing effort from the public and the private sectors to make these technologies more explainable and ultimately accountable. This talk will first consider the ethical challenges facing complex algorithmic systems concerning opacity, discrimination, group privacy, and moral responsibility for failures and harms. Ethical considerations often ground legal and regulatory action; recognising this, the second half of the talk will examine how these challenges are being addressed in European and American regulation, in particular concerning new provisions the European General Data Protection Regulation that pressures designers and users to explain how complex algorithmic systems function.

Technology is rapidly evolving and enriching the modern world with numerous of distributed cyber physical networks and so the applications. Many of the applications are integrated with extremely low-cost networked computers that add eye and ear (i.e., sensor) and arm, leg and voice (i.e., actuator) to perform their intended tasks efficiently. Inevitably, much of sensor nodes information are highly sensitive and critical, and thus security is a critical concern. In this seminar, I will provide an overview of my recent and ongoing research, i.e., design and analysis of security schemes in distributed cyber physical networks and applications.

As the Middle East goes through one of its most historic, yet painful episodes, the fate of the region’s Kurds have drawn substantial interest. Transnational Kurdish awakening—both political and armed—has attracted unprecedented global interest as individual Kurdish minorities across four countries, Turkey, Iraq, Iran, and Syria, have begun to shake their respective political status quo in various ways. In order to analyse this trend in a region in flux, this paper introduces a new methodology in generating computerised geopolitical data. Selfies of militants from three main warring non-state actors, ISIS, YPG and FSA, through February 2014 – February 2016, was sorted and operationalized through a dedicated repository of geopolitical events, extracted from a comprehensive open source archive of Turkish, Kurdish, Arabic, and Farsi sources, and constructed using entity extraction and recognition algorithms. These selfies were crosschecked against events related to conflict, such as unrest, attack, sabotage and bombings were then filtered based on human- curated lists of actors and locations. The result is a focused data set of more than 2000 events (or activity nodes) with a high level of geographical and temporal granularity. This data is then used to generate a series of four heat maps based on six-month intervals. They highlight the intensity of armed group events and the evolution of multiple fronts in the border regions of Turkey, Syria, Iraq and Iran.

Data arising in cyber-security applications often have a network, or graph-like, structure, and accurate statistical modelling of connectivity behaviour has important implications, for instance, for network intrusion detection. We present a linear algebraic approach to network modelling, which is massively scalable and also very general. In this approach, nodes are embedded in a finite dimensional latent space, where common statistical, signal-processing and machine-learning methodologies are then available, albeit with some new geometrical considerations. Mass testing for anomalous edges, correlations, and changepoints is then discussed. Results are illustrated on network data collected at Los Alamos National Laboratory. 

Roscoe recently showed how HISPs, a class of protocol to allow humans to contribute to the creation of secure authentic channels between them, can be made auditable in the sense that a failed attack on them cannot be disguised as communication failure.  In this paper we study the same issue for PAKEs: password authenticated key exchanges.  We find that because this second style of protocol relies on long term state, it is harder to make them auditable, and that to do so we have to develop new ideas on how to approximate fair exchange without a TTP. This is joint work by Professor Bill Roscoe (Oxford) and Professor Peter Ryan (Luxembourg)

As the Middle East goes through one of its most historic, yet painful episodes, the fate of the region’s Kurds have drawn substantial interest. Transnational Kurdish awakening—both political and armed—has attracted unprecedented global interest as individual Kurdish minorities across four countries, Turkey, Iraq, Iran, and Syria, have begun to shake their respective political status quo in various ways. In order to analyse this trend in a region in flux, this paper introduces a new methodology in generating computerised geopolitical data. Selfies of militants from three main warring non-state actors, ISIS, YPG and FSA, through February 2014 – February 2016, was sorted and operationalized through a dedicated repository of geopolitical events, extracted from a comprehensive open source archive of Turkish, Kurdish, Arabic, and Farsi sources, and constructed using entity extraction and recognition algorithms. These selfies were crosschecked against events related to conflict, such as unrest, attack, sabotage and bombings were then filtered based on human- curated lists of actors and locations. The result is a focused data set of more than 2000 events (or activity nodes) with a high level of geographical and temporal granularity. This data is then used to generate a series of four heat maps based on six-month intervals. They highlight the intensity of armed group events and the evolution of multiple fronts in the border regions of Turkey, Syria, Iraq and Iran.