-
Global, robust and comparable digital carbon assets
Authors:
Sadiq Jaffer,
Michael Dales,
Patrick Ferris,
Thomas Swinfield,
Derek Sorensen,
Robin Message,
Srinivasan Keshav,
Anil Madhavapeddy
Abstract:
Carbon credits purchased in the voluntary carbon market allow unavoidable emissions, such as from international flights for essential travel, to be offset by an equivalent climate benefit, such as avoiding emissions from tropical deforestation. However, many concerns regarding the credibility of these offsetting claims have been raised. Moreover, the credit market is manual, therefore inefficient…
▽ More
Carbon credits purchased in the voluntary carbon market allow unavoidable emissions, such as from international flights for essential travel, to be offset by an equivalent climate benefit, such as avoiding emissions from tropical deforestation. However, many concerns regarding the credibility of these offsetting claims have been raised. Moreover, the credit market is manual, therefore inefficient and unscalable, and non-fungible, therefore illiquid. To address these issues, we propose an efficient digital methodology that combines remote sensing data, modern econometric techniques, and on-chain certification and trading to create a new digital carbon asset (the PACT stablecoin) against which carbon offsetting claims can be transparently verified. PACT stablecoins are produced as outputs from a reproducible computational pipeline for estimating the climate benefits of carbon offset projects that not only quantifies the CO2 emissions involved, but also allows for similar credits to be pooled based on their co-benefits such as biodiversity and jurisdictional attributes, increasing liquidity through fungibility within pools. We implement and evaluate the PACT carbon stablecoin on the Tezos blockchain, which is designed to facilitate low-cost transactions while minimizing environmental impact. Our implementation includes a contract for a registry for tracking issuance, ownership, and retirement of credits, and a custodian contract to bridge on-chain and off-chain transactions. Our work brings scale and trust to the voluntary carbon market by providing a transparent, scalable, and efficient framework for high integrity carbon credit transactions.
△ Less
Submitted 3 April, 2024; v1 submitted 21 March, 2024;
originally announced March 2024.
-
Enabling Lightweight Privilege Separation in Applications with MicroGuards
Authors:
Zahra Tarkhani,
Anil Madhavapeddy
Abstract:
Application compartmentalization and privilege separation are our primary weapons against ever-increasing security threats and privacy concerns on connected devices. Despite significant progress, it is still challenging to privilege separate inside an application address space and in multithreaded environments, particularly on resource-constrained and mobile devices. We propose MicroGuards, a ligh…
▽ More
Application compartmentalization and privilege separation are our primary weapons against ever-increasing security threats and privacy concerns on connected devices. Despite significant progress, it is still challenging to privilege separate inside an application address space and in multithreaded environments, particularly on resource-constrained and mobile devices. We propose MicroGuards, a lightweight kernel modification and set of security primitives and APIs aimed at flexible and fine-grained in-process memory protection and privilege separation in multithreaded applications. MicroGuards take advantage of hardware support in modern CPUs and are high-level enough to be adaptable to various architectures. This paper focuses on enabling MicroGuards on embedded and mobile devices running Linux kernel and utilizes tagged memory support to achieve good performance. Our evaluation show that MicroGuards add small runtime overhead (less than 3.5\%), minimal memory footprint, and are practical to get integrated with existing applications to enable fine-grained privilege separation.
△ Less
Submitted 25 June, 2023;
originally announced June 2023.
-
Planetary computing for data-driven environmental policy-making
Authors:
Patrick Ferris,
Michael Dales,
Sadiq Jaffer,
Amelia Holcomb,
Eleanor Toye Scott,
Thomas Swinfield,
Alison Eyres,
Andrew Balmford,
David Coomes,
Srinivasan Keshav,
Anil Madhavapeddy
Abstract:
We make a case for "planetary computing" -- infrastructure to handle the ingestion, transformation, analysis and publication of global data products for furthering environmental science and enabling better informed policy-making. We draw on our experiences as a team of computer scientists working with environmental scientists on forest carbon and biodiversity preservation, and classify existing so…
▽ More
We make a case for "planetary computing" -- infrastructure to handle the ingestion, transformation, analysis and publication of global data products for furthering environmental science and enabling better informed policy-making. We draw on our experiences as a team of computer scientists working with environmental scientists on forest carbon and biodiversity preservation, and classify existing solutions by their flexibility in scalably processing geospatial data, and also how well they support building trust in the results via traceability and reproducibility. We identify research gaps in the intersection of computing and environmental science around how to handle continuously changing datasets that are often collected across decades and require careful access control rather than being fully open access.
△ Less
Submitted 1 June, 2024; v1 submitted 8 March, 2023;
originally announced March 2023.
-
Enhancing the Security & Privacy of Wearable Brain-Computer Interfaces
Authors:
Zahra Tarkhani,
Lorena Qendro,
Malachy O'Connor Brown,
Oscar Hill,
Cecilia Mascolo,
Anil Madhavapeddy
Abstract:
Brain computing interfaces (BCI) are used in a plethora of safety/privacy-critical applications, ranging from healthcare to smart communication and control. Wearable BCI setups typically involve a head-mounted sensor connected to a mobile device, combined with ML-based data processing. Consequently, they are susceptible to a multiplicity of attacks across the hardware, software, and networking sta…
▽ More
Brain computing interfaces (BCI) are used in a plethora of safety/privacy-critical applications, ranging from healthcare to smart communication and control. Wearable BCI setups typically involve a head-mounted sensor connected to a mobile device, combined with ML-based data processing. Consequently, they are susceptible to a multiplicity of attacks across the hardware, software, and networking stacks used that can leak users' brainwave data or at worst relinquish control of BCI-assisted devices to remote attackers. In this paper, we: (i) analyse the whole-system security and privacy threats to existing wearable BCI products from an operating system and adversarial machine learning perspective; and (ii) introduce Argus, the first information flow control system for wearable BCI applications that mitigates these attacks. Argus' domain-specific design leads to a lightweight implementation on Linux ARM platforms suitable for existing BCI use-cases. Our proof of concept attacks on real-world BCI devices (Muse, NeuroSky, and OpenBCI) led us to discover more than 300 vulnerabilities across the stacks of six major attack vectors. Our evaluation shows Argus is highly effective in tracking sensitive dataflows and restricting these attacks with an acceptable memory and performance overhead (<15%).
△ Less
Submitted 19 January, 2022;
originally announced January 2022.
-
How Computer Science Can Aid Forest Restoration
Authors:
Gemma Gordon,
Amelia Holcomb,
Tom Kelly,
Srinivasan Keshav,
Jon Ludlum,
Anil Madhavapeddy
Abstract:
The world faces two interlinked crises: climate change and loss of biodiversity. Forest restoration on degraded lands and surplus croplands can play a significant role both in sequestering carbon and re-establishing bio-diversity. There is a considerable body of research and practice that addresses forest restoration. However, there has been little work by computer scientists to bring powerful com…
▽ More
The world faces two interlinked crises: climate change and loss of biodiversity. Forest restoration on degraded lands and surplus croplands can play a significant role both in sequestering carbon and re-establishing bio-diversity. There is a considerable body of research and practice that addresses forest restoration. However, there has been little work by computer scientists to bring powerful computational techniques to bear on this important area of work, perhaps due to a lack of awareness. In an attempt to bridge this gap, we present our vision of how techniques from computer science, broadly speaking, can aid current practice in forest restoration.
△ Less
Submitted 12 August, 2021;
originally announced September 2021.
-
Retrofitting Effect Handlers onto OCaml
Authors:
KC Sivaramakrishnan,
Stephen Dolan,
Leo White,
Tom Kelly,
Sadiq Jaffer,
Anil Madhavapeddy
Abstract:
Effect handlers have been gathering momentum as a mechanism for modular programming with user-defined effects. Effect handlers allow for non-local control flow mechanisms such as generators, async/await, lightweight threads and coroutines to be composably expressed. We present a design and evaluate a full-fledged efficient implementation of effect handlers for OCaml, an industrial-strength multi-p…
▽ More
Effect handlers have been gathering momentum as a mechanism for modular programming with user-defined effects. Effect handlers allow for non-local control flow mechanisms such as generators, async/await, lightweight threads and coroutines to be composably expressed. We present a design and evaluate a full-fledged efficient implementation of effect handlers for OCaml, an industrial-strength multi-paradigm programming language. Our implementation strives to maintain the backwards compatibility and performance profile of existing OCaml code. Retrofitting effect handlers onto OCaml is challenging since OCaml does not currently have any non-local control flow mechanisms other than exceptions. Our implementation of effect handlers for OCaml: (i) imposes a mean 1% overhead on a comprehensive macro benchmark suite that does not use effect handlers; (ii) remains compatible with program analysis tools that inspect the stack; and (iii) is efficient for new code that makes use of effect handlers.
△ Less
Submitted 1 April, 2021;
originally announced April 2021.
-
Enclave-Aware Compartmentalization and Secure Sharing with Sirius
Authors:
Zahra Tarkhani,
Anil Madhavapeddy
Abstract:
Hardware-assisted trusted execution environments (TEEs) are critical building blocks of many modern applications. However, they have a one-way isolation model that introduces a semantic gap between a TEE and its outside world. This lack of information causes an ever-increasing set of attacks on TEE-enabled applications that exploit various insecure interactions with the host OSs, applications, or…
▽ More
Hardware-assisted trusted execution environments (TEEs) are critical building blocks of many modern applications. However, they have a one-way isolation model that introduces a semantic gap between a TEE and its outside world. This lack of information causes an ever-increasing set of attacks on TEE-enabled applications that exploit various insecure interactions with the host OSs, applications, or other enclaves. We introduce Sirius, the first compartmentalization framework that achieves strong isolation and secure sharing in TEE-assisted applications by controlling the dataflows within primary kernel objects (e.g. threads, processes, address spaces, files, sockets, pipes) in both the secure and normal worlds. Sirius replaces ad-hoc interactions in current TEE systems with a principled approach that adds strong inter- and intra-address space isolation and effectively eliminates a wide range of attacks. We evaluate Sirius on ARM platforms and find that it is lightweight ($\approx 15K$ LoC) and only adds $\approx 10.8\%$ overhead to enable TEE support on applications such as httpd, and improves the performance of existing TEE-enabled applications such as the Darknet ML framework and ARM's LibDDSSec by $0.05\%-5.6\%$.
△ Less
Submitted 23 November, 2020; v1 submitted 3 September, 2020;
originally announced September 2020.
-
Retrofitting Parallelism onto OCaml
Authors:
KC Sivaramakrishnan,
Stephen Dolan,
Leo White,
Sadiq Jaffer,
Tom Kelly,
Anmol Sahoo,
Sudha Parimala,
Atul Dhiman,
Anil Madhavapeddy
Abstract:
OCaml is an industrial-strength, multi-paradigm programming language, widely used in industry and academia. OCaml is also one of the few modern managed system programming languages to lack support for shared memory parallel programming. This paper describes the design, a full-fledged implementation and evaluation of a mostly-concurrent garbage collector (GC) for the multicore extension of the OCam…
▽ More
OCaml is an industrial-strength, multi-paradigm programming language, widely used in industry and academia. OCaml is also one of the few modern managed system programming languages to lack support for shared memory parallel programming. This paper describes the design, a full-fledged implementation and evaluation of a mostly-concurrent garbage collector (GC) for the multicore extension of the OCaml programming language. Given that we propose to add parallelism to a widely used programming language with millions of lines of existing code, we face the challenge of maintaining backwards compatibility--not just in terms of the language features but also the performance of single-threaded code running with the new GC. To this end, the paper presents a series of novel techniques and demonstrates that the new GC strikes a balance between performance and feature backwards compatibility for sequential programs and scales admirably on modern multicore processors.
△ Less
Submitted 2 July, 2020; v1 submitted 24 April, 2020;
originally announced April 2020.
-
$μ$Tiles: Efficient Intra-Process Privilege Enforcement of Memory Regions
Authors:
Zahra Tarkhani,
Anil Madhavapeddy
Abstract:
With the alarming rate of security advisories and privacy concerns on connected devices, there is an urgent need for strong isolation guarantees in resource-constrained devices that demand very lightweight solutions. However, the status quo is that Unix-like operating systems do not offer privilege separation inside a process. Lack of practical fine-grained compartmentalization inside a shared add…
▽ More
With the alarming rate of security advisories and privacy concerns on connected devices, there is an urgent need for strong isolation guarantees in resource-constrained devices that demand very lightweight solutions. However, the status quo is that Unix-like operating systems do not offer privilege separation inside a process. Lack of practical fine-grained compartmentalization inside a shared address space leads to private data leakage through applications' untrusted dependencies and compromised threads. To this end, we propose $μ$Tiles, a lightweight kernel abstraction and set of security primitives based on mutual distrust for intra-process privilege separation, memory protection, and secure multithreading. $μ$Tiles takes advantage of hardware support for virtual memory tagging (e.g., ARM memory domains) to achieve significant performance gain while eliminating various hardware limitations. Our results (based on OpenSSL, the Apache HTTP server, and LevelDB) show that $μ$Tiles is extremely lightweight (adds $\approx 10KB$ to kernel image) for IoT use cases. It adds negligible runtime overhead ($\approx 0.5\%-3.5\%$) and is easy to integrate with existing applications for providing strong privilege separation.
△ Less
Submitted 9 April, 2020;
originally announced April 2020.
-
Programming Unikernels in the Large via Functor Driven Development
Authors:
Gabriel Radanne,
Thomas Gazagnaire,
Anil Madhavapeddy,
Jeremy Yallop,
Richard Mortier,
Hannes Mehnert,
Mindy Preston,
David Scott
Abstract:
Compiling applications as unikernels allows them to be tailored to diverse execution environments. Dependency on a monolithic operating system is replaced with linkage against libraries that provide specific services. Doing so in practice has revealed a major barrier: managing the configuration matrix across heterogenous execution targets. A realistic unikernel application depends on hundreds of l…
▽ More
Compiling applications as unikernels allows them to be tailored to diverse execution environments. Dependency on a monolithic operating system is replaced with linkage against libraries that provide specific services. Doing so in practice has revealed a major barrier: managing the configuration matrix across heterogenous execution targets. A realistic unikernel application depends on hundreds of libraries, each of which may place different demands on the different target execution platforms (e.g.,~cryptographic acceleration).
We propose a modular approach to structuring large scale codebases that cleanly separates configuration, application and operating system logic. Our implementation is built on the \mirage unikernel framework, using the \ocaml language's powerful abstraction and metaprogramming facilities. Leveraging modules allows us to build many components independently, with only loose coupling through a set of standardised signatures. Components can be parameterized by other components and composed. Our approach accounts for state, dependency ordering, and error management, and our usage over the years has demonstrated significant efficiency benefits by leveraging compiler features such as global link-time optimisation during the configuration process. We describe our application architecture and experiences via some practical applications of our approach, and discuss how library development in \mirage can facilitate adoption in other unikernel frameworks and programming languages.
△ Less
Submitted 7 May, 2019;
originally announced May 2019.
-
Fractal: Automated Application Scaling
Authors:
Masoud Koleini,
Carlos Oviedo,
Derek McAuley,
Charalampos Rotsos,
Anil Madhavapeddy,
Thomas Gazagnaire,
Magnus Skejgstad,
Richard Mortier
Abstract:
To date, cloud applications have used datacenter resources through manual configuration and deployment of virtual machines and containers. Current trends see increasing use of microservices, where larger applications are split into many small containers, to be developed and deployed independently. However, even with the rise of the devops movement and orchestration facilities such as Kubernetes, t…
▽ More
To date, cloud applications have used datacenter resources through manual configuration and deployment of virtual machines and containers. Current trends see increasing use of microservices, where larger applications are split into many small containers, to be developed and deployed independently. However, even with the rise of the devops movement and orchestration facilities such as Kubernetes, there is a tendency to separate development from deployment. We present an exploration of a more extreme point on the devops spectrum: Fractal. Developers embed orchestration logic inside their application, fully automating the processes of scaling up and down. Providing a set of extensions to and an API over the Jitsu platform, we outline the design of Fractal and describe the key features of its implementation: how an application is self-replicated, how replica lifecycles are managed, how failure recovery is handled, and how network traffic is transparently distributed between replicas. We present evaluation of a self-scaling website, and demonstrate that Fractal is both useful and feasible.
△ Less
Submitted 25 February, 2019;
originally announced February 2019.
-
Personal Data: Thinking Inside the Box
Authors:
Hamed Haddadi,
Heidi Howard,
Amir Chaudhry,
Jon Crowcroft,
Anil Madhavapeddy,
Richard Mortier
Abstract:
We propose there is a need for a technical platform enabling people to engage with the collection, management and consumption of personal data; and that this platform should itself be personal, under the direct control of the individual whose data it holds. In what follows, we refer to this platform as the Databox, a personal, networked service that collates personal data and can be used to make t…
▽ More
We propose there is a need for a technical platform enabling people to engage with the collection, management and consumption of personal data; and that this platform should itself be personal, under the direct control of the individual whose data it holds. In what follows, we refer to this platform as the Databox, a personal, networked service that collates personal data and can be used to make those data available. While your Databox is likely to be a virtual platform, in that it will involve multiple devices and services, at least one instance of it will exist in physical form such as on a physical form-factor computing device with associated storage and networking, such as a home hub.
△ Less
Submitted 20 January, 2015;
originally announced January 2015.
-
Kadupul: Livin' on the Edge with Virtual Currencies and Time-Locked Puzzles
Authors:
Magnus Skjegstad,
Anil Madhavapeddy,
Jon Crowcroft
Abstract:
Devices connected to the Internet today have a wide range of local communication channels available, such as wireless Wifi, Bluetooth or NFC, as well as wired backhaul. In densely populated areas it is possible to create heterogeneous, multihop communication paths using a combination of these technologies, and often transmit data with lower latency than via a wired Internet connection. However, th…
▽ More
Devices connected to the Internet today have a wide range of local communication channels available, such as wireless Wifi, Bluetooth or NFC, as well as wired backhaul. In densely populated areas it is possible to create heterogeneous, multihop communication paths using a combination of these technologies, and often transmit data with lower latency than via a wired Internet connection. However, the potential for sharing meshed wireless radios in this way has never been realised due to the lack of economic incentives to do so on the part of individual nodes.
In this paper, we explore how virtual currencies such as Bitcoin might be used to provide an end-to-end incentive scheme to convince forwarding nodes that it is profitable to send packets on via the lowest latency mechanism available. Clients inject a small amount of money to transmit a datagram, and forwarding engines compete to solve a time-locked puzzle that can be claimed by the node that delivers the result in the lowest latency. This approach naturally extends congestion control techniques to a surge pricing model when available bandwidth is low. We conclude by discussing several latency-sensitive applications that would benefit for this, such as video streaming and local augmented reality systems.
△ Less
Submitted 15 December, 2014;
originally announced December 2014.