We run various seminars throughout the year around cyber security.
Revisiting security vulnerabilities in commercial password manager
20 August 2020
Dr Siamak F. Shahandashti (University of York, UK)
SEAL: Sealed-bid auction without auctioneers
25 June 2020
Professor Feng Hao (University of Warwick, UK).
Abstract: Vickrey auction is a second-price sealed-bid auction scheme, named after William Vickrey who among many other contributions first developed the theory for this scheme and won a Nobel prize in 1996. However, despite the extreme importance in the auction theory, Vickrey auction has rarely been used in practice.
One key obstacle concerns the trustworthiness of the auctioneer. The auctioneer can trivially learn all bid inputs which may contain trade secrets. Furthermore, a dishonest auctioneer might secretly modify the second-highest price in order to increase the auction revenue without bidders noticing it.
In this talk, we resolve this fundamental trust problem by designing a publicly verifiable e-auction scheme that completely removes the need for auctioneers. This represents a paradigm change from previous schemes. Our solution is called Self-Enforcing Auction Lot (SEAL). It does not require any secret channels between bidders; all communication is public and everyone including the third party observers can verify the integrity of the auction outcome.
The system allows bidders to jointly compute the winning bid while preserving the privacy of losing bids, as well as effectively resolving any tie in the contest if it exists. It supports both first-price and second-price sealed-bid auctions and most importantly, it occurs only a linear computation and communication complexity with respect to the bit length of the bid price, which is probably the best one may hope for. All these make SEAL a practical solution to deploy in a real-world application, e.g. as a smart contract on a blockchain platform.
A security and privacy analysis of the UK contact tracing app
29 May 2020
Dr Chris Culnane (UK).
Abstract: In this presentation we will present our analysis of the UK's Contact Tracing App. We will provide a critique of some of the design decision taken, as well as examining in more detail some of the technical implementation issues we found during our recent analysis.
Where applicable we will compare the approach to the one taken by Australia in their COVIDSafe app, highlighting similarities and differences, as well as signs of recent convergence on some technical aspects. Additionally, we will discuss some of the future challenges and risks that usage of these apps may create, and suggest steps that could be taken to mitigate such risks.
Secure auditing of internet services
6 March 2020
Dr Daniel O’Keeffe (Royal Holloway University of London, UK).
Abstract: Users of online services such as messaging, code hosting and collaborative document editing expect the services to uphold the integrity of their data. Despite providers’ best efforts, data corruption still occurs, but at present service integrity violations are excluded from SLAs. For providers to include such violations as part of SLAs, the competing requirements of clients and providers must be satisfied.
In this talk I will describe LibSEAL, a SEcure Audit Library for Internet services that creates a non-repudiable audit log of service operations and checks invariants to discover violations of service integrity. LibSEAL is a drop-in replacement for TLS libraries used by services, and runs inside a trusted execution environment, such as Intel SGX, to protect the integrity of the audit log. We evaluate LibSEAL with three popular online services (Git, ownCloud and Dropbox) and demonstrate that it is effective in discovering integrity violations with low overhead.
I will conclude the talk with a brief overview of some ongoing work in trustworthy cloud computing at Royal Holloway.
Learning quadratic games on networks
22 January 2020
Dr Xiaowen Dong (University of Oxford, UK).
Abstract: Individuals, or organisations, cooperate with or compete against one another in a wide range of practical situations. In the economics literature, such strategic interactions are often modelled as games played on networks, where an individual's payoff depends not only on her action but also that of her neighbours.
The current literature has largely focused on analysing the characteristics of network games in the scenario where the structure of the network, which is represented by a graph, is known beforehand. It is often the case, however, that the actions of the players are readily observable while the underlying interaction network remains hidden.
In this talk, I will introduce two novel frameworks for learning, from the observations on individual actions, network games with linear-quadratic payoffs, and in particular the structure of the interaction network. Both frameworks are based on the Nash equilibrium of such games and involve solving a joint optimisation problem for the graph structure and the individual marginal benefits.
We test the proposed frameworks on both synthetic and real world examples, and show that they can effectively and more accurately learn the games than the baselines. The proposed approach has both theoretical and practical implications for understanding strategic interactions in a network environment.
Logical dynamics in large games
20 November 2019
Professor Jam Ramanujam (The Institute of Mathematical Sciences, India).
Abstract: In two-player games, each player reasons about how the opponent would act at a position and expect herself (the player) to respond, and so on. Such intersubjectivity can be generalised to n-player games, and the logical basis of equilibrium notions is given thus.
However, what if n is large, say 10000? In such games payoffs are associated with strategy distributions rather than profiles. We discuss dynamics in such games and the use of logic to specify player types in these contexts.
Secure data outsourcing
15 November 2019
Associate Professor Alptekin Küpçü (Koc University, Turkey).
Abstract: As many services are moving to the cloud, we are losing control of our own data. This constitutes one of the biggest problems that we face in this decade. In this talk, I will first describe various cloud scenarios and services, including cloud storage and databases, and searching within them. I will briefly present the problems and current solutions to them, highlighting techniques to know to understand and improve current solutions, as well as open problems.
Establishing unlinkability relying on existing verification tools
30 October 2019
Dr Stéphanie Delaune (IRISA, France).
Abstract: Cryptographic protocols aim at securing communications over insecure networks such as the Internet, where dishonest users may listen to communications and interfere with them. For example, passports are no more pure paper documents. Instead, they contain a chip that stores additional information such as pictures and fingerprints of their holder. In order to ensure privacy, these chips include a mechanism, i.e. a cryptographic protocol, that does not let the passport disclose private information to external users. This is just a single example but of course privacy appears in many other contexts such as RFIDs technologies or electronic voting.
Formal methods have been successfully applied to automatically analyze traditional protocols and discover flaws. Privacy-type security properties (e.g. anonymity, unlinkability, ...) are expressed relying on a notion of behavioral equivalence, and are actually more difficult to analyse. We will discuss some recent advances that have been done to analyse automatically equivalence-based security properties, and we will review some issues that remain to be solved in this field. In particular, we will see that existing verification tools, such as ProVerif and Tamarin, are not suitable to analyse unlinkability. Therefore, we have developed a different approach: we design sufficient conditions that can then be effectively checked automatically using existing tools, and allows one to conclude on a number of case studies. This result, first published at S&P in 2016, has been recently extended to deal with stateful protocols. This is a joint work with D. Baelde, L. Hirschi, and S. Moreau.
Supersingular isogeny graphs
9 October 2019
Professor Omran Ahm (Institute for Research in Fundamental Sciences, Iran).
Abstract: The supersingular isogeny graphs are a class of expander graphs which have recently found applications in cryptography. In this talk, first, we explain what they are and then we explain how they have been used to construct cryptographic hash functions and key exchange protocols.
Ring signatures in blockchain
13 August 2019
Dr Tsz Hon Yuen (University of Hong Kong).
Abstract: Ring signature is a signature scheme which provides anonymity to the signer, without using trusted authority. It can be used in privacy-preserving applications such as e-voting and e-cash. Recently, it is used in cryptocurrency Monero to provide anonymity to spenders: the real spender's identity is hidden with respect to N public keys in the system. However, the ring signature used in Monero has signature size O(N), and N=10/20 in practice. Hence the level of anonymity is limited.
A number of researches has been done to reduce the signature size to O(log N). As a result, the ring size of N=2048 or more can be used in practice. It greatly increases the level of anonymity. In our recent work, we show how to construct such efficient ring signature using Bulletproof. We construct the most efficient O(log N)-size ring signature.
Tractable verification of multi-agent systems
29 May 2019
Dr Francesco Belardinelli (Imperial College London, UK).
Abstract: The formal verification of multi-agent systems is a key research area, as MAS are applied to the modelling and design of systems in domains as diverse as transportation, avionics, robotics, and security. Unfortunately, in many set ups of interest the model checking problem is either undecidable or untractable, thus hindering the development of any (efficient) model checking tool.
In this talk I will present two recent contributions on tractable model checking for multi-agent systems. In the first one we show how communication by broadcast can lead to a decidable model checking problem, also in the presence of imperfect information (and perfect memory). In the second contribution, we show that reasoning about a single resource in the temporal logic CTL comes at no extra computational cost. So, under specific assumptions, expressive logics for temporal and strategic reasoning can be applied effectively in the specification and verification of multi-agent systems.
15 May 2019
Dr Nikolaos Pitropakis (Edinburgh Napier University, UK).
Abstract: Domain squatting is a common adversarial practice where attackers register domain names that are purposefully similar to popular domains. During this presentation we will begin a journey, where we will explore DNS and all of the forms of domain squatting.
Then we will we focus on a specific type of domain squatting called “combosquatting,” in which attackers register domains that combine a popular trademark with one or more phrases (e.g., betterfacebook[.]com, youtube-live[.]com). We will discuss the results of the first large scale, empirical study of combosquatting where more than 468 billion DNS records, collected from passive and active DNS data sources over almost six years were used for the analysis.
Machine learning and cyber security: Friends or foes?
27 February 2019
Matilda Rhode (Cardiff University, UK).
Abstract: Cyber security challenges are constantly evolving. In the short-term malicious actors may tweak individual attacks or malicious software to bypass particular defences. In the longer term the trends in types of attack change whenever a new solution has been widely adopted. Cyber defences are the sticks shaping the malicious landscape but there are also carrots, new opportunities which give good returns relative to the effort of malicious actors. For example the wide adoption of internet of things devices typically introduces a weak point into a network; the increasing reliance on data and digital systems has made ransomware attacks highly lucrative.
Machine learning has been met with scepticism from the security community, as in a number of other domains, but in the last few years has begun to demonstrate its worth in real-world scenarios when compare to traditional rule-based systems. Neural networks in particular have helped to mitigate the problems caused by short term changes to attack techniques.
The wide adoption of machine learning into other domains has introduced new security challenges. Adversarial attacks on computer vision systems as used by self-driving cars and automatic CCTV analysis have created cyber security challenges that did not exists several years ago. Adversarial attacks can also impact machine learning solutions for extant security problems such as malware and intrusion detection. This talk will explore the prominent threats to the security of machine learning cyber defences and how to mitigate them.
Bridging the security gap of NFV/SDN with trusted computing
6 February 2019
Dr Ludovic Jacquin (HP Labs, Bristol).
Biography: Dr Ludovic Jacquin is a Senior Researcher at Hewlett Packard Labs – the research organisation of Hewlett Packard Enterprise – in Bristol, UK. He holds an Applied Mathematics and Computer Science MSc from ENSIMAG (Grenoble, France) and received his PhD in Computer Science from Grenoble University (France) in 2013.
His broader research interest is to develop security mechanisms for computer and network infrastructure, both at the hardware and operating system level. He joined the Security Lab of Hewlett Packard Enterprise in 2014 with a focus on trust and attestation of the network infrastructure in the new paradigm of SDN and their application to related environments such as NFV. During his Ph.D., he mainly worked on the impact of network signalling protocols on security protocols such as IPsec.
Abstract: This talk will present the role of trusted computing and TPMs in SHIELD.
SHIELD is a H2020 Innovation Action project that aims to deliver an open solution for dynamically establishing and deploying virtual Security infrastructures in ISPs and corporate networks. It leverages Trusted Computing technologies to bridge the gap between orchestration tools and the virtual security functions introduced by Network Function Virtualisation; SHIELD also addresses the equivalent gap in networking introduced by Software-Defined Networks between controllers and network elements.
The second part of the talk will focus on some of the future looking research done in the Security Lab of Hewlett Packard Labs.
A treasury system for cryptocurrencies: Enabling better collaborative
23 January 2019
Dr Bingsheng Zhang (University, UK).
Abstract: A treasury system is a community-controlled and decentralized collaborative decision-making mechanism for sustainable funding of blockchain development and maintenance. During each treasury period, project proposals are submitted, discussed, and voted for; top-ranked projects are funded from the treasury.
The Dash governance system is a real-world example of such kind of systems. In this work, we, for the first time, provide a rigorous study of the treasury system. We modelled, designed, and implemented a provably secure treasury system that is compatible with most existing blockchain infrastructures, such as Bitcoin, Ethereum, etc. More specifically, the proposed treasury system supports liquid democracy/delegative voting for better collaborative intelligence. Namely, the stakeholders can either vote directly on the proposed projects or delegate their votes to experts.
Its core component is a distributed universally composable secure end-to-end verifiable voting protocol. The integrity of the treasury voting decisions is guaranteed even when all the voting committee members are corrupted. To further improve efficiency, we proposed the world’s first honest verifier zero-knowledge proof for unit vector encryption with logarithmic size communication.
This partial result may be of independent interest to other cryptographic protocols. A pilot system is implemented in Scala over the Scorex 2.0 framework, and its benchmark results indicate that the proposed system can support tens of thousands of treasury participants with high efficiency. This work is to be published at NDSS 2019.
Rule control of teleo-reactive, multi-tasking, communicating robotic agents
9 January 2019
Professor Keith Clark (Emeritus Professor Imperial College, UK).
Abstract: The robotic agents are programmed in two rule based languages: QuLog and TeleoR. They communicate using a logic based pub/sub and addressed message routing server, Pedro.
QuLog is a flexibly typed multi-threaded relation+function+imperative rule language. Its declarative subset of relation and function defining rules is used for encoding an agent’s dynamic beliefs and static knowledge. Its imperative rules are used for programming an agent’s behaviour. Imperative rules can invoke the relation and function rules, but not vice versa.
TeleoR is an application specific extension of QuLog for programming agents controlling robotic devices. It is a major extension of the T-R language proposed by Nils Nilsson. T-R’s ancestry goes back to the conditional triangular table action plans of the first cognitive robot, Shakey, built and programmed by a team lead by Nilsson at SRI in the late 1960s. Both TeleoR and T-R have sequences of guarded robotic action rules clustered into parameterised procedures:
- Two agents each controlling one mobile robot in co-operative bottle collecting. The agents have a joint goal of together collecting a given number of bottles. They communicate so each agent knows how many bottles both robots have collected, and to avoid the robots colliding with minimal divergence from each robot’s current path. They each stop their robot when the joint total is reached.
- A multi-tasking agent controlling a robotic arm and fairly sharing its use between multiple concurrent construction tasks. Colleagues at UNSW Sydney have ported a slightly more complex two arm controlling version of the agent program to a Baxter robot building towers of letter labeled blocks.