From fc3cdeaa198b6a6745625727dd8b1ef6c17db80d Mon Sep 17 00:00:00 2001 From: Kesha Hietala Date: Tue, 24 Sep 2024 11:31:13 -0600 Subject: [PATCH] add FSE paper + other small updates --- _config.yml | 4 ++-- _pages/about.md | 4 ++-- _pages/cv.md | 4 ++-- _publications/cedar-fse24.md | 14 ++++++++++++++ 4 files changed, 20 insertions(+), 6 deletions(-) create mode 100644 _publications/cedar-fse24.md diff --git a/_config.yml b/_config.yml index 87489c811fb4e..c0631accb3833 100644 --- a/_config.yml +++ b/_config.yml @@ -82,9 +82,9 @@ analytics: author: name : "Kesha Hietala" avatar : "profile.jpg" - bio : "Applied Scientist in Automated Reasoning" + bio : "Computer Science Researcher" location : - employer : "Amazon AWS" + employer : pubmed : googlescholar : "https://scholar.google.com/citations?user=SXWh3IYAAAAJ&hl=en" email : diff --git a/_pages/about.md b/_pages/about.md index 7fedbb795468f..d5b2c89422883 100644 --- a/_pages/about.md +++ b/_pages/about.md @@ -7,13 +7,13 @@ redirect_from: - /about.html --- -Hello! My name is Kesha, and I'm an Applied Scientist in the Automated Reasoning in Identity Group at Amazon AWS. +Hello! My name is Kesha. I'm interested in **compilers**, **program analysis** and **formal verification**. I got my PhD in 2022 in [Computer Science at the University of Maryland](https://www.cs.umd.edu/), where I was advised by [Mike Hicks](https://mhicks.me/). I did my undergraduate in [Computer Science at the University of Minnesota](https://cse.umn.edu/cs). For my dissertation, I designed and implemented SQIR, a *small quantum intermediate representation* embedded in the Coq proof assistant, and VOQC, a *verified optimizer for quantum circuits*. You can learn more about SQIR and VOQC in [this blog post](https://blog.sigplan.org/2021/06/02/verifying-a-quantum-compiler/), or you can check out [my dissertation](../files/drafts/khieta-dissertation.pdf). -At Amazon, I work on the [Cedar authorization language](https://www.cedarpolicy.com). +I spent two years as an Applied Scientist in the Automated Reasoning in Identity Group at Amazon (AWS) where I worked on the [Cedar authorization language](https://www.cedarpolicy.com). In my free time, I enjoy include puzzles, painting, and spending time with my three cats and husband, [Thomas Rolinger](https://www.researchgate.net/profile/Thomas_Rolinger). diff --git a/_pages/cv.md b/_pages/cv.md index 1265b304241a8..59f6e6455b574 100644 --- a/_pages/cv.md +++ b/_pages/cv.md @@ -18,7 +18,7 @@ redirect_from: * Minors in Mathematics and Asian Languages and Literatures (Japanese) ## Work experience -I joined AWS full time in July 2022. +I worked at Amazon (AWS) July 2022 - September 2024. During my time as a student, I was fortunate enough to have several internships: * Microsoft Quantum, Summer 2021 @@ -70,7 +70,7 @@ During my time as a student, I was fortunate enough to have several internships: ## Academic Service * PC member for Coq Workshop 2022, PLanQC 2022 & 2024, CPP 2024, ICFP 2024 -* AEC member & external reviewer for OOPSLA 2024 & 2024 +* AEC member & external reviewer for OOPSLA 2023 & 2024 * External reviewer for TQC 2020, MFCS 2022, PLDI 2023 * Sub-reviewer for CCS 2017, Oakland S&P 2017, RC 2019, PLDI 2020, QCTIP 2020, PLDI 2021, OOPSLA 2021 * Student volunteer at POPL 2020 diff --git a/_publications/cedar-fse24.md b/_publications/cedar-fse24.md new file mode 100644 index 0000000000000..16fd1cba5e0e8 --- /dev/null +++ b/_publications/cedar-fse24.md @@ -0,0 +1,14 @@ +--- +title: "How We Built Cedar: A Verification-Guided Approach" +collection: publications +permalink: /publications/cedar-fse24 +excerpt: +date: 2024-07-10 +venue: 'Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering (FSE)' +link: 'https://dl.acm.org/doi/abs/10.1145/3663529.3663854' +paperurl: 'https://arxiv.org/pdf/2407.01688' +github: 'https://github.com/cedar-policy' +citation: 'Craig Disselkoen, Aaron Eline, Shaobo He, Kyle Headley, Michael Hicks, Kesha Hietala, John Kastner, Anwar Mamat, Matt McCutchen, Neha Rungta, Bhakti Shah, Emina Torlak, Andrew Wells. "How We Built Cedar: A Verification-Guided Approach." Companion Proceedings of the 32nd ACM International Conference on the Foundations of Software Engineering (FSE). 2024.' +abstract: "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." +--- +Industry track paper