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.

extended abstract (prisc18-paper2.pdf)177KiB
presentation slides (2018jan13-PriSC18_RobS_fix3.pdf)9.1MiB