arXiv subjects

John Kastner

Publications and source records attributed to John Kastner.

6 recordsLinked to original sources

arXiv2024

How We Built Cedar: A Verification-Guided Approach

This paper presents verification-guided development (VGD), a software engineering process we used to build Cedar, a new policy language for expressive, fast, safe, and analyzable authorization. Developing a system with VGD involves writing an executable model of the system and mechanically proving properties about the model; writing production code for the system and using differential random testing (DRT) to check that the production code matches the model; and using property-based testing (PBT) to check properties of unmodeled parts of the production code. Using VGD for Cedar, we can build fast, idiomatic production code, prove our model correct, and find and fix subtle implementation bugs that evade code reviews and unit testing. While carrying out proofs, we found and fixed 4 bugs in Cedar's policy validator, and DRT and PBT helped us find and fix 21 additional bugs in various parts of Cedar.

cs.SE↗

arXiv2024

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

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 typing 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.

cs.PL↗

arXiv2022

CoronaViz: Visualizing Multilayer Spatiotemporal COVID-19 Data with Animated Geocircles

While many dashboards for visualizing COVID-19 data exist, most separate geospatial and temporal data into discrete visualizations or tables. Further, the common use of choropleth maps or space-filling map overlays supports only a single geospatial variable at once, making it difficult to compare the temporal and geospatial trends of multiple, potentially interacting variables, such as active cases, deaths, and vaccinations. We present CoronaViz, a COVID-19 visualization system that conveys multilayer, spatiotemporal data in a single, interactive display. CoronaViz encodes variables with concentric, hollow circles, termed geocircles, allowing multiple variables via color encoding and avoiding occlusion problems. The radii of geocircles relate to the values of the variables they represent via the psychophysically determined Flannery formula. The time dimension of spatiotemporal variables is encoded with sequential rendering. Animation controls allow the user to seek through time manually or to view the pandemic unfolding in accelerated time. An adjustable time window allows aggregation at any granularity, from single days to cumulative values for the entire available range. In addition to describing the CoronaViz system, we report findings from a user study comparing CoronaViz with multi-view dashboards from the New York Times and Johns Hopkins University. While participants preferred using the latter two dashboards to perform queries with only a geospatial component or only a temporal component, participants uniformly preferred CoronaViz for queries with both spatial and temporal components, highlighting the utility of a unified spatiotemporal encoding. CoronaViz is open-source and freely available at http://coronaviz.umiacs.io.

cs.HC↗

arXiv2022

C to Checked C by 3C

Owing to the continued use of C (and C++), spatial safety violations (e.g., buffer overflows) still constitute one of today's most dangerous and prevalent security vulnerabilities. To combat these violations, Checked C extends C with bounds-enforced checked pointer types. Checked C is essentially a gradually typed spatially safe C - checked pointers are backwards-binary compatible with legacy pointers, and the language allows them to be added piecemeal, rather than necessarily all at once, so that safety retrofitting can be incremental. This paper presents a semi-automated process for porting a legacy C program to Checked C. The process centers on 3C, a static analysis-based annotation tool. 3C employs two novel static analysis algorithms - typ3c and boun3c - to annotate legacy pointers as checked pointers, and to infer array bounds annotations for pointers that need them. 3C performs a root cause analysis to direct a human developer to code that should be refactored; once done, 3C can be re-run to infer further annotations (and updated root causes). Experiments on 11 programs totaling 319KLoC show 3C to be effective at inferring checked pointer types, and experience with previously and newly ported code finds 3C works well when combined with human-driven refactoring.

cs.PL↗

arXiv2020

NewsStand CoronaViz: A Map Query Interface for Spatio-Temporal and Spatio-Textual Monitoring of Disease Spread

With the rapid continuing spread of COVID-19, it is clearly important to be able to track the progress of the virus over time in order to be better prepared to anticipate its emergence and spread in new regions as well as declines in its presence in regions thereby leading to or justifying "reopening" decisions. There are many applications and web sites that monitor officially released numbers of cases which are likely to be the most accurate methods for tracking the progress of the virus; however, they will not necessarily paint a complete picture. To begin filling any gaps in official reports, we have developed the NewsStand CoronaViz web application (https://coronaviz.umiacs.io) that can run on desktops and mobile devices that allows users to explore the geographic spread in discussions about the virus through analysis of keyword prevalence in geotagged news articles and tweets in relation to the real spread of the virus as measured by confirmed case numbers reported by the appropriate authorities. NewsStand CoronaViz users have access to dynamic variants of the disease-related variables corresponding to the numbers of confirmed cases, active cases, deaths, and recoveries (where they are provided) via a map query interface. It has the ability to step forward and backward in time using both a variety of temporal window sizes (day, week, month, or combinations thereof) in addition to user-defined varying spatial window sizes specified by direct manipulation actions (e.g., pan, zoom, and hover) as well as textually (e.g., by the name of the containing country, state or province, or county as well as textually-specified spatially-adjacent combinations thereof), and finally by the amount of spatio-temporally-varying news and tweet volume involving COVID-19.

cs.IR↗

arXiv2020

Equal Area Breaks: A Classification Scheme for Data to Obtain an Evenly-colored Choropleth Map

An efficient algorithm for computing the choropleth map classification scheme known as equal area breaks or geographical quantiles is introduced. An equal area breaks classification aims to obtain a coloring for the map such that the area associated with each of the colors is approximately equal. This is meant to be an alternative to an approach that assigns an equal number of regions with a particular range of property values to each color, called quantiles, which could result in the mapped area being dominated by one or a few colors. Moreover, it is possible that the other colors are barely discernible. This is the case when some regions are much larger than others (e.g., compare Switzerland with Russia). A number of algorithms of varying computational complexity are presented to achieve an equal area assignment to regions. They include a pair of greedy algorithms, as well as an optimal algorithm that is based on dynamic programming. The classification obtained from the optimal equal area algorithm is compared with the quantiles and Jenks natural breaks algorithms and found to be superior from a visual standpoint by a user study. Finally, a modified approach is presented which enables users to vary the extent to which the coloring algorithm satisfies the conflicting goals of equal area for each color with that of assigning an equal number of regions to each color.

cs.HC↗