Information systems that handle personal information must adhere to legal regulations, corporate privacy policies, and contractual agreements designed to protect personal privacy. Relying exclusively on application designers and developers for such assurances is unrealistic. There is a need for methods and tools that can identify errors in the handing of personal data and provide formal assurances that personal information is handled appropriately.
This project is developing a software development framework that uses novel language-based techniques to ensure that software enforces privacy policies. Privacy policies (based on legal and regulatory requirements) are formally specified in temporal logic, and identify circumstances under which information can be shared (based on criteria such as the roles of individuals involved, prior events, and whether the data has been aggregated) and future obligations that are incurred as a result of the information sharing. The framework consists of policy analysis tools, a programming language, program analysis tools that verify both privacy and declassification policies are enforced, and a runtime environment. Used in concert, these components produce distributed information systems that verifiably handle personal information appropriately.
The framework being developed by this project will address problems faced by many information systems. However, the project will focus especially on the needs of the medical industry, both with respect to patient records and clinical trials. As medical practice transitions to electronic medical records, the need for high-assurance systems becomes increasingly acute. This project will develop the capabilities needed to verify that electronic medical records systems comply with applicable privacy policies.
