Privacy-preserving blueprints enable users to create escrows using the auditor's public key. An escrow encrypts the evaluation of a function P(t,x), where t is a secret input used to generate the auditor's key and x is the user's private input to escrow generation. Nothing but P(t,x) is revealed even to a fully corrupted auditor. The original definition and construction (Kohlweiss et al., EUROCRYPT'23) only support the evaluation of functions on an input x provided by a single user.
We address this limitation by introducing updatable privacy-preserving blueprint schemes (UPPB), which enhance the original notion with the ability for multiple parties to non-interactively update the private value x in a blueprint. Moreover, a UPPB scheme allows for verifying that a blueprint is the result of a sequence of valid updates while revealing nothing else.
We present uBlu, an efficient instantiation of UPPB for computing a comparison between private user values and a private threshold t set by the auditor, where the current value x is the cumulative sum of private inputs, which enables applications such as privacy-preserving anti-money laundering and location tracking. Additionally, we show the feasibility of the notion generically for all value update functions and (binary) predicates from FHE and NIZKs.
Our main technical contribution is a technique to keep the size of primary blueprint components independent of the number of updates and reasonable for practical applications. This is achieved by elegantly extending an algebraic NIZK by Couteau and Hartmann (CRYPTO'20) with an update function and making it compatible with our additive updates. This result is of independent interest and may find additional applications thanks to the concise size of our proofs.
In this seminar I will present the paper that lies the foundation for the phd position I applied to. Key Transparency Log are an emerging technique to provide a secure and transparent way to manage and distribute cryptographic keys in centralised systems such as WhatsApp and iMessage. This paper (by Brorsson et al) presents a new way to prevent split-view attacks in Key Transparency Logs by leveraging light-weight and scalable cryptographic tools.
In a world where cryptographic constructs are stuck in a race against faster algorithms, we propose a cosmic solution: why not root cryptographic provable delays in the speed of light? This paper introduces Sequential Communication Delay (SCD) in the Universal Composability framework, a functionality models communication channels where data is transmitted fashionably late. With our SCD proofs, we proposed the first constructions of a Verifiable Delay Function and a Publicly Verifiable Time-Lock Puzzle that do not rely on computational assumptions Say goodbye to the worries of computational speed-ups and hello to a time-delay rooted in the cosmos!
The advent of privacy laws and principles such as data minimization and informed consent are supposed to protect citizens from over-collection of personal data. Nevertheless, current processes, mainly through filling forms are still based on practices that lead to over-collection. Indeed, any citizen wishing to apply for a benefit (or service) will transmit all their personal data involved in the evaluation of the eligibility criteria. The resulting problem of over-collection affects millions of individuals, with considerable volumes of information collected. If this problem of compliance concerns both public and private organizations (e.g., social services, banks, insurance companies), it is because it faces non-trivial issues, which hinder the implementation of data minimization by developers. In this paper, we propose a new modeling approach that enables data minimization and informed choices for the users, for any decision problem modeled using classical logic, which covers a wide range of practical cases. Our data minimization solution uses game theoretic notions to explain and quantify the privacy payoff for the user. We show how our algorithms can be applied to practical cases study as a new PET for minimal, fully accurate (all due services must be preserved) and informed data collection. If time permits, we will perform a short demonstration of our prototype system.
Computer systems are increasingly relied upon for a wide range of important tasks, but much of the research on reliability has been restricted to the control systems for safety-critical hardware. For other systems, efforts to assess their effectiveness has been more ad-hoc and of questionable validity, even those relied upon to produce legally admissible evidence. From breathalyzers and forensic software to the infamous Post Office Horizon system, computer bugs can make the difference between someone being imprisoned and going free. This talk will discuss some examples of computer evidence failures risking causing miscarriages of justice, and what can be done to mitigate such risks in the future. In particular, it will motivate the idea that computer systems relied upon for computer evidence should be built with rigorous engineering techniques, but that these techniques are distinct from what are needed for safety-critical systems. When combined with appropriate treatment by the legal system, we can help avoid future miscarriages of justice.
Cryptography, data Hiding and digital watermarking algorithms being the basic building blocks for making powerful security solutions and security and privacy protocols. The systems at each end must negotiate and establish the configuration of these basic algorithms and their parameters before secure communication can occur. I will describe my research on the design of different types of cryptographic algorithms aimed at some application domains which will span everything from crypto-compression techniques and new image cryptosystems to lightweight cryptographic primitives for resource-restrained devices. One of the main objectives will be to provide a formal verification of these algorithms regarding their statistical, differential, and linear cryptanalysis, to verify their claims of security proof. In addition to standard cryptography, we might look at new ways to support confidentiality, e.g., data hiding in digital images. I will be talking about blind steganalysis methods using machine learning/deep learning methods which can be used in targeted attacks to break or assess the security of these data hiding systems. I will also illustrate the significant value that a rigorous cryptanalysis / security evaluation plays in the comprehensive design of what the critical security and privacy constructs. These techniques combine domain knowledge and cryptographic algorithms to secure the way in which sensitive data can be integrated. This analysis may provide an understanding of what types of algorithms can be better to use based on their cryptanalysis work.
WebAssembly is a new low-level programming language designed with the goal to increase interoperability and security across the software ecosystem. The WebAssembly specification is defined by the World Wide Web Consortium, with a multitude of implementors, ranging from browsers to standalone runtimes.
In order to ensure adherence to the specification, some WebAssembly implementations use formally-verified interpreters as testing oracles. This thesis explores a novel approach to designing a formally-verified interpreter, by using an intrinsically-typed representation of the WebAssembly syntax.
This intrinsically-typed interpreter is implemented in the Lean 4 proof assistant, leveraging its functional-but-in-place features to achieve good performance without sacrificing functional purity.
Cyber-physical systems tightly integrate computational resources with physical processes through sensing and actuating, widely penetrating various safety-critical domains, such as autonomous driving, medical monitoring, and industrial control. Unfortunately, they are susceptible to assorted attacks that can result in injuries or physical damage soon after the system is compromised. Consequently, we require mechanisms that swiftly recover their physical states, redirecting a compromised system to desired states to mitigate hazardous situations that can result from attacks. However, existing recovery studies have overlooked stochastic uncertainties that can be unbounded, making a recovery infeasible or invalidating safety and real-time guarantees. In this talk, I will present a novel recovery approach that achieves the highest probability of steering the physical states of systems with stochastic uncertainties to a target set rapidly or within a given time. Finally, I will demonstrate the practicality of our solution through the implementation in multiple use cases encompassing both linear and nonlinear dynamics, including robotic vehicles, drones, and vehicles in high-fidelity simulators.
Software supply chain attacks exploit discrepancies between source code repositories and deployed artifacts, highlighting the need for rigorous integrity checks during the artifact’s build process. As systems grow in complexity, preemptive measures are essential to ensure that the source code certifiably aligns with the deployed code. Modern software development relies heavily on third-party libraries sourced from registries like Maven Central, npm, and PyPI. However, these ecosystems have become prime targets for supply-chain attacks, introducing malware into and also shadowing trusted packages. Such attacks jeopardize both developers and users, compromising the integrity of their software supply chain. This presentation discusses recent supply chain attacks and proposed solutions. Additionally, we present Macaron, our open-source project from Oracle Labs offering a flexible checker framework and policy engine to detect and mitigate supply chain security threats, safeguarding software components and maintaining their security posture over the development lifecycle.
The threat and severe consequences (financial or otherwise) of ransomware in traditional desktop- and handheld-based computer systems have been well documented in the literature. The same cannot be said for systems comprising constrained, embedded IoT devices used in industrial applications: When it comes to ransomware, the landscape is still largely unexplored. In industrial settings, IoT devices have started being considered for the control of mission-critical systems. A simultaneous or almost-simultaneous ransomware attack on a very large number of devices could prove very disruptive, costly, or outright dangerous. An attack of this nature could for example disrupt the operation of IoT-enabled supply chains, compromise food production by targeting smart agriculture settings, cause unforeseeable consequences to the power grid through compromise of smart metering or electric car charging infrastructure, or even endanger lives by tampering with actuators in factories or transport systems. The CHARIOT EPSRC-funded project aims to devise, design, and prototype methods to prevent, detect, recover from and immunise against ransomware attacks in resource-constrained industrial IoT environments. In this talk I will present the project’s progress to date, as well as some prior work on anomaly detection that led to this research activity at Bristol.