An actor-based framework for verifiable privacy policy enforcement: assume-guarantee specification of an actor-component architecture

Organizations that hold private information about individuals are required to obey privacy policies that dictate how that information can be handled. However, the systems that hold this information are often complex, and the organizations face the difficult task of ensuring that these systems behave correctly, or else face great penalty. A formal approach to solving this problem is to implement the information system in an actor-based architectural style that can be mechanically checked. This thesis aims to display the feasibility of this approach by developing privacy policy specifications for actors which can be provably composed to show that privacy policies are satisfied for the entire system. The contribution towards this goal is an actor-component architecture design for an Electronic Medical Record System, and a developed language for and implementation of assume-guarantee specifications for the actors which captures HIPAA-compliant behavior for a reasonable set of use cases. Finally, methods for evaluating the specifications are discussed and some intermediate steps are provided.