Visible to the public Verifiable Assume-Guarantee Privacy Specifications for Actor Component Architectures

TitleVerifiable Assume-Guarantee Privacy Specifications for Actor Component Architectures
Publication TypeConference Paper
Year of Publication2017
AuthorsJohnson, Claiborne, MacGahan, Thomas, Heaps, John, Baldor, Kevin, von Ronne, Jeffery, Niu, Jianwei
Conference NameProceedings of the 22Nd ACM on Symposium on Access Control Models and Technologies
Conference LocationNew York, NY, USA
ISBN Number978-1-4503-4702-0
Keywordsassume-guarantee specifications, first-order linear temporal logic, Human Behavior, policy, privacy, Privacy Policies, privacy policy, pubcrawl, safety and liveness properties, Scalability, static analysis

Many organizations process personal information in the course of normal operations. Improper disclosure of this information can be damaging, so organizations must obey privacy laws and regulations that impose restrictions on its release or risk penalties. Since electronic management of personal information must be held in strict compliance with the law, software systems designed for such purposes must have some guarantee of compliance. To support this, we develop a general methodology for designing and implementing verifiable information systems. This paper develops the design of the History Aware Programming Language into a framework for creating systems that can be mechanically checked against privacy specifications. We apply this framework to create and verify a prototypical Electronic Medical Record System (EMRS) expressed as a set of actor components and first-order linear temporal logic specifications in assume-guarantee form. We then show that the implementation of the EMRS provably enforces a formalized Health Insurance Portability and Accountability Act (HIPAA) policy using a combination of model checking and static analysis techniques.

Citation Keyjohnson_verifiable_2017