[PRL] Practice Talk, TOMORROW 8/18 3:00pm in 366 WVH

William J. Bowman wilbowma at ccs.neu.edu
Mon Aug 17 13:43:47 EDT 2015


Hello all,

I am giving a practice talk for my ICFP talk tomorrow Aug. 18, 3:00pm, in 366 WVH. Please come criticize my talk.

Title: Noninterference for Free

Abstract:
The dependency core calculus (DCC) as a framework for studying a variety
of dependency analyses (e.g., secure information flow). The key property
provided by DCC is noninterference, which guarantees that a low-level
observer (attacker) cannot distinguish high-level (protected)
computations.  The proof of noninterference for DCC suggests a
connection to parametricity in System F, which suggests that it should
be possible to implement dependency analyses in languages with
parametric polymorphism.

We present a translation from DCC into Fω and prove that the translation
preserves noninterference.  To express noninterference in Fω we define a
notion of observer-sensitive equivalence that makes essential use of
both first-order and higher-order polymorphism.  Our translation
provides insights into DCC's type system and shows how DCC can be
implemented in a polymorphic language without loss of the
security/noninterference guarantees available in DCC.  Our contributions
include proof techniques that should be valuable when proving other
secure compilation or full abstraction results.

-- 
William J. Bowman
Northeastern University
College of Computer and Information Science
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 819 bytes
Desc: not available
URL: <http://lists.ccs.neu.edu/pipermail/prl/attachments/20150817/97f1dba5/attachment.pgp>


More information about the PRL mailing list