Uploaded image for project: 'Comdev GSOC'
  1. Comdev GSOC
  2. GSOC-243

[GSoC][Teaclave (incubating)] Data Privacy Policy Definition and Function Verification





      The Apache Teaclave (incubating) is a cutting-edge solution for confidential computing, providing Function-as-a-Service (FaaS) capabilities that enable the decoupling of data and function providers. Despite its impressive functionality and security features, Teaclave currently lacks a mechanism for data providers to enforce policies on the data they upload. For example, data providers may wish to restrict access to certain columns of data for third-party function providers. Open Policy Agent (OPA) offers flexible control over service behavior and has been widely adopted by the cloud-native community. If Teaclave were to integrate OPA, data providers could apply policies to their data, enhancing Teaclave’s functionality. Another potential security loophole in Teaclave is the absence of a means to verify the expected behavior of a function. This gap leaves the system vulnerable to exploitation by malicious actors. Fortunately, most of Teaclave’s interfaces can be reused, with the exception of the function uploading phase, which may require an overhaul to address this issue. Overall, the integration of OPA and the addition of a function verification mechanism would make Teaclave an even more robust and secure solution for confidential computing.


      If this proposal moves on smoothly, new functionality will be added to the Teaclave project that enables the verification of the function behavior that it strictly conforms to a prescribed policy.


      • 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.

      Timeline Estimation

      • 0.5 month: Policy language parser and/or policy language design (if Rego is not an ideal choice).
      • 1.5 − 2 months: Verification contracts rewriting on the function source code based on the policy parsed. • (∼ 1 month): The function can be properly verified formally (by, e.g., querying the Z3 SMT solver).

      Difficulty: Major
      Project size: ~350 hour (large)
      Potential mentors:
      Mingshen Sun, Apache Teaclave (incubating) PPMC, mssun@apache.org




            Unassigned Unassigned
            mssun Mingshen Sun
            0 Vote for this issue
            1 Start watching this issue