Authorization is a challenge in multi-user systems that requires determining who can access specific resources. When authorization logic is embedded within application code, permissions become difficult to audit and maintain over time. Cedar is an open-source authorization language that externalizes access control into dedicated policies, making authorization logic more transparent and reusable across applications. Cedar is designed to balance four competing goals: expressiveness, performance, safety, and analyzability. Cedar's syntax allows developers to naturally express access control based on roles and attributes, supporting role-based, attribute-based, and relation-based models with an intuitive syntax. Cedar helps policy authors write correct policies through a type system to detect common mistakes and provides a sound and complete logical encoding. Cedar is implemented in Rust with code available at https://github.com/cedar-policy, formally verified in Lean to ensure correctness, and is currently in use at cloud scale in Amazon Verified Permissions. This talk will present the motivation for and the design of Cedar, and share lessons learned from the verification-guided development process used to build Cedar.

OBJECTIVE: The COVID-19 pandemic emphasized the value of geospatial visual analytics for both epidemiologists and the general public. However, systems struggled to encode temporal and geospatial trends of multiple, potentially interacting variables, such as active cases, deaths, and vaccinations. We sought to ask (1) how epidemiologists interact with visual analytics tools, (2) how multiple, time-varying, geospatial variables can be conveyed in a unified view, and (3) how complex spatiotemporal encodings affect utility for both experts and non-experts. MATERIALS AND METHODS: We propose encoding variables with animated, concentric, hollow circles, allowing multiple variables via color encoding and avoiding occlusion problems, and we implement this method in a browser-based tool called CoronaViz. We conduct task-based evaluations with non-experts, as well as in-depth interviews and observational sessions with epidemiologists, covering a range of tools and encodings. RESULTS: Sessions with epidemiologists confirmed the importance of multivariate, spatiotemporal queries and the utility of CoronaViz for answering them, while providing direction for future development. Non-experts tasked with performing spatiotemporal queries unanimously preferred animation to multi-view dashboards. DISCUSSION: We find that conveying complex, multivariate data necessarily involves trade-offs. Yet, our studies suggest the importance of complementary visualization strategies, with our animated multivariate spatiotemporal encoding filling important needs for exploration and presentation. CONCLUSION: CoronaViz's unique ability to convey multiple, time-varying, geospatial variables makes it both a valuable addition to interactive COVID-19 dashboards and a platform for empowering experts and the public during future disease outbreaks. CoronaViz is open-source and a live instance is freely hosted at http://coronaviz.umiacs.io.

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.

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.

Online sources of news have steadily supplanted their paper counterparts alongside the growth of the internet. This growth in online news has led to a surplus of data in the form of the text of news articles published online. While an abundance of data is obviously desirable, it can make it difficult for a human to analyze and find trends in the data without assistance. The application demonstrated in the paper aims to aid users in such analysis by building a spatio-textual and spatiotemporal data visualization based on the existing NewsStand architecture. The application is shown to be applicable to tracking the changing geographic prevalence of a disease (e.g., COVID-19) over time.