Noninterference (NI) defines a program to be secure if changes to high-security inputs cannot alter low-security outputs. NI indirectly states the epistemic property that the low-security outputs do not include knowledge obtained from the high-security inputs. However, NI is too restrictive a property to incorporate declassification of some high-security inputs and not others. By reasoning about declassification in epistemic logic, we express what knowledge is obtained through the execution of a program by the declassifications. Therefore, as a consequence of the adequacy of the epistemic logic for modeling the program behavior, we can still derive some NI-like properties for those high inputs that have not been declassified. In this talk, I will present our formulation of declassification and explain how it affects the epistemic properties of programs.
Joint work with Robert Harper.
In partial fulfillment of the CS Speaking Skills Requirement.
deb [atsymbol] cs.cmu.edu