We have a new paper on dynamic enforcement of knowledge-based
privacy policies. In this setup, a user has some private information that untrusted
parties can query. The system tracks how receiving the answers to
queries affects the queriers' beliefs. Using a novel abstract domain
for tracking sets of probability distributions and performing Bayesian
inference, the system is able to ensure that a potential attacker's
uncertainty remains high across multiple queries.
Nov. 19, 2010
Just posted a new paper on proving the correctness of software updates that are applied at run-time. It's available here.
I am now back in Pittsburgh and working on my thesis and a POPL submission or two. I am also looking for jobs, so if you're hiring, please see my resume.
Off to Cambridge
I am currently in Cambridge, UK at MSR. If you're in Europe and want to talk about separation logic, numeric abstractions for heap programs, or verification in general, send me an email. I'll be around until the end of April.