Privacy-Sensitive Information Flow with JML

14 years 7 months ago
Privacy-Sensitive Information Flow with JML
In today's society, people have very little control over what kinds of personal data are collected and stored by various agencies in both the private and public sectors. We describe an approach to addressing this problem that allows individuals to specify constraints on the way their own data is used. Our solution uses formal methods to allow developers of software that processes personal data to provide assurances that the software meets the specified privacy constraints. In the domain of privacy, it is often not sufficient to express properties of interest as a relation between the input and output of a program as is done for general program correctness. Here we consider a stronger class of properties that allows us to express constraints on information flow. In particular, we can express that an algorithm does not leak any information from particular "sensitive" values. We describe a general methodology for expressing this kind of information flow property as Hoare-st...
Guillaume Dufay, Amy P. Felty, Stan Matwin
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2005
Where CADE
Authors Guillaume Dufay, Amy P. Felty, Stan Matwin
Comments (0)