Speaker
Ranjit Jhala
Abstract
We trust web applications with our most sensitive data: finances, health records, email, or even our political proclivities. While application developers go to great lengths to protect this data, the steady stream of news about data exfiltration shows that today's approach to safeguarding sensitive data by sprinkling access control checks throughout the application is not enough.
We present STORM, a new web framework that lets developers build model-view-controller (MVC) applications, with compile-time enforcement of security policies. With STORM, users specify all security policies in a declarative language, alongside the data model i.e. the description of the application database schema. Policies are logical assertions that describe which users are allowed to view, insert, or update particular rows and columns of each table in the database. STORM enforces these policies at compile-time by using refinement types to constrain STORM’s API with logical assertions that describe the data produced and consumed by the underlying operation and the users allowed access to that data.
We show that our centralized policy specification approach is expressive enough to describe a large suite of policies from the literature, including information flow control policies that had previously only been amenable to dynamic policy enforcement, and does so with modest annotation overhead for the programmer and zero run-time cost.
Bio
Ranjit Jhala is a professor of Computer Science and Engineering at the University of California, San Diego. He works on algorithms and tools that help engineer reliable computer systems. His work draws from and contributes to the areas of Model Checking, Program Analysis, and Automated Deduction, and Type Systems. He is fortunate to have helped create several influential systems including the BLAST software model checker, RELAY race detector, MACE/ MC distributed language and model checker, and Liquid Types. He received ACM SIGPLAN's Robin Milner Young Researcher Award in 2018.
Passcode: 583807; Video-off please during talk.
[Could not make it? Click on image below (soon) ↓ for recording]
