Privacy verification tool

Patent metadata

Field	Value
Publication number	US-9996704-B2
Application number	US-201514639329-A
Country	US
Kind code	B2
Filing date	Mar 5, 2015
Priority date	Mar 15, 2013
Publication date	Jun 12, 2018
Grant date	Jun 12, 2018

Abstract

Systems and methods for protecting the privacy of users by controlling access to the users' data. In particular, some embodiments provide for a higher-level declarative language for expressing privacy policies which can be verified using a computer-aided verification tool. The verification tool uses the expressed privacy policies along with language-level assumptions and assertions in the verification process. For example, high-level models of the privacy policies can be reduced to a simpler verification representation (e.g., a Boolean representation) based on a set of assertions. This verification representation can then be submitted to a constraint solver (e.g., Satisfiability Modulo Theories solver) for verification.

First claim

What is claimed is:

1. A method comprising:
receiving a request for accessing data stored in a storage location;
in an event of a failure in retrieving data stored in the storage location, determining whether the failure is associated with an entirety of the request or a portion of the request;
upon determining that the failure is associated with the portion of the request:
retrieving, from Hall the storage location, a storage and privacy service (SPS) program expressing one or more access control rules;
granting, based on the SPS program, access to data that is retrievable from the storage location;
generating, using a processor, a verification representation representing an abstraction of the SPS program based on one or more assertions;
submitting the verification representation to a constraint solver to generate a set of access control outputs; and
determining if the set of access control outputs returned from the constraint solver satisfy a desired set of privacy constraints in view of the one or more assertions.

2. The method of claim 1 , further comprising generating one or more suggestions to fix the SPS program if the set of access control outputs do not satisfy the desired set of privacy constraints.

3. The method of claim 1 , wherein generating the verification representation of the SPS program includes evaluating and abstracting the SPS program based on the one or more assertions.

4. The method of claim 1 , wherein generating the verification representation includes generating an intermediate representation by evaluating the SPS program by substituting constants, functions, and let-bound expressions.

5. The method of claim 4 , wherein generating the verification representation further includes transforming an intermediate representation of the SPS program into a Boolean representation and an integer representation.

6. The method of claim 1 , wherein generating the verification representation includes reducing the program to a Boolean satisfiability problem.

7. The method of claim 1 , wherein the SPS program includes one or more nodes that identify properties, edges, and node variables.

8. The method of claim 7 , wherein the one or more nodes identify node field access, data structure traversals, arithmetic operations, or Boolean operations.

9. The method of claim 1 , wherein the determining that the failure is associated with the portion of the request includes identifying that a portion of the data that access is requested for is un-retrievable.

10. A system comprising:
a memory;
a database having stored thereon a program written in a declarative language used to enforce a set of privacy policies; and
one or more processors configured to:
receive a request for accessing data stored in the database;
in an event of a failure in retrieving data stored in the database, determine whether the failure is associated with an entirety of the request or a portion of the request;
upon determining that the failure is associated with the portion of the request:
retrieve the program written in the declarative language used to enforce the set of privacy policies;

grant, based on the program, access to data that is retrievable from the database;
generate a verification representation of the program, wherein the verification representation represents an abstraction of the program based on one or more assertions; and
search over the verification representation to determine if the program satisfies the set of privacy policies in view of the one or more assertions.

11. The system of claim 10 , wherein the one or more processors are further configured to reduce the program to a Boolean satisfiability problem.

12. The system of claim 10 , wherein the verification representation includes an intermediate representation of the program into a Boolean representation and an integer representation.

13. The system of claim 10 , wherein the one or more processors are further configured to generate the one or more assertions.

14. The system of claim 13 , wherein the one or more processors are further configured to receive the one or more assertions and abstract the program based on the one or more assertions.

15. The system of claim 10 , wherein the one or more processors are further configured to generate one or more suggestions for updating the program when a determination is made that the program does not satisfy the set of privacy policies.

16. The system of claim 10 , further comprising a graphical user interface, under the control of the one or more processors, configured to aid a user in creating and testing the program.

17. A computer-implemented method comprising:
receiving a request for accessing data stored in a storage location;
in an event of a failure in retrieving data stored in the storage location, determining whether the failure is associated with an entirety of the request or a portion of the request;
upon determining that the failure is associated with the portion of the request:
retrieving, from a storage location, a storage and privacy service (SPS) program expressing one or more access control rules defining data access within a social networking system;
granting, based on the SPS program, access to data that is retrievable from the storage location;
receiving one or more assertions to test compliance of the SPS program in view of a set of privacy constraints;
generating, using a processor, a logical representation of the SPS program based on the one or more assertions, wherein the logical representation represents an abstraction of the SPS program based on the one or more assertions and includes Boolean variables; and
searching over assignments to the Boolean variables in the logical representation of the SPS program to determine if the SPS program satisfies the privacy constraints in view of the one or more assertions.

18. The computer-implemented method of claim 17 , wherein searching over the assignments includes submitting the logical representation to a constraint solver to generate a set of access control responses of the SPS program in view of the one or more assertions.

19. The computer-implemented method of claim 17 , further comprising generating a graphical user interface that includes one or more suggestions to fix the SPS program if the SPS program does not satisfy the privacy constraints.

20. The computer-implemented method of claim 17 , wherein generating the logical representation of the SPS program includes generating an intermediate representation by evaluating the SPS program by substituting constants, functions, and let-bound expressions.

21. The computer-implemented method of claim 20 , wherein generating the verification representation further includes transforming the intermediate representation into a Boolean and integer representation.

22. The system of claim 10 , wherein the determining that the failure is associated with the portion of the request includes identifying that a portion of the data that access is requested for is un-retrievable.

23. The computer-implemented method of claim 17 , wherein the determining that the failure is associated with the portion of the request includes identifying that a portion of the data that access is requested for is un-retrievable.

Assignees

• Facebook Inc

Inventors

• Heise Stephen Charles
• Yang Jean
• Reeves Dwayne
• Jia Yiding

Classifications

• G06F2221/2101

  Auditing as a secondary aspect · CPC title

• G06F21/6245 Primary

  Protecting personal data, e.g. for financial or medical purposes · CPC title

• H04L63/102

  Entity profiles · CPC title

• G06F21/6227 Primary

  where protection concerns the structure of data, e.g. records, types, queries · CPC title