[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