-
Evidence Tampering and Chain of Custody in Layered Attestations
Authors:
Ian D. Kretz,
Clare C. Parran,
John D. Ramsdell,
Paul D. Rowe
Abstract:
In distributed systems, trust decisions are made on the basis of integrity evidence generated via remote attestation. Examples of the kinds of evidence that might be collected are boot time image hash values; fingerprints of initialization files for userspace applications; and a comprehensive measurement of a running kernel. In layered attestations, evidence is typically composed of measurements o…
▽ More
In distributed systems, trust decisions are made on the basis of integrity evidence generated via remote attestation. Examples of the kinds of evidence that might be collected are boot time image hash values; fingerprints of initialization files for userspace applications; and a comprehensive measurement of a running kernel. In layered attestations, evidence is typically composed of measurements of key subcomponents taken from different trust boundaries within a target system. Discrete measurement evidence is bundled together for appraisal by the components that collectively perform the attestation.
In this paper, we initiate the study of evidence chain of custody for remote attestation. Using the Copland attestation specification language, we formally define the conditions under which a runtime adversary active on the target system can tamper with measurement evidence. We present algorithms for identifying all such tampering opportunities for given evidence as well as tampering "strategies" by which an adversary can modify incriminating evidence without being detected. We then define a procedure for transforming a Copland-specified attestation into a maximally tamper-resistant version of itself. Our efforts are intended to help attestation protocol designers ensure their protocols reduce evidence tampering opportunities to the smallest, most trustworthy set of components possible.
△ Less
Submitted 31 January, 2024;
originally announced February 2024.
-
Generation of patient specific cardiac chamber models using generative neural networks under a Bayesian framework for electroanatomical map**
Authors:
Sunil Mathew,
Jasbir Sra,
Daniel B. Rowe
Abstract:
Electroanatomical map** is a technique used in cardiology to create a detailed 3D map of the electrical activity in the heart. It is useful for diagnosis, treatment planning and real time guidance in cardiac ablation procedures to treat arrhythmias like atrial fibrillation. A probabilistic machine learning model trained on a library of CT/MRI scans of the heart can be used during electroanatomic…
▽ More
Electroanatomical map** is a technique used in cardiology to create a detailed 3D map of the electrical activity in the heart. It is useful for diagnosis, treatment planning and real time guidance in cardiac ablation procedures to treat arrhythmias like atrial fibrillation. A probabilistic machine learning model trained on a library of CT/MRI scans of the heart can be used during electroanatomical map** to generate a patient-specific 3D model of the chamber being mapped. The use of probabilistic machine learning models under a Bayesian framework provides a way to quantify uncertainty in results and provide a natural framework of interpretability of the model. Here we introduce a Bayesian approach to surface reconstruction of cardiac chamber models from a sparse 3D point cloud data acquired during electroanatomical map**. We show how probabilistic graphical models trained on segmented CT/MRI data can be used to generate cardiac chamber models from few acquired locations thereby reducing procedure time and x-ray exposure. We show how they provide insight into what the neural network learns from the segmented CT/MRI images used to train the network, which provides explainability to the resulting cardiac chamber models generated by the model.
△ Less
Submitted 26 November, 2023;
originally announced November 2023.
-
Pruning a neural network using Bayesian inference
Authors:
Sunil Mathew,
Daniel B. Rowe
Abstract:
Neural network pruning is a highly effective technique aimed at reducing the computational and memory demands of large neural networks. In this research paper, we present a novel approach to pruning neural networks utilizing Bayesian inference, which can seamlessly integrate into the training procedure. Our proposed method leverages the posterior probabilities of the neural network prior to and fo…
▽ More
Neural network pruning is a highly effective technique aimed at reducing the computational and memory demands of large neural networks. In this research paper, we present a novel approach to pruning neural networks utilizing Bayesian inference, which can seamlessly integrate into the training procedure. Our proposed method leverages the posterior probabilities of the neural network prior to and following pruning, enabling the calculation of Bayes factors. The calculated Bayes factors guide the iterative pruning. Through comprehensive evaluations conducted on multiple benchmarks, we demonstrate that our method achieves desired levels of sparsity while maintaining competitive accuracy.
△ Less
Submitted 4 August, 2023;
originally announced August 2023.
-
No Language Left Behind: Scaling Human-Centered Machine Translation
Authors:
NLLB Team,
Marta R. Costa-jussà,
James Cross,
Onur Çelebi,
Maha Elbayad,
Kenneth Heafield,
Kevin Heffernan,
Elahe Kalbassi,
Janice Lam,
Daniel Licht,
Jean Maillard,
Anna Sun,
Skyler Wang,
Guillaume Wenzek,
Al Youngblood,
Bapi Akula,
Loic Barrault,
Gabriel Mejia Gonzalez,
Prangthip Hansanti,
John Hoffman,
Semarley Jarrett,
Kaushik Ram Sadagopan,
Dirk Rowe,
Shannon Spruit,
Chau Tran
, et al. (14 additional authors not shown)
Abstract:
Driven by the goal of eradicating language barriers on a global scale, machine translation has solidified itself as a key focus of artificial intelligence research today. However, such efforts have coalesced around a small subset of languages, leaving behind the vast majority of mostly low-resource languages. What does it take to break the 200 language barrier while ensuring safe, high quality res…
▽ More
Driven by the goal of eradicating language barriers on a global scale, machine translation has solidified itself as a key focus of artificial intelligence research today. However, such efforts have coalesced around a small subset of languages, leaving behind the vast majority of mostly low-resource languages. What does it take to break the 200 language barrier while ensuring safe, high quality results, all while kee** ethical considerations in mind? In No Language Left Behind, we took on this challenge by first contextualizing the need for low-resource language translation support through exploratory interviews with native speakers. Then, we created datasets and models aimed at narrowing the performance gap between low and high-resource languages. More specifically, we developed a conditional compute model based on Sparsely Gated Mixture of Experts that is trained on data obtained with novel and effective data mining techniques tailored for low-resource languages. We propose multiple architectural and training improvements to counteract overfitting while training on thousands of tasks. Critically, we evaluated the performance of over 40,000 different translation directions using a human-translated benchmark, Flores-200, and combined human evaluation with a novel toxicity benchmark covering all languages in Flores-200 to assess translation safety. Our model achieves an improvement of 44% BLEU relative to the previous state-of-the-art, laying important groundwork towards realizing a universal translation system. Finally, we open source all contributions described in this work, accessible at https://github.com/facebookresearch/fairseq/tree/nllb.
△ Less
Submitted 25 August, 2022; v1 submitted 11 July, 2022;
originally announced July 2022.
-
Graph Convolutional Networks for Model-Based Learning in Nonlinear Inverse Problems
Authors:
William Herzberg,
Daniel B. Rowe,
Andreas Hauptmann,
Sarah J. Hamilton
Abstract:
The majority of model-based learned image reconstruction methods in medical imaging have been limited to uniform domains, such as pixelated images. If the underlying model is solved on nonuniform meshes, arising from a finite element method typical for nonlinear inverse problems, interpolation and embeddings are needed. To overcome this, we present a flexible framework to extend model-based learni…
▽ More
The majority of model-based learned image reconstruction methods in medical imaging have been limited to uniform domains, such as pixelated images. If the underlying model is solved on nonuniform meshes, arising from a finite element method typical for nonlinear inverse problems, interpolation and embeddings are needed. To overcome this, we present a flexible framework to extend model-based learning directly to nonuniform meshes, by interpreting the mesh as a graph and formulating our network architectures using graph convolutional neural networks. This gives rise to the proposed iterative Graph Convolutional Newton-type Method (GCNM), which includes the forward model in the solution of the inverse problem, while all updates are directly computed by the network on the problem specific mesh. We present results for Electrical Impedance Tomography, a severely ill-posed nonlinear inverse problem that is frequently solved via optimization-based methods, where the forward problem is solved by finite element methods. Results for absolute EIT imaging are compared to standard iterative methods as well as a graph residual network. We show that the GCNM has strong generalizability to different domain shapes and meshes, out of distribution data as well as experimental data, from purely simulated training data and without transfer training.
△ Less
Submitted 8 July, 2021; v1 submitted 28 March, 2021;
originally announced March 2021.
-
Limitations on Observability of Effects in Cyber-Physical Systems
Authors:
Suresh K. Damodaran,
Paul D. Rowe
Abstract:
Increased interconnectivity of Cyber-Physical Systems, by design or otherwise, increases the cyber attack surface and attack vectors. Observing the effects of these attacks is helpful in detecting them. In this paper, we show that many attacks on such systems result in a control loop effect we term Process Model Inconsistency (PMI). Our formal approach elucidates the relationships among incomplete…
▽ More
Increased interconnectivity of Cyber-Physical Systems, by design or otherwise, increases the cyber attack surface and attack vectors. Observing the effects of these attacks is helpful in detecting them. In this paper, we show that many attacks on such systems result in a control loop effect we term Process Model Inconsistency (PMI). Our formal approach elucidates the relationships among incompleteness, incorrectness, safety, and inconsistency of process models. We show that incomplete process models lead to inconsistency. Surprisingly, inconsistency may arise even in complete and correct models. We illustrate our approach through an Automated Teller Machine (ATM) example, and describe the practical implications of the theoretical results.
△ Less
Submitted 22 March, 2019;
originally announced March 2019.
-
Enrich-by-need Protocol Analysis for Diffie-Hellman (Extended Version)
Authors:
Moses D. Liskov,
Joshua D. Guttman,
John D. Ramsdell,
Paul D. Rowe,
F. Javier Thayer
Abstract:
Enrich-by-need protocol analysis is a style of symbolic protocol analysis that characterizes all executions of a protocol that extend a given scenario. In effect, it computes a strongest security goal the protocol achieves in that scenario. CPSA, a Cryptographic Protocol Shapes Analyzer, implements enrich-by-need protocol analysis.
In this paper, we describe how to analyze protocols using the Di…
▽ More
Enrich-by-need protocol analysis is a style of symbolic protocol analysis that characterizes all executions of a protocol that extend a given scenario. In effect, it computes a strongest security goal the protocol achieves in that scenario. CPSA, a Cryptographic Protocol Shapes Analyzer, implements enrich-by-need protocol analysis.
In this paper, we describe how to analyze protocols using the Diffie-Hellman mechanism for key agreement (DH) in the enrich-by-need style. DH, while widespread, has been challenging for protocol analysis because of its algebraic structure. DH essentially involves fields and cyclic groups, which do not fit the standard foundational framework of symbolic protocol analysis. By contrast, we justify our analysis via an algebraically natural model.
This foundation makes the extended CPSA implementation reliable. Moreover, it provides informative and efficient results.
An appendix explains how unification is efficiently done in our framework.
△ Less
Submitted 16 April, 2018;
originally announced April 2018.
-
Principles of Layered Attestation
Authors:
Paul D. Rowe
Abstract:
Systems designed with measurement and attestation in mind are often layered, with the lower layers measuring the layers above them. Attestations of such systems, which we call layered attestations, must bundle together the results of a diverse set of application-specific measurements of various parts of the system. Some methods of layered attestation are more trustworthy than others, so it is impo…
▽ More
Systems designed with measurement and attestation in mind are often layered, with the lower layers measuring the layers above them. Attestations of such systems, which we call layered attestations, must bundle together the results of a diverse set of application-specific measurements of various parts of the system. Some methods of layered attestation are more trustworthy than others, so it is important for system designers to understand the trust consequences of different system configurations. This paper presents a formal framework for reasoning about layered attestations, and provides generic reusable principles for achieving trustworthy results.
△ Less
Submitted 3 March, 2016;
originally announced March 2016.
-
Formal Support for Standardizing Protocols with State
Authors:
Joshua D. Guttman,
Moses D. Liskov,
John D. Ramsdell,
Paul D. Rowe
Abstract:
Many cryptographic protocols are designed to achieve their goals using only messages passed over an open network. Numerous tools, based on well-understood foundations, exist for the design and analysis of protocols that rely purely on message passing. However, these tools encounter difficulties when faced with protocols that rely on non-local, mutable state to coordinate several local sessions.…
▽ More
Many cryptographic protocols are designed to achieve their goals using only messages passed over an open network. Numerous tools, based on well-understood foundations, exist for the design and analysis of protocols that rely purely on message passing. However, these tools encounter difficulties when faced with protocols that rely on non-local, mutable state to coordinate several local sessions.
We adapt one of these tools, {\cpsa}, to provide automated support for reasoning about state. We use Ryan's Envelope Protocol as an example to demonstrate how the message-passing reasoning can be integrated with state reasoning to yield interesting and powerful results.
Keywords: protocol analysis tools, stateful protocols, TPM, PKCS#11.
△ Less
Submitted 24 September, 2015;
originally announced September 2015.
-
A Cut Principle for Information Flow
Authors:
Joshua D. Guttman,
Paul D. Rowe
Abstract:
We view a distributed system as a graph of active locations with unidirectional channels between them, through which they pass messages. In this context, the graph structure of a system constrains the propagation of information through it.
Suppose a set of channels is a cut set between an information source and a potential sink. We prove that, if there is no disclosure from the source to the cut…
▽ More
We view a distributed system as a graph of active locations with unidirectional channels between them, through which they pass messages. In this context, the graph structure of a system constrains the propagation of information through it.
Suppose a set of channels is a cut set between an information source and a potential sink. We prove that, if there is no disclosure from the source to the cut set, then there can be no disclosure to the sink. We introduce a new formalization of partial disclosure, called *blur operators*, and show that the same cut property is preserved for disclosure to within a blur operator. This cut-blur property also implies a compositional principle, which ensures limited disclosure for a class of systems that differ only beyond the cut.
△ Less
Submitted 24 March, 2015; v1 submitted 16 October, 2014;
originally announced October 2014.
-
A Hybrid Analysis for Security Protocols with State
Authors:
John D. Ramsdell,
Daniel J. Dougherty,
Joshua D. Guttman,
Paul D. Rowe
Abstract:
Cryptographic protocols rely on message-passing to coordinate activity among principals. Each principal maintains local state in individual local sessions only as needed to complete that session. However, in some protocols a principal also uses state to coordinate its different local sessions. Sometimes the non-local, mutable state is used as a means, for example with smart cards or Trusted Platfo…
▽ More
Cryptographic protocols rely on message-passing to coordinate activity among principals. Each principal maintains local state in individual local sessions only as needed to complete that session. However, in some protocols a principal also uses state to coordinate its different local sessions. Sometimes the non-local, mutable state is used as a means, for example with smart cards or Trusted Platform Modules. Sometimes it is the purpose of running the protocol, for example in commercial transactions.
Many richly developed tools and techniques, based on well-understood foundations, are available for design and analysis of pure message-passing protocols. But the presence of cross-session state poses difficulties for these techniques.
In this paper we provide a framework for modeling stateful protocols. We define a hybrid analysis method. It leverages theorem-proving---in this instance, the PVS prover---for reasoning about computations over state. It combines that with an "enrich-by-need" approach---embodied by CPSA---that focuses on the message-passing part. As a case study we give a full analysis of the Envelope Protocol, due to Mark Ryan.
△ Less
Submitted 16 June, 2014; v1 submitted 15 April, 2014;
originally announced April 2014.
