Data Privacy Policy Definition and Function Verification for Teaclave

Teaclave currently lacks a mechanism for data providers to enforce policies on the data they upload, and also it cannot verify that the behavior of the uploaded function conforms to the expected rules. These two gaps leave the system vulnerable to exploitation by malicious actors. To solve the problem, verification should be exerted on the uploaded function so that its behavior that it strictly conforms to a prescribed policy. The standard formal verifier can be adopted (e.g., Prusti, Creusot) to formally verify the function's behavior. A set of deliverables as follows can be anticipated in the coming future. Milestones: Basic policies (e.g., addition, subtraction) of the data can be verified by Teaclave; Complex policies can be verified. Components: Verifier for the function code; Policy language adapters (adapt policy language to verifier); Policy language parser; Function source code converter (append policies to the functions). Documentation: The internal working mechanism of the verification; How to write policies for the data.