Skip to main content
CSIRO Logo Data 61 logo

Practical probability: Applying pGCL to lattice scheduling

Authors

David Cock

UNSW

NICTA

Abstract

Building on our published mechanisation of the probabilistic program logic pGCL we present a verified lattice scheduler, a standard covert-channel mitigation technique, employing randomisation as an elegant means of ensuring starvation-freeness. We show that this scheduler enforces probabilistic non-leakage, in addition to non-starvation. The refinement framework employed is compatible with that used in the L4.verified project, supporting our argument that full-scale verification of probabilistic security properties for realistic systems software is feasible.

BibTeX Entry

  @inproceedings{Cock_13,
    doi              = {10.1007/978-3-642-39634-2_23},
    booktitle        = {Proceedings of the 4th International Conference on Interactive Theorem Proving},
    month            = jul,
    paperurl         = {https://ts.data61.csiro.au/publications/nicta_full_text/6726.pdf},
    slides           = {http://ts.data61.csiro.au/publications/nicta_slides/6726.pdf},
    year             = {2013},
    keywords         = {side-channels pgcl security verification},
    title            = {Practical Probability: Applying {pGCL} to Lattice Scheduling},
    pages            = {1--16},
    author           = {Cock, David},
    address          = {Rennes, France}
  }

Download