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.
The presentation delves into the critical aspects of QNAME Minimization within the DNS, presenting an in-depth analysis through two key studies. The first segment, "Adoption of QNAME Minimization," presents the main takeaways from "A Second Look at QNAME Minimization" (PAM, 2023). This study provides insights into how QNAME Minimization has been embraced across different platforms and its implications for privacy and performance in DNS lookups. The second segment, "Implementation of QNAME Minimization," introduces new research on fingerprinting DNS resolvers by leveraging the query patterns emerging from QNAME Minimization. This study, currently under submission, aims to shed light on the plethora of implementation approaches to minimizing queries and how these differences can be used to fingerprint resolver software and versions. Through these studies, the presentation aims to foster a deeper understanding of DNS resolver dynamics, highlighting the importance of QNAME Minimization in bolstering DNS privacy.
In this talk, I'll advocate a proof technique for ensuring soundness or security properties of practical languages, which implement interoperability using glue code that mediates interaction between languages after compilation to a common lower-level intermediate representation (IR). This proof technique involves building a _semantic intermediate representation_: a semantic model of source-language types as relations on terms of the lower-level IR. Semantic IRs can be used to guide the design and implementation of sound FFIs and to verify that the IR glue code used to implement conversions ensures type soundness. More interestingly, semantic IRs provide a basis for numerous avenues of future work on the principled design of language interoperability: how to support the inclusion of libraries whose behavior is foreign to the original language, how to prove soundness and security properties that are robust to behaviors (attackers) outside of the semantic IR, and how to develop a compiler IRs and backends that makes it easier to implement and verify sound interoperability for a wide array of source languages.
Content scanning systems employ perceptual hashing algorithms to scan user content for illicit material, such as child pornography or terrorist recruitment flyers. Perceptual hashing algorithms help determine whether two images are visually similar while preserving the privacy of the input images. Several efforts from industry and academia propose scanning on client devices such as smartphones due to the impending rollout of end-to-end encryption that will make server-side scanning difficult. These proposals have met with strong criticism because of the potential for the technology to be misused for censorship. However, the risks of this technology in the context of surveillance are not well understood. This talk will discuss results from our experimental investigation of physical surveillance risks in these systems. Concretely: (1) we offer a definition of physical surveillance in the context of client-side image scanning systems; (2) we experimentally characterize this risk; (3) we experimentally study the trade-off between the robustness of client-side image scanning systems and surveillance, showing that more robust detection of illicit material leads to an increased potential for physical surveillance in most settings.
Modern computer systems, encompassing mobile, cyber-physical, and cloud applications, are evolving to become more interconnected and complex. These systems facilitate diverse domain interactions, which in turn increase their vulnerability and present new challenges in security. Consequently, there is a critical need to assess and manage the security and attack surfaces of modern computer systems. This task demands scalable and reliable approaches to cope with the volatility of these ecosystems, highlighting the need for principled security solutions. In this talk, I will present how novel program analysis techniques, combined with security principles, can be leveraged to manage and reduce attack surfaces. I will present LMCAS, a software debloating approach that customizes applications based on runtime configurations and eliminates superfluous code, which preserving the required functionality. I will conclude by discussing future research directions that I am eager to explore.
It has been five years since the General Data Protection Regulation (GDPR) went into effect in the EU. Ever since, research has continued to show that the creators of online services find it difficult to implement the legal requirements of EU legislation into practice. They mainly resort to lengthy privacy policies and often deceptive cookie notices to ask users for their consent to data processing, rather than revise their own data processing practices and opt for approaches that collect less personal data. This comes to the detriment of service providers and users, who are both faced with decreased usability of websites, apps, and devices.
This talk investigates approaches to both understand the roadblocks that keep system creators and users from adopting a privacy-by-design mindset and to find ways to address them. This is ever more important in the light of new European platform regulations that intend to create boundaries for personalized advertising and introduce interoperability requirements, which in turn pose new opportunities to empower system creators and users alike to take control of users' privacy.