Trustworthy Systems

Per-thread compositional compilation for confidentiality-preserving concurrent programs

Authors

Rob Sison

DATA61

UNSW

Abstract

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 abstract and 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.

BibTeX Entry

  @inproceedings{Sison_18,
    address          = {Los Angeles},
    author           = {Sison, Robert},
    booktitle        = {2nd Workshop on Principles of Secure Compilation},
    date             = {2018-1-13},
    month            = jan,
    numpages         = {2},
    paperurl         = {https://trustworthy.systems/publications/full_text/Sison_18.pdf},
    publisher        = {Cătălin Hriţcu},
    title            = {Per-Thread Compositional Compilation for Confidentiality-Preserving Concurrent Programs},
    year             = {2018}
  }

Download