Sat 13 Jan 2018 16:30 - 17:00 at Hershey - Session 3 Chair(s): Lars Birkedal

Recent work has demonstrated that per-thread compositional verification of value-dependent noninterference is feasible for concurrent programs. However, the gap remains that the verification of this (necessarily timing-sensitive) property for the source code of a program may not guarantee that the property still holds for that program once it has been compiled and is running on actual hardware. To this end, I have adapted and implemented in the Isabelle/HOL theorem prover an existing compilation scheme from a generic imperative While language to a generic RISC-style assembly language, and proved that my compiler preserves the compositional value-dependent noninterference property in question. As a proof of concept, I have exercised this compiler on a concurrent While model of the Cross Domain Desktop Compositor, and instantiated all of the related proofs of security for the compiled RISC-style assembly artifact of the system. In this talk I will expand on the details and immediate trajectory of this work, as well as discussing medium-to-long term plans and overarching objectives for my PhD thesis.

presentation slides handout (2018jan13-PriSC18_RobS_handout.pdf)5.25MiB
extended abstract (prisc18-paper2.pdf)177KiB
presentation slides (2018jan13-PriSC18_RobS_fix3.pdf)9.2MiB

Sat 13 Jan
Times are displayed in time zone: Tijuana, Baja California change

16:00 - 18:00: Session 3PriSC at Hershey
Chair(s): Lars BirkedalAarhus University
16:00 - 16:30
Talk
Constant-time WebAssembly
PriSC
John RennerUCSD, Sunjay CauligiUCSD, Deian StefanUniversity of California, San Diego
Pre-print File Attached
16:30 - 17:00
Talk
Per-Thread Compositional Compilation for Confidentiality-Preserving Concurrent Programs
PriSC
Robert SisonData61, CSIRO and UNSW
File Attached
17:00 - 17:30
Talk
On Compositional Compiler Correctness and Fully Abstract Compilation
PriSC
Daniel PattersonNortheastern University, Amal AhmedNortheastern University, USA
File Attached
17:30 - 18:00
Talk
Foundations of Dependent Interoperability
PriSC
Pierre-Evariste DagandLIP6/CNRS , Nicolas TabareauInria, France, Éric TanterUniversity of Chile
Link to publication File Attached