Showing 1–25 of 25 results for author: Morrison, A

Last-Level Cache Side-Channel Attacks Are Feasible in the Modern Public Cloud (Extended Version)

Authors: Zirui Neil Zhao, Adam Morrison, Christopher W. Fletcher, Josep Torrellas

Abstract: Last-level cache side-channel attacks have been mostly demonstrated in highly-controlled, quiescent local environments. Hence, it is unclear whether such attacks are feasible in a production cloud environment. In the cloud, side channels are flooded with noise from activities of other tenants and, in Function-as-a-Service (FaaS) workloads, the attacker has a very limited time window to mount the a… ▽ More Last-level cache side-channel attacks have been mostly demonstrated in highly-controlled, quiescent local environments. Hence, it is unclear whether such attacks are feasible in a production cloud environment. In the cloud, side channels are flooded with noise from activities of other tenants and, in Function-as-a-Service (FaaS) workloads, the attacker has a very limited time window to mount the attack. In this paper, we show that such attacks are feasible in practice, although they require new techniques. We present an end-to-end, cross-tenant attack on a vulnerable ECDSA implementation in the public FaaS Google Cloud Run environment. We introduce several new techniques to improve every step of the attack. First, to speed-up the generation of eviction sets, we introduce L2-driven candidate address filtering and a Binary Search-based algorithm for address pruning. Second, to monitor victim memory accesses with high time resolution, we introduce Parallel Probing. Finally, we leverage power spectral density from signal processing to easily identify the victim's target cache set in the frequency domain. Overall, using these mechanisms, we extract a median value of 81% of the secret ECDSA nonce bits from a victim container in 19 seconds on average. △ Less

Submitted 20 May, 2024; originally announced May 2024.

Journal ref: 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS 2024), Volume 2, pages 582-600, La Jolla, CA, USA, May 2024

DECLASSIFLOW: A Static Analysis for Modeling Non-Speculative Knowledge to Relax Speculative Execution Security Measures (Full Version)

Authors: Rutvik Choudhary, Alan Wang, Zirui Neil Zhao, Adam Morrison, Christopher W. Fletcher

Abstract: Speculative execution attacks undermine the security of constant-time programming, the standard technique used to prevent microarchitectural side channels in security-sensitive software such as cryptographic code. Constant-time code must therefore also deploy a defense against speculative execution attacks to prevent leakage of secret data stored in memory or the processor registers. Unfortunately… ▽ More Speculative execution attacks undermine the security of constant-time programming, the standard technique used to prevent microarchitectural side channels in security-sensitive software such as cryptographic code. Constant-time code must therefore also deploy a defense against speculative execution attacks to prevent leakage of secret data stored in memory or the processor registers. Unfortunately, contemporary defenses, such as speculative load hardening (SLH), can only satisfy this strong security guarantee at a very high performance cost. This paper proposes DECLASSIFLOW, a static program analysis and protection framework to efficiently protect constant-time code from speculative leakage. DECLASSIFLOW models "attacker knowledge" -- data which is inherently transmitted (or, implicitly declassified) by the code's non-speculative execution -- and statically removes protection on such data from points in the program where it is already guaranteed to leak non-speculatively. Overall, DECLASSIFLOW ensures that data which never leaks during the non-speculative execution does not leak during speculative execution, but with lower overhead than conservative protections like SLH. △ Less

Submitted 14 December, 2023; originally announced December 2023.

Journal ref: In Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (CCS '23). Association for Computing Machinery, New York, NY, USA, 2053-2067

Empirical Comparison between Cross-Validation and Mutation-Validation in Model Selection

Authors: **yang Yu, Sami Hamdan, Leonard Sasse, Abigail Morrison, Kaustubh R. Patil

Abstract: Mutation validation (MV) is a recently proposed approach for model selection, garnering significant interest due to its unique characteristics and potential benefits compared to the widely used cross-validation (CV) method. In this study, we empirically compared MV and $k$-fold CV using benchmark and real-world datasets. By employing Bayesian tests, we compared generalization estimates yielding th… ▽ More Mutation validation (MV) is a recently proposed approach for model selection, garnering significant interest due to its unique characteristics and potential benefits compared to the widely used cross-validation (CV) method. In this study, we empirically compared MV and $k$-fold CV using benchmark and real-world datasets. By employing Bayesian tests, we compared generalization estimates yielding three posterior probabilities: practical equivalence, CV superiority, and MV superiority. We also evaluated the differences in the capacity of the selected models and computational efficiency. We found that both MV and CV select models with practically equivalent generalization performance across various machine learning algorithms and the majority of benchmark datasets. MV exhibited advantages in terms of selecting simpler models and lower computational costs. However, in some cases MV selected overly simplistic models leading to underfitting and showed instability in hyperparameter selection. These limitations of MV became more evident in the evaluation of a real-world neuroscientific task of predicting sex at birth using brain functional connectivity. △ Less

Submitted 15 February, 2024; v1 submitted 23 November, 2023; originally announced November 2023.

Runtime Construction of Large-Scale Spiking Neuronal Network Models on GPU Devices

Authors: Bruno Golosio, Jose Villamar, Gianmarco Tiddia, Elena Pastorelli, Jonas Stapmanns, Viviana Fanti, Pier Stanislao Paolucci, Abigail Morrison, Johanna Senk

Abstract: Simulation speed matters for neuroscientific research: this includes not only how quickly the simulated model time of a large-scale spiking neuronal network progresses, but also how long it takes to instantiate the network model in computer memory. On the hardware side, acceleration via highly parallel GPUs is being increasingly utilized. On the software side, code generation approaches ensure hig… ▽ More Simulation speed matters for neuroscientific research: this includes not only how quickly the simulated model time of a large-scale spiking neuronal network progresses, but also how long it takes to instantiate the network model in computer memory. On the hardware side, acceleration via highly parallel GPUs is being increasingly utilized. On the software side, code generation approaches ensure highly optimized code, at the expense of repeated code regeneration and recompilation after modifications to the network model. Aiming for a greater flexibility with respect to iterative model changes, here we propose a new method for creating network connections interactively, dynamically, and directly in GPU memory through a set of commonly used high-level connection rules. We validate the simulation performance with both consumer and data center GPUs on two neuroscientifically relevant models: a cortical microcircuit of about 77,000 leaky-integrate-and-fire neuron models and 300 million static synapses, and a two-population network recurrently connected using a variety of connection rules. With our proposed ad hoc network instantiation, both network construction and simulation times are comparable or shorter than those obtained with other state-of-the-art simulation technologies, while still meeting the flexibility demands of explorative network modeling. △ Less

Submitted 16 June, 2023; originally announced June 2023.

Comments: 29 pages, 9 figures

Journal ref: Appl. Sci. 2023, 13(17), 9598

Prefix Siphoning: Exploiting LSM-Tree Range Filters For Information Disclosure (Full Version)

Authors: Adi Kaufman, Moshik Hershcovitch, Adam Morrison

Abstract: Key-value stores typically leave access control to the systems for which they act as storage engines. Unfortunately, attackers may circumvent such read access controls via timing attacks on the key-value store, which use differences in query response times to glean information about stored data. To date, key-value store timing attacks have aimed to disclose stored values and have exploited exter… ▽ More Key-value stores typically leave access control to the systems for which they act as storage engines. Unfortunately, attackers may circumvent such read access controls via timing attacks on the key-value store, which use differences in query response times to glean information about stored data. To date, key-value store timing attacks have aimed to disclose stored values and have exploited external mechanisms that can be disabled for protection. In this paper, we point out that key disclosure is also a security threat -- and demonstrate key disclosure timing attacks that exploit mechanisms of the key-value store itself. We target LSM-tree based key-value stores utilizing range filters, which have been recently proposed to optimize LSM-tree range queries. We analyze the impact of the range filters SuRF and prefix Bloom filter on LSM-trees through a security lens, and show that they enable a key disclosure timing attack, which we call prefix siphoning. Prefix siphoning successfully leverages benign queries for non-present keys to identify prefixes of actual keys -- and in some cases, full keys -- in scenarios where brute force searching for keys (via exhaustive enumeration or random guesses) is infeasible. △ Less

Submitted 8 September, 2023; v1 submitted 7 June, 2023; originally announced June 2023.

Comments: Full version of USENIX ATC'23 paper

Probabilistic Formal Modelling to Uncover and Interpret Interaction Styles

Authors: Oana Andrei, Muffy Calder, Matthew Chalmers, Alistair Morrison

Abstract: We present a study using new computational methods, based on a novel combination of machine learning for inferring admixture hidden Markov models and probabilistic model checking, to uncover interaction styles in a mobile app. These styles are then used to inform a redesign, which is implemented, deployed, and then analysed using the same methods. The data sets are logged user traces, collected ov… ▽ More We present a study using new computational methods, based on a novel combination of machine learning for inferring admixture hidden Markov models and probabilistic model checking, to uncover interaction styles in a mobile app. These styles are then used to inform a redesign, which is implemented, deployed, and then analysed using the same methods. The data sets are logged user traces, collected over two six-month deployments of each version, involving thousands of users and segmented into different time intervals. The methods do not assume tasks or absolute metrics such as measures of engagement, but uncover the styles through unsupervised inference of clusters and analysis with probabilistic temporal logic. For both versions there was a clear distinction between the styles adopted by users during the first day/week/month of usage, and during the second and third months, a result we had not anticipated. △ Less

Submitted 1 May, 2023; originally announced May 2023.

Emergent communication enhances foraging behaviour in evolved swarms controlled by Spiking Neural Networks

Authors: Cristian Jimenez Romero, Alper Yegenoglu, Aarón Pérez Martín, Sandra Diaz-Pier, Abigail Morrison

Abstract: Social insects such as ants communicate via pheromones which allows them to coordinate their activity and solve complex tasks as a swarm, e.g. foraging for food. This behavior was shaped through evolutionary processes. In computational models, self-coordination in swarms has been implemented using probabilistic or simple action rules to shape the decision of each agent and the collective behavior.… ▽ More Social insects such as ants communicate via pheromones which allows them to coordinate their activity and solve complex tasks as a swarm, e.g. foraging for food. This behavior was shaped through evolutionary processes. In computational models, self-coordination in swarms has been implemented using probabilistic or simple action rules to shape the decision of each agent and the collective behavior. However, manual tuned decision rules may limit the behavior of the swarm. In this work we investigate the emergence of self-coordination and communication in evolved swarms without defining any explicit rule. We evolve a swarm of agents representing an ant colony. We use an evolutionary algorithm to optimize a spiking neural network (SNN) which serves as an artificial brain to control the behavior of each agent. The goal of the evolved colony is to find optimal ways to forage for food and return it to the nest in the shortest amount of time. In the evolutionary phase, the ants are able to learn to collaborate by depositing pheromone near food piles and near the nest to guide other ants. The pheromone usage is not manually encoded into the network; instead, this behavior is established through the optimization procedure. We observe that pheromone-based communication enables the ants to perform better in comparison to colonies where communication via pheromone did not emerge. We assess the foraging performance by comparing the SNN based model to a rule based system. Our results show that the SNN based model can efficiently complete the foraging task in a short amount of time. Our approach illustrates self coordination via pheromone emerges as a result of the network optimization. This work serves as a proof of concept for the possibility of creating complex applications utilizing SNNs as underlying architectures for multi-agent interactions where communication and self-coordination is desired. △ Less

Submitted 8 September, 2023; v1 submitted 16 December, 2022; originally announced December 2022.

Comments: 27 pages, 16 figures

Phenomenological modeling of diverse and heterogeneous synaptic dynamics at natural density

Authors: Agnes Korcsak-Gorzo, Charl Linssen, Jasper Albers, Stefan Dasbach, Renato Duarte, Susanne Kunkel, Abigail Morrison, Johanna Senk, Jonas Stapmanns, Tom Tetzlaff, Markus Diesmann, Sacha J. van Albada

Abstract: This chapter sheds light on the synaptic organization of the brain from the perspective of computational neuroscience. It provides an introductory overview on how to account for empirical data in mathematical models, implement such models in software, and perform simulations reflecting experiments. This path is demonstrated with respect to four key aspects of synaptic signaling: the connectivity o… ▽ More This chapter sheds light on the synaptic organization of the brain from the perspective of computational neuroscience. It provides an introductory overview on how to account for empirical data in mathematical models, implement such models in software, and perform simulations reflecting experiments. This path is demonstrated with respect to four key aspects of synaptic signaling: the connectivity of brain networks, synaptic transmission, synaptic plasticity, and the heterogeneity across synapses. Each step and aspect of the modeling and simulation workflow comes with its own challenges and pitfalls, which are highlighted and addressed. △ Less

Submitted 19 February, 2023; v1 submitted 10 December, 2022; originally announced December 2022.

Comments: 38 pages, 5 figures, LaTeX; added two figures, clarified and extended formulations, updated format, added references

A Trust Framework for Government Use of Artificial Intelligence and Automated Decision Making

Authors: Pia Andrews, Tim de Sousa, Bruce Haefele, Matt Beard, Marcus Wigan, Abhinav Palia, Kathy Reid, Saket Narayan, Morgan Dumitru, Alex Morrison, Geoff Mason, Aurelie Jacquet

Abstract: This paper identifies the current challenges of the mechanisation, digitisation and automation of public sector systems and processes, and proposes a modern and practical framework to ensure and assure ethical and high veracity Artificial Intelligence (AI) or Automated Decision Making (ADM) systems in public institutions. This framework is designed for the specific context of the public sector, in… ▽ More This paper identifies the current challenges of the mechanisation, digitisation and automation of public sector systems and processes, and proposes a modern and practical framework to ensure and assure ethical and high veracity Artificial Intelligence (AI) or Automated Decision Making (ADM) systems in public institutions. This framework is designed for the specific context of the public sector, in the jurisdictional and constitutional context of Australia, but is extendable to other jurisdictions and private sectors. The goals of the framework are to: 1) earn public trust and grow public confidence in government systems; 2) to ensure the unique responsibilities and accountabilities (including to the public) of public institutions under Administrative Law are met effectively; and 3) to assure a positive human, societal and ethical impact from the adoption of such systems. The framework could be extended to assure positive environmental or other impacts, but this paper focuses on human/societal outcomes and public trust. This paper is meant to complement principles-based frameworks like Australia's Artificial Intelligence Ethics Framework and the EU Assessment List for Trustworthy AI. In many countries, COVID created a bubble of improved trust, a bubble which has arguably already popped, and in an era of unprecedented mistrust of public institutions (but even in times of high trust) it is not enough that a service is faster, or more cost-effective. This paper proposes recommendations for government systems (technology platforms, operations, culture, governance, engagement, etc.) that would help to improve public confidence and trust in public institutions, policies and services, whilst meeting the special obligations and responsibilities of the public sector. △ Less

Submitted 22 August, 2022; originally announced August 2022.

Comments: Comments were integrated into the paper from all peer reviewers. Am happy to provide a copied history of comments if useful

Prefix Filter: Practically and Theoretically Better Than Bloom

Authors: Tomer Even, Guy Even, Adam Morrison

Abstract: Many applications of approximate membership query data structures, or filters, require only an incremental filter that supports insertions but not deletions. However, the design space of incremental filters is missing a "sweet spot" filter that combines space efficiency, fast queries, and fast insertions. Incremental filters, such as the Bloom and blocked Bloom filter, are not space efficient. Dyn… ▽ More Many applications of approximate membership query data structures, or filters, require only an incremental filter that supports insertions but not deletions. However, the design space of incremental filters is missing a "sweet spot" filter that combines space efficiency, fast queries, and fast insertions. Incremental filters, such as the Bloom and blocked Bloom filter, are not space efficient. Dynamic filters (i.e., supporting deletions), such as the cuckoo or vector quotient filter, are space efficient but do not exhibit consistently fast insertions and queries. In this paper, we propose the prefix filter, an incremental filter that addresses the above challenge: (1) its space (in bits) is similar to state-of-the-art dynamic filters; (2) query throughput is high and is comparable to that of the cuckoo filter; and (3) insert throughput is high with overall build times faster than those of the vector quotient filter and cuckoo filter by $1.39\times$-$1.46\times$ and $3.2\times$-$3.5\times$, respectively. We present a rigorous analysis of the prefix filter that holds also for practical set sizes (i.e., $n=2^{25}$). The analysis deals with the probability of failure, false positive rate, and probability that an operation requires accessing more than a single cache line. △ Less

Submitted 25 October, 2022; v1 submitted 31 March, 2022; originally announced March 2022.

Comments: Full version of VLDB'22 paper

Exploring hyper-parameter spaces of neuroscience models on high performance computers with Learning to Learn

Authors: Alper Yegenoglu, Anand Subramoney, Thorsten Hater, Cristian Jimenez-Romero, Wouter Klijn, Aaron Perez Martin, Michiel van der Vlag, Michael Herty, Abigail Morrison, Sandra Diaz-Pier

Abstract: Neuroscience models commonly have a high number of degrees of freedom and only specific regions within the parameter space are able to produce dynamics of interest. This makes the development of tools and strategies to efficiently find these regions of high importance to advance brain research. Exploring the high dimensional parameter space using numerical simulations has been a frequently used te… ▽ More Neuroscience models commonly have a high number of degrees of freedom and only specific regions within the parameter space are able to produce dynamics of interest. This makes the development of tools and strategies to efficiently find these regions of high importance to advance brain research. Exploring the high dimensional parameter space using numerical simulations has been a frequently used technique in the last years in many areas of computational neuroscience. High performance computing (HPC) can provide today a powerful infrastructure to speed up explorations and increase our general understanding of the model's behavior in reasonable times. △ Less

Submitted 28 February, 2022; originally announced February 2022.

Cuckoo Trie: Exploiting Memory-Level Parallelism for Efficient DRAM Indexing

Authors: Adar Zeitak, Adam Morrison

Abstract: We present the Cuckoo Trie, a fast, memory-efficient ordered index structure. The Cuckoo Trie is designed to have memory-level parallelism -- which a modern out-of-order processor can exploit to execute DRAM accesses in parallel -- without sacrificing memory efficiency. The Cuckoo Trie thus breaks a fundamental performance barrier faced by current indexes, whose bottleneck is a series of dependent… ▽ More We present the Cuckoo Trie, a fast, memory-efficient ordered index structure. The Cuckoo Trie is designed to have memory-level parallelism -- which a modern out-of-order processor can exploit to execute DRAM accesses in parallel -- without sacrificing memory efficiency. The Cuckoo Trie thus breaks a fundamental performance barrier faced by current indexes, whose bottleneck is a series of dependent pointer-chasing DRAM accesses -- e.g., traversing a search tree path -- which the processor cannot parallelize. Our evaluation shows that the Cuckoo Trie outperforms state-of-the-art-indexes by up to 20%--360% on a variety of datasets and workloads, typically with a smaller or comparable memory footprint. △ Less

Submitted 23 January, 2022; originally announced January 2022.

Comments: Published in SOSP 2021

espiownage: Tracking Transients in Steelpan Drum Strikes Using Surveillance Technology

Authors: Scott H. Hawley, Andrew C. Morrison, Grant S. Morgan

Abstract: We present an improvement in the ability to meaningfully track features in high speed videos of Caribbean steelpan drums illuminated by Electronic Speckle Pattern Interferometry (ESPI). This is achieved through the use of up-to-date computer vision libraries for object detection and image segmentation as well as a significant effort toward cleaning the dataset previously used to train systems for… ▽ More We present an improvement in the ability to meaningfully track features in high speed videos of Caribbean steelpan drums illuminated by Electronic Speckle Pattern Interferometry (ESPI). This is achieved through the use of up-to-date computer vision libraries for object detection and image segmentation as well as a significant effort toward cleaning the dataset previously used to train systems for this application. Besides improvements on previous metric scores by 10% or more, noteworthy in this project are the introduction of a segmentation-regression map for the entire drum surface yielding interference fringe counts comparable to those obtained via object detection, as well as the accelerated workflow for coordinating the data-cleaning-and-model-training feedback loop for rapid iteration allowing this project to be conducted on a timescale of only 18 days. △ Less

Submitted 23 October, 2021; originally announced October 2021.

Comments: 6 pages, 5 figures, submitted to NeurIPS 2021 Workshop on Machine Learning and the Physical Sciences

ACM Class: I.4.6; I.4.9

An Analysis of Speculative Type Confusion Vulnerabilities in the Wild

Authors: Ofek Kirzner, Adam Morrison

Abstract: Spectre v1 attacks, which exploit conditional branch misprediction, are often identified with attacks that bypass array bounds checking to leak data from a victim's memory. Generally, however, Spectre v1 attacks can exploit any conditional branch misprediction that makes the victim execute code incorrectly. In this paper, we investigate speculative type confusion, a Spectre v1 attack vector in whi… ▽ More Spectre v1 attacks, which exploit conditional branch misprediction, are often identified with attacks that bypass array bounds checking to leak data from a victim's memory. Generally, however, Spectre v1 attacks can exploit any conditional branch misprediction that makes the victim execute code incorrectly. In this paper, we investigate speculative type confusion, a Spectre v1 attack vector in which branch mispredictions make the victim execute with variables holding values of the wrong type and thereby leak memory content. We observe that speculative type confusion can be inadvertently introduced by a compiler, making it extremely hard for programmers to reason about security and manually apply Spectre mitigations. We thus set out to determine the extent to which speculative type confusion affects the Linux kernel. Our analysis finds exploitable and potentially-exploitable arbitrary memory disclosure vulnerabilities. We also find many latent vulnerabilities, which could become exploitable due to innocuous system changes, such as coding style changes. Our results suggest that Spectre mitigations which rely on statically/manually identifying "bad" code patterns need to be rethought, and more comprehensive mitigations are needed. △ Less

Submitted 2 July, 2021; v1 submitted 29 June, 2021; originally announced June 2021.

Comments: To appear in USENIX Security 2021

ConvNets for Counting: Object Detection of Transient Phenomena in Steelpan Drums

Authors: Scott H. Hawley, Andrew C. Morrison

Abstract: We train an object detector built from convolutional neural networks to count interference fringes in elliptical antinode regions in frames of high-speed video recordings of transient oscillations in Caribbean steelpan drums illuminated by electronic speckle pattern interferometry (ESPI). The annotations provided by our model aim to contribute to the understanding of time-dependent behavior in suc… ▽ More We train an object detector built from convolutional neural networks to count interference fringes in elliptical antinode regions in frames of high-speed video recordings of transient oscillations in Caribbean steelpan drums illuminated by electronic speckle pattern interferometry (ESPI). The annotations provided by our model aim to contribute to the understanding of time-dependent behavior in such drums by tracking the development of sympathetic vibration modes. The system is trained on a dataset of crowdsourced human-annotated images obtained from the Zooniverse Steelpan Vibrations Project. Due to the small number of human-annotated images and the ambiguity of the annotation task, we also evaluate the model on a large corpus of synthetic images whose properties have been matched to the real images by style transfer using a Generative Adversarial Network. Applying the model to thousands of unlabeled video frames, we measure oscillations consistent with audio recordings of these drum strikes. One unanticipated result is that sympathetic oscillations of higher-octave notes significantly precede the rise in sound intensity of the corresponding second harmonic tones; the mechanism responsible for this remains unidentified. This paper primarily concerns the development of the predictive model; further exploration of the steelpan images and deeper physical insights await its further application. △ Less

Submitted 6 September, 2021; v1 submitted 31 January, 2021; originally announced February 2021.

Comments: 13 pages, 9 figures, accepted for J. Acous. Soc. Am. (JASA) Special Issue on Machine Learning in Acoustics

ACM Class: I.4.7

Recoverable, Abortable, and Adaptive Mutual Exclusion with Sublogarithmic RMR Complexity

Authors: Daniel Katzan, Adam Morrison

Abstract: We present the first recoverable mutual exclusion (RME) algorithm that is simultaneously abortable, adaptive to point contention, and with sublogarithmic RMR complexity. Our algorithm has $O(\min(K,\log_W N))$ RMR passage complexity and $O(F + \min(K,\log_W N))$ RMR super-passage complexity, where $K$ is the number of concurrent processes (point contention), $W$ is the size (in bits) of registers,… ▽ More We present the first recoverable mutual exclusion (RME) algorithm that is simultaneously abortable, adaptive to point contention, and with sublogarithmic RMR complexity. Our algorithm has $O(\min(K,\log_W N))$ RMR passage complexity and $O(F + \min(K,\log_W N))$ RMR super-passage complexity, where $K$ is the number of concurrent processes (point contention), $W$ is the size (in bits) of registers, and $F$ is the number of crashes in a super-passage. Under the standard assumption that $W=Θ(\log N)$, these bounds translate to worst-case $O(\frac{\log N}{\log \log N})$ passage complexity and $O(F + \frac{\log N}{\log \log N})$ super-passage complexity. Our key building blocks are: * A $D$-process abortable RME algorithm, for $D \leq W$, with $O(1)$ passage complexity and $O(1+F)$ super-passage complexity. We obtain this algorithm by using the Fetch-And-Add (FAA) primitive, unlike prior work on RME that uses Fetch-And-Store (FAS/SWAP). * A generic transformation that transforms any abortable RME algorithm with passage complexity of $B < W$, into an abortable RME lock with passage complexity of $O(\min(K,B))$. △ Less

Submitted 8 July, 2023; v1 submitted 15 November, 2020; originally announced November 2020.

Comments: Full version of OPODIS 2020 paper

Proving Highly-Concurrent Traversals Correct

Authors: Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky, Sharon Shoham

Abstract: Modern highly-concurrent search data structures, such as search trees, obtain multi-core scalability and performance by having operations traverse the data structure without any synchronization. As a result, however, these algorithms are notoriously difficult to prove linearizable, which requires identifying a point in time in which the traversal's result is correct. The problem is that traversing… ▽ More Modern highly-concurrent search data structures, such as search trees, obtain multi-core scalability and performance by having operations traverse the data structure without any synchronization. As a result, however, these algorithms are notoriously difficult to prove linearizable, which requires identifying a point in time in which the traversal's result is correct. The problem is that traversing the data structure as it undergoes modifications leads to complex behaviors, necessitating intricate reasoning about all interleavings of reads by traversals and writes mutating the data structure. In this paper, we present a general proof technique for proving unsynchronized traversals correct in a significantly simpler manner, compared to typical concurrent reasoning and prior proof techniques. Our framework relies only on sequential properties} of traversals and on a conceptually simple and widely-applicable condition about the ways an algorithm's writes mutate the data structure. Establishing that a target data structure satisfies our condition requires only simple concurrent reasoning, without considering interactions of writes and reads. This reasoning can be further simplified by using our framework. To demonstrate our technique, we apply it to prove several interesting and challenging concurrent binary search trees: the logical-ordering AVL tree, the Citrus tree, and the full contention-friendly tree. Both the logical-ordering tree and the full contention-friendly tree are beyond the reach of previous approaches targeted at simplifying linearizability proofs. △ Less

Submitted 10 January, 2024; v1 submitted 2 October, 2020; originally announced October 2020.

Comments: Extended version of a paper appearing in OOPSLA'20

Just another quantum assembly language (Jaqal)

Authors: Benjamin C. A. Morrison, Andrew J. Landahl, Daniel S. Lobser, Kenneth M. Rudinger, Antonio E. Russo, Jay W. Van Der Wall, Peter Maunz

Abstract: The Quantum Scientific Computing Open User Testbed (QSCOUT) is a trapped-ion quantum computer testbed realized at Sandia National Laboratories on behalf of the Department of Energy's Office of Science and its Advanced Scientific Computing (ASCR) program. Here we describe Jaqal, for Just another quantum assembly language, the programming language we invented to specify programs executed on QSCOUT.… ▽ More The Quantum Scientific Computing Open User Testbed (QSCOUT) is a trapped-ion quantum computer testbed realized at Sandia National Laboratories on behalf of the Department of Energy's Office of Science and its Advanced Scientific Computing (ASCR) program. Here we describe Jaqal, for Just another quantum assembly language, the programming language we invented to specify programs executed on QSCOUT. Jaqal is useful beyond QSCOUT---it can support mutliple hardware targets because it offloads gate names and their pulse-sequence definitions to external files. We describe the capabilities of the Jaqal language, our approach in designing it, and the reasons for its creation. To learn more about QSCOUT, Jaqal, or JaqalPaq, the metaprogramming Python package we developed for Jaqal, please visit https://qscout.sandia.gov, https://gitlab.com/jaqal, or send an e-mail to [email protected]. △ Less

Submitted 18 August, 2020; originally announced August 2020.

Comments: Accepted by the IEEE International Conference on Quantum Computing and Engineering, Oct. 12-16, 2020. Contains overlaps with the formal Jaqal language specification in arXiv:2003.09382, but expands significantly on the rationales behind the language choices made

Speculative Interference Attacks: Breaking Invisible Speculation Schemes

Authors: Mohammad Behnia, Prateek Sahu, Riccardo Paccagnella, Jiyong Yu, Zirui Zhao, Xiang Zou, Thomas Unterluggauer, Josep Torrellas, Carlos Rozas, Adam Morrison, Frank Mckeen, Fangfei Liu, Ron Gabor, Christopher W. Fletcher, Abhishek Basak, Alaa Alameldeen

Abstract: Recent security vulnerabilities that target speculative execution (e.g., Spectre) present a significant challenge for processor design. The highly publicized vulnerability uses speculative execution to learn victim secrets by changing cache state. As a result, recent computer architecture research has focused on invisible speculation mechanisms that attempt to block changes in cache state due to s… ▽ More Recent security vulnerabilities that target speculative execution (e.g., Spectre) present a significant challenge for processor design. The highly publicized vulnerability uses speculative execution to learn victim secrets by changing cache state. As a result, recent computer architecture research has focused on invisible speculation mechanisms that attempt to block changes in cache state due to speculative execution. Prior work has shown significant success in preventing Spectre and other vulnerabilities at modest performance costs. In this paper, we introduce speculative interference attacks, which show that prior invisible speculation mechanisms do not fully block these speculation-based attacks. We make two key observations. First, misspeculated younger instructions can change the timing of older, bound-to-retire instructions, including memory operations. Second, changing the timing of a memory operation can change the order of that memory operation relative to other memory operations, resulting in persistent changes to the cache state. Using these observations, we demonstrate (among other attack variants) that secret information accessed by mis-speculated instructions can change the order of bound-to-retire loads. Load timing changes can therefore leave secret-dependent changes in the cache, even in the presence of invisible speculation mechanisms. We show that this problem is not easy to fix: Speculative interference converts timing changes to persistent cache-state changes, and timing is typically ignored by many cache-based defenses. We develop a framework to understand the attack and demonstrate concrete proof-of-concept attacks against invisible speculation mechanisms. We provide security definitions sufficient to block speculative interference attacks; describe a simple defense mechanism with a high performance cost; and discuss how future research can improve its performance. △ Less

Submitted 23 April, 2021; v1 submitted 23 July, 2020; originally announced July 2020.

Comments: Updated CR Version

Programmable In-Network Security for Context-aware BYOD Policies

Authors: Qiao Kang, Lei Xue, Adam Morrison, Yuxin Tang, Ang Chen, Xiapu Luo

Abstract: Bring Your Own Device (BYOD) has become the new norm in enterprise networks, but BYOD security remains a top concern. Context-aware security, which enforces access control based on dynamic runtime context, holds much promise. Recent work has developed SDN solutions to collect device context for network-wide access control in a central controller. However, the central controller poses a bottleneck… ▽ More Bring Your Own Device (BYOD) has become the new norm in enterprise networks, but BYOD security remains a top concern. Context-aware security, which enforces access control based on dynamic runtime context, holds much promise. Recent work has developed SDN solutions to collect device context for network-wide access control in a central controller. However, the central controller poses a bottleneck that can become an attack target, and processing context changes at remote software has low agility. We present a new paradigm, programmable in-network security (Poise), which is enabled by the emergence of programmable switches. At the heart of Poise is a novel switch primitive, which can be programmed to support a wide range of context-aware policies in hardware. Users of Poise specify concise policies, and Poise compiles them into different instantiations of the security primitive in P4. Compared to centralized SDN defenses, Poise is resilient to control plane saturation attacks, and it dramatically increases defense agility. △ Less

Submitted 4 August, 2019; originally announced August 2019.

Staged deployment of interactive multi-application HPC workflows

Authors: Wouter Klijn, Sandra Diaz-Pier, Abigail Morrison, Alexander Peyser

Abstract: Running scientific workflows on a supercomputer can be a daunting task for a scientific domain specialist. Workflow management solutions (WMS) are a standard method for reducing the complexity of application deployment on high performance computing (HPC) infrastructure. We introduce the design for a middleware system that extends and combines the functionality from existing solutions in order to c… ▽ More Running scientific workflows on a supercomputer can be a daunting task for a scientific domain specialist. Workflow management solutions (WMS) are a standard method for reducing the complexity of application deployment on high performance computing (HPC) infrastructure. We introduce the design for a middleware system that extends and combines the functionality from existing solutions in order to create a high-level, staged user-centric operation/deployment model. This design addresses the requirements of several use cases in the life sciences, with a focus on neuroscience. In this manuscript we focus on two use cases: 1) three coupled neuronal simulators (for three different space/time scales) with in-transit visualization and 2) a closed-loop workflow optimized by machine learning, coupling a robot with a neural network simulation. We provide a detailed overview of the application-integrated monitoring in relationship with the HPC job. We present here a novel usage model for large scale interactive multi-application workflows running on HPC systems which aims at reducing the complexity of deployment and execution, thus enabling new science. △ Less

Submitted 29 July, 2019; originally announced July 2019.

Comments: 7 pages, 3 figures, The 2019 International Conference on High Performance Computing & Simulation

Order out of Chaos: Proving Linearizability Using Local Views

Authors: Yotam M. Y. Feldman, Constantin Enea, Adam Morrison, Noam Rinetzky, Sharon Shoham

Abstract: Proving the linearizability of highly concurrent data structures, such as those using optimistic concurrency control, is a challenging task. The main difficulty is in reasoning about the view of the memory obtained by the threads, because as they execute, threads observe different fragments of memory from different points in time. Until today, every linearizability proof has tackled this challenge… ▽ More Proving the linearizability of highly concurrent data structures, such as those using optimistic concurrency control, is a challenging task. The main difficulty is in reasoning about the view of the memory obtained by the threads, because as they execute, threads observe different fragments of memory from different points in time. Until today, every linearizability proof has tackled this challenge from scratch. We present a unifying proof argument for the correctness of unsynchronized traversals, and apply it to prove the linearizability of several highly concurrent search data structures, including an optimistic self-balancing binary search tree, the Lazy List and a lock-free skip list. Our framework harnesses {\em sequential reasoning} about the view of a thread, considering the thread as if it traverses the data structure without interference from other operations. Our key contribution is showing that properties of reachability along search paths can be deduced for concurrent traversals from such interference-free traversals, when certain intuitive conditions are met. Basing the correctness of traversals on such \emph{local view arguments} greatly simplifies linearizability proofs. To apply our framework, the user proves that the data structure satisfies two conditions: (1) acyclicity of the order on memory, even when it is considered across intermediate memory states, and (2) preservation of search paths to locations modified by interfering writes. Establishing the conditions, as well as the full linearizability proof utilizing our proof argument, reduces to simple concurrent reasoning. The result is a clear and comprehensible correctness proof, and elucidates common patterns underlying several existing data structures. △ Less

Submitted 5 August, 2018; v1 submitted 10 May, 2018; originally announced May 2018.

Comments: Full version of the DISC'18 paper

NESTML: a modeling language for spiking neurons

Authors: Dimitri Plotnikov, Bernhard Rumpe, Inga Blundell, Tammo Ippen, Jochen Martin Eppler, Abgail Morrison

Abstract: Biological nervous systems exhibit astonishing complexity .Neuroscientists aim to capture this com- plexity by modeling and simulation of biological processes. Often very comple xm odels are nec- essary to depict the processes, which makes it dif fi cult to create these models. Powerful tools are thus necessary ,which enable neuroscientists to express models in acomprehensi ve and concise way and… ▽ More Biological nervous systems exhibit astonishing complexity .Neuroscientists aim to capture this com- plexity by modeling and simulation of biological processes. Often very comple xm odels are nec- essary to depict the processes, which makes it dif fi cult to create these models. Powerful tools are thus necessary ,which enable neuroscientists to express models in acomprehensi ve and concise way and generate ef fi cient code for digital simulations. Se veral modeling languages for computational neuroscience ha ve been proposed [Gl10, Ra11]. Howe ver, as these languages seek simulator inde- pendence the ytypically only support asubset of the features desired by the modeler .Int his article, we present the modular and extensible domain speci fi cl anguage NESTML, which provides neuro- science domain concepts as fi rst-class language constructs and supports domain experts in creating neuron models for the neural simulation tool NEST .N ESTML and aset of example models are publically available on GitHub. △ Less

Submitted 9 June, 2016; originally announced June 2016.

Comments: 16 pages, 5 figures, Modellierung 2016 Conference

Closed loop interactions between spiking neural network and robotic simulators based on MUSIC and ROS

Authors: Philipp Weidel, Mikael Djurfeldt, Renato Duarte, Abigail Morrison

Abstract: In order to properly assess the function and computational properties of simulated neural systems, it is necessary to account for the nature of the stimuli that drive the system. However, providing stimuli that are rich and yet both reproducible and amenable to experimental manipulations is technically challenging, and even more so if a closed-loop scenario is required. In this work, we present a… ▽ More In order to properly assess the function and computational properties of simulated neural systems, it is necessary to account for the nature of the stimuli that drive the system. However, providing stimuli that are rich and yet both reproducible and amenable to experimental manipulations is technically challenging, and even more so if a closed-loop scenario is required. In this work, we present a novel approach to solve this problem, connecting robotics and neural network simulators. We implement a middleware solution that bridges the Robotic Operating System (ROS) to the Multi-Simulator Coordinator (MUSIC). This enables any robotic and neural simulators that implement the corresponding interfaces to be efficiently coupled, allowing real-time performance for a wide range of configurations. This work extends the toolset available for researchers in both neurorobotics and computational neuroscience, and creates the opportunity to perform closed-loop experiments of arbitrary complexity to address questions in multiple areas, including embodiment, agency, and reinforcement learning. △ Less

Submitted 16 April, 2016; originally announced April 2016.

Probabilistic Formal Analysis of App Usage to Inform Redesign

Authors: Oana Andrei, Muffy Calder, Matthew Chalmers, Alistair Morrison, Mattias Rost

Abstract: This paper sets out a process of app analysis intended to support understanding of use but also redesign. From usage logs we infer activity patterns - Markov models - and employ probabilistic formal analysis to ask questions about the use of the app. The core of this paper's contribution is a bridging of stochastic and formal modelling, but we also describe the work to make that analytic core util… ▽ More This paper sets out a process of app analysis intended to support understanding of use but also redesign. From usage logs we infer activity patterns - Markov models - and employ probabilistic formal analysis to ask questions about the use of the app. The core of this paper's contribution is a bridging of stochastic and formal modelling, but we also describe the work to make that analytic core utile within a design team. We illustrate our work via a case study of a mobile app presenting analytic findings and discussing how they are feeding into redesign. We had posited that two activity patterns indicated two separable sets of users, each of which might benefit from a differently tailored app version, but our subsequent analysis detailed users' interleaving of activity patterns over time - evidence speaking more in favour of redesign that supports each pattern in an integrated way. We uncover patterns consisting of brief glances at particular data and recommend them as possible candidates for new design work on widget extensions: small displays available while users use other apps. △ Less

Submitted 27 October, 2015; originally announced October 2015.

Comments: 13 pages, 6 figures, 7 tables, under review