SCS Student Seminar Series / CS Speaking Skills Talk

Speaking Skills
Ph.D. Studentq
Computer Science Department
Carnegie Mellon University
Reasoning about Declassification in Epistemic Logic
Tuesday, April 22, 2014 - 12:00pm
McWilliams Classroom 4303 
Gates&Hillman Centers

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.

For More Information, Please Contact: