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.1MiB

Sat 13 Jan

prisc-2018
16:00 - 18:00: PriSC 2018 - Session 3 at Hershey
Chair(s): Lars BirkedalAarhus University
prisc-2018151585560000016:00 - 16:30
Talk
John RennerUCSD, Sunjay CauligiUCSD, Deian StefanUniversity of California, San Diego
Pre-print File Attached
prisc-2018151585740000016:30 - 17:00
Talk
Robert SisonData61, CSIRO and UNSW
File Attached
prisc-2018151585920000017:00 - 17:30
Talk
Daniel PattersonNortheastern University, Amal AhmedNortheastern University, USA
File Attached
prisc-2018151586100000017:30 - 18:00
Talk
Pierre-Evariste DagandLIP6/CNRS , Nicolas TabareauInria, France, √Čric TanterUniversity of Chile
Link to publication File Attached