[Pl-seminar] Correction: Thu. 2/25 Seminar: Dominique Devriese, Reasoning about Object Capabilities with Logical Relations and Effect Parametricity

[William J. Bowman]

Correction: Seminar is on *Thursday* Feb. 25, 2016

--
William J. Bowman

On Sun, Feb 21, 2016 at 10:24:16PM -0500, Andrew Cobb wrote:
> FYI, 2/25 is a Thursday
> 
> William J. Bowman wrote:
> >NUPRL Seminar presents
> >
> >Dominique Devriese
> >Katholieke Universiteit Leuven
> >
> >13:30--14:50
> >Friday, Feb. 25, 2016
> >Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html)
> >Host: Amal Ahmed
> >
> >
> >Reasoning about Object Capabilities with Logical Relations and Effect Parametricity
> >
> >Abstract:
> >Object capabilities are a technique for fine-grained privilege separation in programming languages and systems,with important applications in security. However, current formal characterisations do not fully capture capability-safety of a programming language and are not sufficient for verifying typical applications. Using state-of-the-art techniques from programming languages research, we define a logical relation for a core calculus of JavaScript that better characterises capability-safety. The relation is powerful enough to reason about typical capability patterns and supports evolvable invariants on shared data structures, capabilities with restricted authority over them and isolated components with restricted communication channels. We use a novel notion of effect parametricity for deriving properties about effects. We demonstrate that our results imply memory access bounds that have previously been used to characterise capability-safety.
> >
> >
> >Bio:
> >Dominique is a postdoctoral researcher in the research group DistriNet, part of the Computer Science department of the Katholieke Universiteit Leuven. He holds a postdoctoral research fellowship of the Research Foundation - Flanders (FWO). He works on formalising properties of object-oriented and object-capability programming languages---specifically a property called effect parametricity--is the author of the grammar-combinators Haskell parsing library, and has added instance arguments to the programming language/proof assistant Agda. He is interested in information flow security, secure compilation,full abstraction, and functional and dependently typed programming languages.
> >
> >
> >
> >_______________________________________________
> >pl-seminar mailing list
> >pl-seminar at lists.ccs.neu.edu
> >https://lists.ccs.neu.edu/bin/listinfo/pl-seminar
> 
> -- 
>   Andrew
> 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: not available
URL: <http://lists.ccs.neu.edu/pipermail/pl-seminar/attachments/20160221/a77db5b3/attachment.pgp>