Formally ensuring the permissibility of obligations in security and privacy policies
Our society is becoming increasingly dependent on computer information systems for the management of personal information (e.g., medical records, financial data.). Organizations are required to manage and share such information in a manner that conforms to specific privacy regulations (e.g., the Health Insurance Portability and Accountability Act (HIPAA), the Gramm-Leach-Bliley Act (GLBA).). Privacy policies like HIPAA can impose restrictions based on the finite execution history (present requirements) and can also impose future requirements (obligations ). Existing work on checking compliance only investigates whether a certain action respects the present requirements of the policy or investigates whether a certain pending obligation is violated. However, when an obligation is violated they cannot report whether the user was not diligent or whether the policy did not permit the obligation. To this end, we formally specify a property of the policy which we call the Delta-property that statically guarantees that any incurred obligations can be met. When an obligation is violated according to a policy that has the Delta-property, it is safe to assume that the obligation violation is not due to a malformed policy. We prove that checking whether a policy has the Delta-property is undecidable in general. We then develop a sound, semi-automated technique to check whether a policy has the Delta-property under some constraints. We demonstrate the efficacy of our technique by verifying that our interpretation of the HIPAA privacy rule has the Delta-property.
Organizations that intend to be compliant with privacy policies need to rely on their own access control policies to safeguard their resources against unauthorized access. For instance, having access control policy to ensure only valid organization employees have access to the individual's personal information. These access control policies can allow access to a resource provided that the requesting user or some other user promises to perform some obligations. We are particularly interested in user obligations that can depend on and affect the authorization state of the system. Existing work introduces the property "accountability" that ensures that all the incurred user obligations are authorized. However, they assume that obligations cannot further incur other obligations (i.e., no cascading obligations). As a result, it significantly reduces the expressive power of their obligation model as it cannot express several real life scenarios. We show that deciding accountability in the most general case is NP-hard. We then consider several special yet practical cases of cascading obligations and provide a decision procedure for accountability in their presence.