Practical probability: Applying pGCL to lattice scheduling
Authors
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} }