Lambda-RBAC: Programming with Role-Based Access Control
Radha Jagadeesan, Alan Jeffrey, Corin Pitcher, James Riely

TL;DR
This paper introduces Lambda-RBAC, a formal system with static analysis for role-based access control embedded in code, addressing safety and protection concerns for program components.
Contribution
It presents a formal calculus and static analysis framework for role-based access control within programming, enabling safety and protection verification.
Findings
Formal calculus for role-based access control
Static analysis for safety and protection
Addresses in-code role constraints
Abstract
We study mechanisms that permit program components to express role constraints on clients, focusing on programmatic security mechanisms, which permit access controls to be expressed, in situ, as part of the code realizing basic functionality. In this setting, two questions immediately arise: (1) The user of a component faces the issue of safety: is a particular role sufficient to use the component? (2) The component designer faces the dual issue of protection: is a particular role demanded in all execution paths of the component? We provide a formal calculus and static analysis to answer both questions.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.
Taxonomy
TopicsSecurity and Verification in Computing · Access Control and Trust · Logic, programming, and type systems
