Showing 1–7 of 7 results for author: Cutler, J W

Cedar: A New Language for Expressive, Fast, Safe, and Analyzable Authorization (Extended Version)

Authors: Joseph W. Cutler, Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, Eleftherios Ioannidis, John Kastner, Anwar Mamat, Darin McAdams, Matt McCutchen, Neha Rungta, Emina Torlak, Andrew Wells

Abstract: Cedar is a new authorization policy language designed to be ergonomic, fast, safe, and analyzable. Rather than embed authorization logic in an application's code, developers can write that logic as Cedar policies and delegate access decisions to Cedar's evaluation engine. Cedar's simple and intuitive syntax supports common authorization use-cases with readable policies, naturally leveraging concep… ▽ More Cedar is a new authorization policy language designed to be ergonomic, fast, safe, and analyzable. Rather than embed authorization logic in an application's code, developers can write that logic as Cedar policies and delegate access decisions to Cedar's evaluation engine. Cedar's simple and intuitive syntax supports common authorization use-cases with readable policies, naturally leveraging concepts from role-based, attribute-based, and relation-based access control models. Cedar's policy structure enables access requests to be decided quickly. Cedar's policy validator leverages optional ty** to help policy writers avoid mistakes, but not get in their way. Cedar's design has been finely balanced to allow for a sound and complete logical encoding, which enables precise policy analysis, e.g., to ensure that when refactoring a set of policies, the authorized permissions do not change. We have modeled Cedar in the Lean programming language, and used Lean's proof assistant to prove important properties of Cedar's design. We have implemented Cedar in Rust, and released it open-source. Comparing Cedar to two open-source languages, OpenFGA and Rego, we find (subjectively) that Cedar has equally or more readable policies, but (objectively) performs far better. △ Less

Submitted 8 March, 2024; v1 submitted 7 March, 2024; originally announced March 2024.

Stream Types

Authors: Joseph W. Cutler, Christopher Watson, Emeka Nkurumeh, Phillip Hilliard, Harrison Goldstein, Caleb Stanford, Benjamin C. Pierce

Abstract: We propose a rich foundational theory of typed data streams and stream transformers, motivated by two high-level goals: (1) The type of a stream should be able to express complex sequential patterns of events over time. And (2) it should describe the internal parallel structure of the stream to support deterministic stream processing on parallel and distributed systems. To these ends, we introduce… ▽ More We propose a rich foundational theory of typed data streams and stream transformers, motivated by two high-level goals: (1) The type of a stream should be able to express complex sequential patterns of events over time. And (2) it should describe the internal parallel structure of the stream to support deterministic stream processing on parallel and distributed systems. To these ends, we introduce stream types, with operators capturing sequential composition, parallel composition, and iteration, plus a core calculus lambda-ST of transformers over typed streams which naturally supports a number of common streaming idioms, including punctuation, windowing, and parallel partitioning, as first-class constructions. lambda-ST exploits a Curry-Howard-like correspondence with an ordered variant of the logic of Bunched Implication to program with streams compositionally and uses Brzozowski-style derivatives to enable an incremental, prefix-based operational semantics. To illustrate the programming style supported by the rich types of lambda-ST, we present a number of examples written in delta, a prototype high-level language design based on lambda-ST. △ Less

Submitted 2 April, 2024; v1 submitted 18 July, 2023; originally announced July 2023.

Comments: Extended Version of the PLDI'24 paper

Fast and Noise-Resilient Magnetic Field Map** on a Low-Cost UAV Using Gaussian Process Regression

Authors: Prince E. Kuevor, Maani Ghaffari, Ella M. Atkins, James W. Cutler

Abstract: This work presents a number of techniques to improve the ability to create magnetic field maps on a UAV which can be used to quickly and reliably gather magnetic field observations at multiple altitudes in a workspace. Unfortunately, the electronics on the UAV can introduce their own magnetic fields, distorting the resultant magnetic field map. We show methods of reducing and working with UAV-indu… ▽ More This work presents a number of techniques to improve the ability to create magnetic field maps on a UAV which can be used to quickly and reliably gather magnetic field observations at multiple altitudes in a workspace. Unfortunately, the electronics on the UAV can introduce their own magnetic fields, distorting the resultant magnetic field map. We show methods of reducing and working with UAV-induced noise to better enable magnetic fields as a sensing modality for indoor navigation. First, some gains in our flight controller create high-frequency motor commands that introduce large noise in the measured magnetic field. Next, we implement a common noise reduction method of distancing the magnetometer from other components on our UAV. Finally, we introduce what we call a compromise GPR (Gaussian process regression) map that can be trained on multiple flight tests to learn any flight-by-flight variations between UAV observation tests. We investigate the spatial density of observations used to train a GPR map then use the compromise map to define a consistency test that can indicate whether or not the magnetometer data and corresponding GPR map are appropriate to use for state estimation. The interventions we introduce in this work facilitate indoor position localization of a UAV whose estimates we found to be quite sensitive to noise generated by the UAV. △ Less

Submitted 31 January, 2023; originally announced February 2023.

Denotational recurrence extraction for amortized analysis

Authors: Joseph W. Cutler, Daniel R. Licata, Norman Danner

Abstract: A typical way of analyzing the time complexity of functional programs is to extract a recurrence expressing the running time of the program in terms of the size of its input, and then to solve the recurrence to obtain a big-O bound. For recurrence extraction to be compositional, it is also necessary to extract recurrences for the size of outputs of helper functions. Previous work has developed tec… ▽ More A typical way of analyzing the time complexity of functional programs is to extract a recurrence expressing the running time of the program in terms of the size of its input, and then to solve the recurrence to obtain a big-O bound. For recurrence extraction to be compositional, it is also necessary to extract recurrences for the size of outputs of helper functions. Previous work has developed techniques for using logical relations to state a formal correctness theorem for a general recurrence extraction translation: a program is bounded by a recurrence when the operational cost is bounded by the extracted cost, and the output value is bounded, according to a value bounding relation defined by induction on types, by the extracted size. This previous work supports higher-order functions by viewing recurrences as programs in a lambda-calculus, or as mathematical entities in a denotational semantics thereof. In this paper, we extend these techniques to support amortized analysis, where costs are rearranged from one portion of a program to another to achieve more precise bounds. We give an intermediate language in which programs can be annotated according to the banker's method of amortized analysis; this language has an affine type system to ensure credits are not spent more than once. We give a recurrence extraction translation of this language into a recurrence language, a simply-typed lambda-calculus with a cost type, and state and prove a bounding logical relation expressing the correctness of this translation. The recurrence language has a denotational semantics in preorders, and we use this semantics to solve recurrences, e.g analyzing binary counters and splay trees. △ Less

Submitted 31 July, 2020; v1 submitted 26 June, 2020; originally announced June 2020.

Comments: To appear in ICFP 2020; formatting changes

ACM Class: F.3.1; F.3.2

Journal ref: Proc. ACM Program. Lang. 4, ICFP, Article 97 (August 2020)

A Generalization Error Bound for Multi-class Domain Generalization

Authors: Aniket Anand Deshmukh, Yunwen Lei, Srinagesh Sharma, Urun Dogan, James W. Cutler, Clayton Scott

Abstract: Domain generalization is the problem of assigning labels to an unlabeled data set, given several similar data sets for which labels have been provided. Despite considerable interest in this problem over the last decade, there has been no theoretical analysis in the setting of multi-class classification. In this work, we study a kernel-based learning algorithm and establish a generalization error b… ▽ More Domain generalization is the problem of assigning labels to an unlabeled data set, given several similar data sets for which labels have been provided. Despite considerable interest in this problem over the last decade, there has been no theoretical analysis in the setting of multi-class classification. In this work, we study a kernel-based learning algorithm and establish a generalization error bound that scales logarithmically in the number of classes, matching state-of-the-art bounds for multi-class classification in the conventional learning setting. We also demonstrate empirically that the proposed algorithm achieves significant performance gains compared to a pooling strategy. △ Less

Submitted 24 May, 2019; originally announced May 2019.

Simple Regret Minimization for Contextual Bandits

Authors: Aniket Anand Deshmukh, Srinagesh Sharma, James W. Cutler, Mark Moldwin, Clayton Scott

Abstract: There are two variants of the classical multi-armed bandit (MAB) problem that have received considerable attention from machine learning researchers in recent years: contextual bandits and simple regret minimization. Contextual bandits are a sub-class of MABs where, at every time step, the learner has access to side information that is predictive of the best arm. Simple regret minimization assumes… ▽ More There are two variants of the classical multi-armed bandit (MAB) problem that have received considerable attention from machine learning researchers in recent years: contextual bandits and simple regret minimization. Contextual bandits are a sub-class of MABs where, at every time step, the learner has access to side information that is predictive of the best arm. Simple regret minimization assumes that the learner only incurs regret after a pure exploration phase. In this work, we study simple regret minimization for contextual bandits. Motivated by applications where the learner has separate training and autonomous modes, we assume that the learner experiences a pure exploration phase, where feedback is received after every action but no regret is incurred, followed by a pure exploitation phase in which regret is incurred but there is no feedback. We present the Contextual-Gap algorithm and establish performance guarantees on the simple regret, i.e., the regret during the pure exploitation phase. Our experiments examine a novel application to adaptive sensor selection for magnetic field estimation in interplanetary spacecraft, and demonstrate considerable improvement over algorithms designed to minimize the cumulative regret. △ Less

Submitted 25 February, 2020; v1 submitted 16 October, 2018; originally announced October 2018.

Comments: The first two authors contributed equally

Kernel Embedding Approaches to Orbit Determination of Spacecraft Clusters

Authors: Srinagesh Sharma, James W. Cutler

Abstract: This paper presents a novel formulation and solution of orbit determination over finite time horizons as a learning problem. We present an approach to orbit determination under very broad conditions that are satisfied for n-body problems. These weak conditions allow us to perform orbit determination with noisy and highly non-linear observations such as those presented by range-rate only (Doppler o… ▽ More This paper presents a novel formulation and solution of orbit determination over finite time horizons as a learning problem. We present an approach to orbit determination under very broad conditions that are satisfied for n-body problems. These weak conditions allow us to perform orbit determination with noisy and highly non-linear observations such as those presented by range-rate only (Doppler only) observations. We show that domain generalization and distribution regression techniques can learn to estimate orbits of a group of satellites and identify individual satellites especially with prior understanding of correlations between orbits and provide asymptotic convergence conditions. The approach presented requires only visibility and observability of the underlying state from observations and is particularly useful for autonomous spacecraft operations using low-cost ground stations or sensors. We validate the orbit determination approach using observations of two spacecraft (GRIFEX and MCubed-2) along with synthetic datasets of multiple spacecraft deployments and lunar orbits. We also provide a comparison with the standard techniques (EKF) under highly noisy conditions. △ Less

Submitted 1 March, 2018; originally announced March 2018.

Comments: Submitted to JMLR