Declassification and Authorization in Epistemic Logic
Friday, October 3rd, 2014 from 12-1 pm in GHC 4303.
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. Moreover, the epistemic logic we choose can also express authorization policies for when a declassification may occur. When knowledge reasoning is combined with authorization in a single logic, we can derive properties of knowledge flows such as the lemma that the derivation that knowledge is declassified must include the proof that the declassification is authorized. In this talk, I will present our formulation of declassification and authorization and outline how we prove interesting epistemic properties of programs that go beyond NI.
The Student Seminar Series is an informal research seminar by and for SCS graduate students from noon to 1 pm on Tuesdays and Fridays. Lunch is provided by the Computer Science Department (personal thanks to Sharon Burks and Debbie Cavlovich!). At each meeting, a different student speaker will give an informal, 40-minute talk about his/her research, followed by questions/suggestions/brainstorming. We try to attract people with a diverse set of interests, and encourage speakers to present at a very general, accessible level.
So why are we doing this and why take part? In the best case scenario, this will lead to some interesting cross-disciplinary work among people in different fields and people may get some new ideas about their research. In the worst case scenario, a few people will practice their public speaking and the rest get together for a free lunch.
Note: Step #1 below are applicable to all SSS speakers. You can schedule AT MOST THREE talks per semester.
SSS is an ideal forum for SCS students to give presentations that count toward fulfilling their speaking requirements. The specifics, though, vary with each department. For instance, students in CSD will need to be familiar with the notes in Section 8 of the Ph.D. document and follow the instructions outlined on the Speakers Club homepage. Roughly speaking, these are the steps:
Armaghan Naik, Computational Biology