Leveraging actors for privacy compliance.

Many organizations store and process personal information about the individuals with whom they interact. Because incorrect handling of this information can be harmful to those individuals, this information is often regulated by privacy policies. Although non-compliance can be costly, determining whether an organization's systems and processes actually follow these policies is challenging. It is our position, however, that such information systems could be formally verified if it is specified, designed, and implemented according to a methodology that prioritizes verifiability of privacy properties. This paper describes one such approach that leverages an actor-based architectural style, formal specifications of personal information that is allowed and required to be communicated, and a domain-specific actor-based language. Specifications at the system-, component- Actor-level are written using a first-order temporal logic. We propose that the software implementation be mechanically-checked against individual actor specifications using abstract interpretation. Whereas, consistency between the different specification levels and would be checked using model checking. By restricting our attention to programs using a specific actor-based style and implementation technology, we can make progress towards the very challenging problem of rigorously verifying program implementations against complex privacy regulations.