Thesis / Dissertation

Proving Confidentiality and Its Preservation Under Compilation for Mixed-Sensitivity Concurrent Programs

Robert Sison, Carroll Morgan (ed.), Toby Murray (ed.), Kai Engelhardt (ed.)

Published : 2020

Abstract

Here, I pose the thesis that proving noninterference and its preservation by a compiler is feasible for mixed-sensitivity concurrent programs. Software does not always have the luxury of limiting itself to single-threaded computation with resources statically dedicated to each user to ensure the confidentiality of their data. Prior work therefore presented formal methods for proving and preserving the strictest kind of confidentiality property, noninterference, for mixed-sensitivity concurrent programs: a term I coin to describe those programs that might reuse memory shared between their threads to hold data of different sensitivity levels at different times. Although these methods addressed..

View full abstract