Skip to main content

Practical probability: Applying pGCL to lattice scheduling


David Cock




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

    doi              = {10.1007/978-3-642-39634-2_23},
    booktitle        = {Proceedings of the 4th International Conference on Interactive Theorem Proving},
    month            = jul,
    paperurl         = {},
    slides           = {},
    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}