DODaniel O'KEeffe

Daniel O'KEeffe

*This is an algorithmically generated author record based on publicly available information.

Current Organizations / Institutes

The organizations/institutes from the scholar's latest article

Previous Organizations / Institutes

The organizations / institutes from the scholar's other articles in the past ten years


Daniel O'KEeffe has a total of 29 co-authors. Here are the top co-authors by number of shared publications:


Latest Publications

  • RustMC : Automated Verification of Real-World Concurrent Rust

    by Oliver Pearce, Julien Lange, Dan O’KEeffe

  • Open Access

    An Empirical Study of C to Rust Translation using Local Large-Language Models

    by Nathan Rutherford, Dan O'KEeffe

    Memory corruption vulnerabilities are prevalent in C/C++ codebases. As a result, recent research has explored automated translation of C/C++ to Rust in order to benefit from Rust’s compiler enforced memory safety guarantees. However, much of the related work for translation using large-language models (LLMs) focuses on techniques that run on proprietary, cloud based LLMs with a high number of parameters. We present Oxidation, a translation pipeline that targets resource constrained LLMs on local machines. To cope with the limited context window of local LLMs, Oxidation proposes a compile and repair approach that leverages a live code environment (REPL) to incrementally validate partial translations, and an arbitration pipeline to generate complete summaries of C functions. Our results over the Transcoder-IR dataset suggest that at the function level, arbitrated translation results in a 3 × increase in translation success for lightweight, non-thinking models. In the case of thinking models, we observed a 31% drop in translation success, but a 5 × performance gain in terms of translation runtime.


  • Open Access

    Fast Durably Linearizable Data Structures for Free

    by Sergey Egorov, Gregory Chockler, Brijesh Dongol, Dan O'KEeffe

  • Open Access

    RustMC: Extending the GenMC stateless model checker to Rust

    by Oliver Pearce, Julien Lange, Dan O'Keeffe

    RustMC is a stateless model checker that enables verification of concurrent Rust programs. As both Rust and C/C++ compile to LLVM IR, RustMC builds on GenMC which provides a verification framework for LLVM IR. This enables the automatic verification of Rust code and any C/C++ dependencies. This tool paper presents the key challenges we addressed to extend GenMC. These challenges arise from Rust's unique compilation strategy and include intercepting threading operations, handling memory intrinsics and uninitialized accesses. Through case studies adapted from real-world programs, we demonstrate RustMC's effectiveness at finding concurrency bugs stemming from unsafe Rust code, FFI calls to C/C++, and incorrect use of atomic operations.

  • Open Access

    AWSomePy: A Dataset and Characterization of Serverless Applications

    by Giuseppe Raffa, Jorge Blasco Alis, Dan O'KEeffe, Santanu Kumar Dash

    Over the last few years, the serverless computing paradigm has become increasingly popular. Thanks to its cost-effectiveness and the possibility of relying on a cloud provider to manage the underlying infrastructure, companies making use of serverless platforms can fully focus on developing the business logic of their products. However, adopting the serverless model also implies facing several performance, traceability and security-related challenges. Some of them can be tackled by analysing real-world applications and identifying key trends, as these can guide the development of novel models and tools. In spite of this, little up-to-date information on such trends is currently available in the literature. In this work, we gather and interpret information that can be leveraged to analyse serverless applications. To achieve our goal, we study a set of applications developed in Python for the Amazon Web Services (AWS) platform. We first conduct an architectural analysis to identify serverless-specific parameters, e.g., plugins used in deployment tools and the number of events and handlers. We then perform an application code-level analysis in order to establish which cloud services and APIs developers use most frequently. Our results show that granular definition of handler permissions is not common practice. Furthermore, developers make use of configuration services and programmatic creation of cloud resources, thus adding workflows difficult to analyse statically. Our dataset, AWSomePy, is publicly available to support future research work.


  • Open Access

    Spons & Shields: practical isolation for trusted execution

    by Vasily A. Sartakov, Daniel O'KEeffe, David Eyers, Lluís Vilanova, Peter Pietzuch

    Trusted execution environments (TEEs) promise a cost-effective, “lift-and-shift” solution for deploying security-sensitive applications in untrusted clouds. For this, they must support rich, multi-component applications, but a large trusted computing base (TCB) inside the TEE risks that attackers can compromise application security. Fine-grained compartmentalisation can increase security through defense-in-depth, but current solutions either run all software components unprotected in the same TEE, lack efficient shared memory support, or isolate application processes using separate TEEs, impacting performance and compatibility. We describe the Spons & Shields framework (SSF) for Intel SGX TEEs, which offers intra-TEE compartmentalisation using two new abstraction, Spons and Shields. Spons and Shields generalise process, library and user/kernel isolation inside the TEE while allowing for efficient memory sharing. When users deploy unmodified multi-component applications in a TEE, SSF dynamically creates Spons (one per POSIX process or library) and Shields (to enforce a given security policy for memory accesses). Applications can be hardened with minor code changes, e.g., by using a separate Shield to isolate an SSL library. SSF uses compiler instrumentation to protect Shield boundaries, exploiting MPX instructions if available. We evaluate SSF using a complex application service (NGINX, PHP interpreter and PostgreSQL) and show that its overhead is comparable to process isolation.


  • Open Access

    LibSEAL

    by Pierre-Louis Aublin, Florian Kelbert, Dan O'KEeffe, Divya Muthukumaran, Christian Priebe, Joshua Lind, Robert Krahn, Christof Fetzer, David Eyers, Peter Pietzuch


  • Open Access

    FlowWatcher

    by Divya Muthukumaran, Dan O'KEeffe, Christian Priebe, David Eyers, Brian Shand, Peter Pietzuch

    Bugs in the authorisation logic of web applications can expose the data of one user to another. Such data disclosure vulnerabilities are common---they can be caused by a single omitted access control check in the application. We make the observation that, while the implementation of the authorisation logic is complex and therefore error-prone, most web applications only use simple access control models, in which each piece of data is accessible by a user or a group of users. This makes it possible to validate the correct operation of the authorisation logic externally, based on the observed data in HTTP traffic to and from an application. We describe FlowWatcher, an HTTP proxy that mitigates data disclosure vulnerabilities in unmodified web applications. FlowWatcher monitors HTTP traffic and shadows part of an application's access control state based on a rule-based specification of the user-data-access (UDA) policy. The UDA policy states the intended data ownership and how it changes based on observed HTTP requests. FlowWatcher detects violations of the UDA policy by tracking data items that are likely to be unique across HTTP requests and responses of different users. We evaluate a prototype implementation of FlowWatcher as a plug-in for the Nginx reverse proxy and show that, with short UDA policies, it can mitigate CVE bugs in six~popular web applications.


  • Open Access

    Network-aware stream query processing in mobile ad-hoc networks

    by Dan O'Keeffe, Theodoros Salonidis, Peter Pietzuch

    Many real-time decision support and sensing applications can be expressed as continuous stream queries over time-varying data streams, following a data stream management model. We consider the problem of the efficient and resilient execution of continuous stream queries in tactical edge networks formed from mobile ad-hoc networks (MANETs) with limited backend connectivity. Previous approaches for distributed stream query execution target data center environments in which networks are static, and centralized control is feasible. The distributed, bandwidth-constrained and highly dynamic nature of MANETs render such approaches insufficient-while a stream query executes in a MANET, changes in the network topology mean that any fixed query plan eventually becomes outdated. We introduce an adaptive, network-aware approach for stream query planning in MANETs, which supports both single- and multi-input windowed stream query operators. The basic idea is to increase the path diversity available when executing stream queries by replicating query operators across many nodes in the MANET. During execution, it becomes possible to dynamically switch between different operator replicas based on connectivity and other network path conditions. We evaluate our approach in emulated MANETs, showing that it can increase substantially the robustness of distributed stream query processing under mobility.