Reference. Formally Verified Cloud-Scale Authorization

Aleks Chakarov, Jaco Geldenhuys, Matthew Heck, Michael Hicks, Sam Huang, Georges-Axel Jaloyan, Anjali Joshi, K. Rustan M. Leino, Mikael Mayer, Sean McLaughlin, Akhilesh Mritunjai, Clement Pit-Claudel, Sorawee Porncharoenwase, Florian Rabe, Marianna Rapoport, Giles Reger, Cody Roux, Neha Rungta, Robin Salkeld, Matthias Schlaipfer, Daniel Schoepe, Johanna Schwartzentruber, Serdar Tasiran, Aaron Tomb, Emina Torlak, Jean-Baptiste Tristan, Lucas Wagner, Michael W. Whalen, Remy Willems, Tongtong Xiang, Tae Joon Byun, Joshua Cohen, Ruijie Fang, Junyoung Jang, Jakob Rath, Hira Taqdees Syeda, Dominik Wagner, Yongwei Yuan · ICSE · 2025 · DOI · pldb

Cite
Cite as @chakarov-2025-formally (helia, typst) · \cite{chakarov-2025-formally} (LaTeX)
BibTeX
bibtex · 1 line
@inproceedings{chakarov-2025-formally, title={Formally Verified Cloud-Scale Authorization}, url={http://dx.doi.org/10.1109/icse55347.2025.00166}, DOI={10.1109/icse55347.2025.00166}, booktitle={2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE)}, publisher={IEEE}, author={Chakarov, Aleks and Geldenhuys, Jaco and Heck, Matthew and Hicks, Michael and Huang, Sam and Jaloyan, Georges-Axel and Joshi, Anjali and Leino, K. Rustan M. and Mayer, Mikael and McLaughlin, Sean and Mritunjai, Akhilesh and Pit-Claudel, Clement and Porncharoenwase, Sorawee and Rabe, Florian and Rapoport, Marianna and Reger, Giles and Roux, Cody and Rungta, Neha and Salkeld, Robin and Schlaipfer, Matthias and Schoepe, Daniel and Schwartzentruber, Johanna and Tasiran, Serdar and Tomb, Aaron and Torlak, Emina and Tristan, Jean-Baptiste and Wagner, Lucas and Whalen, Michael W. and Willems, Remy and Xiang, Tongtong and Byun, Tae Joon and Cohen, Joshua and Fang, Ruijie and Jang, Junyoung and Rath, Jakob and Syeda, Hira Taqdees and Wagner, Dominik and Yuan, Yongwei}, year={2025}, month=Apr, pages={2508–2521} }
hayagriva YAML (typst)
yaml · 51 lines
chakarov-2025-formally:
  type: article
  title: Formally Verified Cloud-Scale Authorization
  author:
  - Chakarov, Aleks
  - Geldenhuys, Jaco
  - Heck, Matthew
  - Hicks, Michael
  - Huang, Sam
  - Jaloyan, Georges-Axel
  - Joshi, Anjali
  - Leino, K. Rustan M.
  - Mayer, Mikael
  - McLaughlin, Sean
  - Mritunjai, Akhilesh
  - Pit-Claudel, Clement
  - Porncharoenwase, Sorawee
  - Rabe, Florian
  - Rapoport, Marianna
  - Reger, Giles
  - Roux, Cody
  - Rungta, Neha
  - Salkeld, Robin
  - Schlaipfer, Matthias
  - Schoepe, Daniel
  - Schwartzentruber, Johanna
  - Tasiran, Serdar
  - Tomb, Aaron
  - Torlak, Emina
  - Tristan, Jean-Baptiste
  - Wagner, Lucas
  - Whalen, Michael W.
  - Willems, Remy
  - Xiang, Tongtong
  - Byun, Tae Joon
  - Cohen, Joshua
  - Fang, Ruijie
  - Jang, Junyoung
  - Rath, Jakob
  - Syeda, Hira Taqdees
  - Wagner, Dominik
  - Yuan, Yongwei
  date: 2025-04
  page-range: 2508-2521
  url: http://dx.doi.org/10.1109/icse55347.2025.00166
  serial-number:
    doi: 10.1109/icse55347.2025.00166
  parent:
    type: proceedings
    title: 2025 IEEE/ACM 47th International Conference on Software Engineering (ICSE)
    publisher: IEEE
Download: chakarov-2025-formally.bib · chakarov-2025-formally.yml
Cited by (1)

Cazamariposas: Automated Instability Debugging in SMT-Based Program Verification zhou-2025-cazamariposasCADE · 2025
Program verification languages such as Dafny and F⋆ often rely heavily on Satisfiability Modulo Theories (SMT) solvers for proof automation. However, SMT-based verification suffers from instability, where semantically irrelevant changes in the source program can cause spurious proof failures. While existing mitigation techniques emphasize preemptive measures, we propose a complementary approach that focuses on diagnosing and repairing specific instances of instability-induced failures. Our key technique is a novel differential analysis to pinpoint problematic quantified formulas in an unstable query. We implement this technique in Cazamariposas, a tool that automatically identifies such quantified formulas and suggests fixes. We evaluate Cazamariposas on multiple large-scale systems verification projects written in three different program verification languages. Our results demonstrate Cazamariposas’ effectiveness as an instability debugger. In the majority of cases, Cazamariposas successfully isolates the issue to a single problematic quantifier, while providing a stabilizing fix.
DOI
Cites 71 works (2 here)
With notes (2)

Verus: Verifying Rust Programs using Linear Ghost Types lattuada-2023-verusOOPSLA · 2023
The Rust programming language provides a powerful type system that checks linearity and borrowing, allowing code to safely manipulate memory without garbage collection and making Rust ideal for developing low-level, high-assurance systems. For such systems, formal verification can be useful to prove functional correctness properties beyond type safety. This paper presents Verus, an SMT-based tool for formally verifying Rust programs. With Verus, programmers express proofs and specifications using the Rust language, allowing proofs to take advantage of Rust’s linear types and borrow checking. We show how this allows proofs to manipulate linearly typed permissions that let Rust code safely manipulate memory, pointers, and concurrent resources. Verus organizes proofs and specifications using a novel mode system that distinguishes specifications, which are not checked for linearity and borrowing, from executable code and proofs, which are checked for linearity and borrowing. We formalize Verus’ linearity, borrowing, and modes in a small lambda calculus, for which we prove type safety and termination of specifications and proofs. We demonstrate Verus on a series of examples, including pointer-manipulating code (an xor-based doubly linked list), code with interior mutability, and concurrent code.
PDF · DOI · arXiv · pldb

CakeML: A verified implementation of ML kumar_cakeml_2014POPL · 2014
We have developed and mechanically verified an ML system called CakeML, which supports a substantial subset of Standard ML. CakeML is implemented as an interactive read-eval-print loop (REPL) in x86-64 machine code. Our correctness theorem ensures that this REPL implementation prints only those results permitted by the semantics of CakeML. Our verification effort touches on a breadth of topics including lexing, parsing, type checking, incremental and dynamic compilation, garbage collection, arbitraryprecision arithmetic, and compiler bootstrapping.
PDF · DOI · pldb
External (69)
chakarov-2025-formally reference entries/refs/chakarov-2025-formally/chakarov-2025-formally.hel