research-article

Public Access

Verifiable Assume-Guarantee Privacy Specifications for Actor Component Architectures

Authors:

Claiborne Johnson,

Thomas MacGahan,

Jeffery von Ronne,

Jianwei NiuAuthors Info & Claims

SACMAT '17 Abstracts: Proceedings of the 22nd ACM on Symposium on Access Control Models and Technologies

Pages 167 - 178

https://doi.org/10.1145/3078861.3078873

Published: 07 June 2017 Publication History

Abstract

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.

References

[1]

1999. Federal Trade Commission, How to comply with the children's online privacy protection rule. (1999). Public Law.

[2]

1999. Senate Banking Committee, Gramm-Leach-Bliley Act. (1999). Public Law 106--102.

[3]

Gul A. Agha, Ian A. Mason, Scott F. Smith, and Carolyn L. Talcott. 1997. A foundation for actor computation. Journal of Functional Programming 7, 01 (1997), 1--72. arXiv:http://journals.cambridge.org/article_S095679689700261X

Digital Library

[4]

Bowen Alpern and Fred B. Schneider. 1987. Recognizing safety and liveness. Distributed Computing 2 (1987), 117--126. Issue 3.

Digital Library

[5]

Paul Ashley, Satoshi Hada, Gijnter Karjoth, Calvin Powers, and Matthias Schunter. 2003. Enterprise Privacy Authorization Language (EPAL 1.2). (November 2003). W3C Member Submission.

[6]

Adam Barth, Anupam Datta, John C. Mitchell, and Helen Nissenbaum. 2006. Privacy and Contextual Integrity: Framework and Applications. In IEEE Symposium on Security and Privacy. IEEE Computer Society, Washington, DC, USA, 184--198.

Digital Library

[7]

Lujo Bauer, Jarred Ligatti, and David Walker. 2002. More Enforceable Security Policies. In Foundations of Computer Security.

[8]

Travis Breaux and Annie Antón. 2008. Analyzing Regulatory Rules for Privacy and Security Requirements. IEEE Trans. Softw. Eng. 34, 1 (2008), 5--20.

Digital Library

[9]

Omar Chowdhury, Andreas Gampe, Jianwei Niu, Jeffery von Ronne, Jared Bennatt, Anupam Datta, Limin Jia, and William H. Winsborough. 2013. Privacy promises that can be kept: A policy analysis method with application to the HIPAA privacy rule. In Proceedings of the 18th ACM symposium on Access control models and technologies. ACM, 3--14.

Digital Library

[10]

A. Cimatti, E. Clarke, F. Giunchiglia, and M. Roveri. 2000. NuSMV: A New Symbolic Model Checker. International Journal of Software Tools for Technology Transfer 2 (2000), 410--425.

[11]

Nicodemos Damianou, Naranker Dulay, Emil Lupu, and Morris Sloman. 2001. The Ponder Policy Specification Language. In POLICY. Springer-Verlag, London, UK, 18--38.

Digital Library

[12]

E. Allen Emerson. 1990. Temporal and modal logic. In Handbook of theoretical computer science, Jan van Leeuwen (Ed.). MIT Press, Cambridge, MA, USA, 995--1072. http://portal.acm.org/citation.cfm?id=114891.114907

Digital Library

[13]

E. Allen Emerson and Kedar S. Namjoshi. 1995. Reasoning about rings. In POPL '95.

Digital Library

[14]

Klaus Havelund and Grigore Roşu. 2004. Efficient monitoring of safety properties. Int. J. Softw. Tools Technol. Transf. 6 (2004), 158--173. Issue 2.

Digital Library

[15]

Carl Hewitt. 1977. Viewing control structures as patterns of passing messages. Artificial Intelligence 8, 3 (1977), 323 -- 364.

Digital Library

[16]

HIPAA 1996. Health Insurance Portability and Accountability Act (HIPAA). (1996). (42 U.S.C. §300gg, 29 U.S.C §1181 et seq., and 42 U.S.C §1320d et seq.; 45 CFR Parts 144, 146, 160 162, and 164).

[17]

Claiborne Johnson. 2016. An Actor-Based Framework for Verifiable Privacy Policy Enforcement: Assume-Guarantee Specification of an Actor-Component Architecture. Master's thesis. University of Texas at San Antonio.

[18]

Bengt Jonsson and Tsay Yih-Kuen. 1996. Assumption/guarantee specifications in linear-time temporal logic. Theoretical Computer Science 167, 1-2 (1996), 47--72.

Digital Library

[19]

Karl Krukow, Mogens Nielsen, and Vladimiro Sassone. 2008. A Logical Framework for History-based Access Control and Reputation Systems. J. Comput. Secur. 16, 1 (Jan. 2008), 63--101. http://dl.acm.org/citation.cfm?id=1370684.1370686

Digital Library

[20]

L. Lamport. 1977. Proving the Correctness of Multiprocess Programs. IEEE Transactions on Software Engineering 3, 2 (1977), 125--143.

Digital Library

[21]

Martin Leucker and Christian Schallhart. 2009. A brief account of runtime verification. Journal of Logic and Algebraic Programming 78, 5 (2009), 293--303. The 1st Workshop on Formal Languages and Analysis of Contract-Oriented Software (FLACOS'07).

[22]

Jay Ligatti, Lujo Bauer, and David Walker. 2009. Run-Time Enforcement of Nonsafety Policies. ACM Trans. Inf. Syst. Secur. 12, Article 19 (January 2009), 41 pages. Issue 3.

Digital Library

[23]

Thomas MacGahan. 2016. Towards Verifiable Privacy Policy Compliance of an Actor-Based Electronic Medical Records System: An extension to the HAPL language focused on exposing a user interface. Master's thesis. University of Texas at San Antonio.

[24]

Thomas MacGahan, Claiborne Johnson, Armando Rodriguez, Jeffery von Ronne, and Jianwei Niu. 2017. Provable Enforcement of HIPAA-Compliant Release of Medical Records Using the History Aware Programming Language. In Proceedings of 22nd ACM Symposium on Access Control Models and Technologies, 10.

Digital Library

[25]

Michael J. May, Carl A. Gunter, and Insup Lee. 2006. Privacy APIs: Access Control Techniques to Analyze and Verify Legal Privacy Policies. In CSFW. IEEE Computer Society, Washington, DC, USA, 85--97.

Digital Library

[26]

A. Pnueli. 1977. The Temporal Logic of Programs. In Proceedings of the 18th IEEE Symposium on Foundations of Computer Science, Vol. 526. 46--67.

Digital Library

[27]

Fred B. Schneider. 2000. Enforceable security policies. ACM Transactions on Information and System Security 3 (2000), 2000.

Digital Library

[28]

A. Prasad Sistla. 1994. Safety, liveness and fairness in temporal logic. Formal Aspects of Computing 6 (1994), 495--511. Issue 5.

[29]

Jeffery von Ronne. 2012. Leveraging actors for privacy compliance. In Proceedings of the 2nd edition on Programming systems, languages and applications based on actors, agents, and decentralized control abstractions. ACM, 133--136.

Digital Library

Cited By

MacGahan TJohnson CRodriguez Avon Ronne JNiu JBertino ESandhu RWeippl E(2017)Provable Enforcement of HIPAA-Compliant Release of Medical Records Using the History Aware Programming LanguageProceedings of the 22nd ACM on Symposium on Access Control Models and Technologies10.1145/3078861.3084176(191-198)Online publication date: 7-Jun-2017
https://dl.acm.org/doi/10.1145/3078861.3084176

Index Terms

Verifiable Assume-Guarantee Privacy Specifications for Actor Component Architectures

Recommendations

Provable Enforcement of HIPAA-Compliant Release of Medical Records Using the History Aware Programming Language
SACMAT '17 Abstracts: Proceedings of the 22nd ACM on Symposium on Access Control Models and Technologies

Dependence on reliable information systems to safeguard personally identifiable information implies a need for privacy policies which guide the release and management of such information, whose mismanaged disclosure can be damaging to both the subject ...
Privacy promises that can be kept: a policy analysis method with application to the HIPAA privacy rule
SACMAT '13: Proceedings of the 18th ACM symposium on Access control models and technologies

Organizations collect personal information from individuals to carry out their business functions. Federal privacy regulations, such as the Health Insurance Portability and Accountability Act (HIPAA), mandate how this collected information can be shared ...
Privacy policies verification in composite services using OWL

Privacy has been an important issue for online services collecting customer data. P3P is a privacy policy language with a fixed vocabulary to express privacy practices of online services. The matching between the privacy practices (P3P policies) and ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

SACMAT '17 Abstracts: Proceedings of the 22nd ACM on Symposium on Access Control Models and Technologies

June 2017

276 pages

ISBN:9781450347020

DOI:10.1145/3078861

General Chair:
Elisa Bertino
Purdue University, USA
,
Program Chairs:
Ravi Sandhu
University of Texas at San Antonio, USA
,
Edgar Weippl
SBA Research, Austria

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

SIGSAC: ACM Special Interest Group on Security, Audit, and Control

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 June 2017

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

NSF

Conference

SACMAT'17

Sponsor:

SIGSAC

SACMAT'17: The 22nd ACM Symposium on Access Control Models and Technologies

June 21 - 23, 2017

Indiana, Indianapolis, USA

Acceptance Rates

SACMAT '17 Abstracts Paper Acceptance Rate 14 of 50 submissions, 28%;

Overall Acceptance Rate 177 of 597 submissions, 30%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

1
Total Citations
View Citations
200
Total Downloads

Downloads (Last 12 months)43
Downloads (Last 6 weeks)7

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

MacGahan TJohnson CRodriguez Avon Ronne JNiu JBertino ESandhu RWeippl E(2017)Provable Enforcement of HIPAA-Compliant Release of Medical Records Using the History Aware Programming LanguageProceedings of the 22nd ACM on Symposium on Access Control Models and Technologies10.1145/3078861.3084176(191-198)Online publication date: 7-Jun-2017
https://dl.acm.org/doi/10.1145/3078861.3084176

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents