Logic flaws are prevalent in multiparty cloud services, which cause serious consequences, e.g., an attacker can make purchases without paying, or gets into other people’s accounts without password. For decades, researchers have been advocating formal verification as a solution, but in the real world developers face many major hurdles to do it. We introduce a technology that significantly lowers these hurdles, and show its effectiveness in real-world deployments.
An Ironclad App lets a user securely transmit her data to a remote machine with the guarantee that every instruction executed on that machine adheres to a formal abstract specification of the app's behavior. This does more than eliminate implementation vulnerabilities such as buffer overflows, parsing errors, or data leaks; it tells the user exactly how the app will behave at all times.
Zero-Effort Payments (ZEP) is a seamless mobile computing system designed to accept payments with no effort on the customer’s part beyond a one-time opt-in. With ZEP, customers need not present cards nor operate smartphones to convey their identities. ZEP uses three complementary identification technologies: face recognition, proximate device detection, and human assistance.
We are looking for participants to engage in a personalised online shopping experience. You will receive a £40 shopping voucher for your participation and get the opportunity to purchase a book at 90% discount. The experiment involves a session of online shopping during which we will measure your eye movements and bodily responses. The shopping session is followed by an interview and we will ask you to fill out a final questionnaire to give us feedback on the study.
Fast, efficient ECC Library
We are exploring ways to reconcile (national) security and privacy through the use of advanced cryptography.
Crowd-sourcing is increasingly being used for providing answers to online polls and surveys. However, existing systems, while taking care of the mechanics of attracting crowd workers, poll building, and payment, provide little that would help the survey-maker or pollster to obtain statistically significant results devoid of even the obvious selection biases. InterPoll: a platform for programming of crowd-sourced polls. Polls are expressed as embedded LINQ queries, whose results are provided to t
In this work, we explore the properties of the global PKI as it exists in practice. We then leverage this information to construct flexible mechanisms that allow observers to fashion individualized policies to determine certificate trust.
Dhwani enables information theoretically secure Near Field Communication (NFC) on existing mobile phones without requiring any special hardware or PKI infrastructure. It uses existing microphones and speakers on phones to perform acoustic NFC.
We investigate how people's behaviour online can be characterized in terms of psychometric measurements such as the Big-5 personality traits openness, conscientiousness, extraversion, agreeableness, and neuroticism as well as general intelligence and satisfaction-with-life. We investigate patterns of Facebook usage, website preferences, query logs, and Facebook Likes and look for interesting correlations which can be used to predict users behaviours, preferences or characteristics.
Embassies is a new model of client-side application delivery that keeps the client code minimal and secure, while pushing almost all functionality into the vendor-supplied applications. The code in this project implements the system described in the NSDI 2013 paper.
ZQL is a language and compiler that allows for client side compuations to be compiled with appropriate cryptographic checks to provide privacy and integrity.
The Web form is the primary mechanism for collecting personal information.
A new initiative to build networks of female researchers in different areas of mathematics, through Research Collaboration Conferences at math insitutes which focus on building collaboration groups consisting of senior and junior women in a given area.
The performance of the elliptic curve method (ECM) for integer factorizationplays an important role in the security assessment of RSA-based protocols as a cofactorization tool inside the number field sieve. This webpage gives addition-subtracting chains to optimize Edwards ECM in terms of both performance and memory requirements. See for more details the "ECM at Work" paper.
One of the barriers to adoption cloud database technologies such as SQL Azure is data security and privacy. Data is a valuable asset to most organizations and storing the data in the cloud is often perceived as a security risk. This project investigates encryption as a mechanism to address such data security concerns. In particular, the goal of the project is to research, design, and build a comprehensive database system that supports encryption as a first class citizen.
Mobile user experiences are enriched by applications that support disconnected operations to provide better mobility, availability, and response time. However, offline data access is at odds with security when the user is not trusted, especially in the case of mobile devices, which must be assumed to be under the full control of the user. Pasture leverages commodity trusted hardware to provide secure offline data access by untrusted users.
Mobile personalization and privacy
U-Prove is an innovative cryptographic technology that allows users to minimally disclose certified information about themselves when interacting with online resource providers. U-Prove provides a superset of the security features of Public Key Infrastructure (PKI), and also provide strong privacy protections by offering superior user control and preventing unwanted user tracking.
In the last 25 years, Elliptic Curve Cryptography (ECC) has become a mainstream primitive for cryptographic protocols and applications. ECC has been standardized for use in key exchange and digital signatures. This project focuses on efficient generation of parameters and implementation of ECC and pairing-based crypto primitives, across architectures and platforms.
Counterdog is an automated theorem prover for a counterfactual meta-logic on propositional Datalog. The prover is complete for the logic, and can prove (or disprove) counterfactual statements such as: "if 'p' is false in a Datalog program, but would be true if it contained 'a:-b', then 'b' is true in the program.". Counterdog is useful for reasoning about Datalog-based trust management languages. The theory and implementation were developed by Moritz Y. Becker and Nik Sultana.
Research on privacy concerns shows that the users are becoming more aware about third party tracking but have no effective means to deal with the issue. We have created a Cookie Tracker, an agent that watches the requests for cookie installations. It presents the user with online information about the sources of the cookies in question.
Curating verification problems and solutions for cryptographic software in C.
Outsourcing data streams and desired computations to a third party such as the cloud is practical for many companies due to overwhelming flow of information and excessively high resource requirements of their data stream applications. However, data outsourcing and remote computations intrinsically raise issues of trust, making it crucial to verify results returned by third parties. The SECOA project investigates techniques addressing this problem.