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.