[FM-India] IARCS Verification Seminar Series -- Talk by Ranjit Jhala on December 7, 1900 hrs IST

[VSS IARCS]

Dear all,

The next talk in the IARCS Verification Seminar Series will be given by
Ranjit Jhala, a Professor of Computer Science Engineering in the Jacobs
School of Engineering at the University of California, San Diego. The talk
is scheduled on Tuesday, December 7, at 1900 hrs IST. The details can be
found on the webpage (https://fmindia.cmi.ac.in/vss/), and also appended to
the body of this email.

The Verification Seminar Series, an initiative by the Indian Association
for Research in Computing Science (IARCS), is a monthly, online
talk-series, broadly in the area of Formal Methods and Programming
Languages, with applications in Verification and Synthesis. The aim of this
talk-series is to provide a platform for Formal Methods researchers to
interact regularly. In addition, we hope that it will make it easier for
researchers to explore newer problems/areas and collaborate on them, and
for younger researchers to start working in these areas.

All are welcome to join.


Best regards,
Deepak, Madhukar, Rahul, Srivathsan

=============================================================

Title: Refinement Types for Secure Web Applications

Meeting Link:
https://us02web.zoom.us/j/89164094870?pwd=eUFNRWp0bHYxRVpwVVNoVUdHU0djQT09
(Meeting ID: 891 6409 4870, Passcode: 082194)

Abstract: 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 evaluate STORM in three ways. First, we show that our centralized policy
specification approach is expressive enough to describe, often more
naturally, a large suite of policies from the literature. Second, we use
STORM to write statically verified implementations of several case studies
from the literature, including those that had previously only been amenable
to dynamic policy enforcement. We show the verification effort is modest:
the programmer needs to write 1 line of refinement type signatures per
20-30 lines of code (LOC). Third, we use STORM to build and deploy two new
end-to-end web applications for collaborative text editing and video-based
social interaction, that have been used at our university and at several
academic workshops, respectively. We demonstrate that STORM distills the
code that the developer has to get right down to compact, auditable
policies (under 70 LOC) that comprise under 1% of the application.

Bio: Ranjit Jhala is a Professor of Computer Science Engineering in the
Jacobs School of Engineering at the University of California, San Diego.
His research interest lies in Programming Languages and Software
Engineering, specifically, in techniques for building reliable computer
systems. His work draws from, combines and contributes to the areas of Type
Systems, Model Checking, Program Analysis and Automated Deduction.