PV2 ⊧ PoS4MPC: Policy Synthesis for MPCsynthesises security policy for secure multi-party computation

Application domain/field

• Synthesis
• Security policy
• Symbolic execution

Type of tool

Synthesis tool

Expected input

• MPC (multi-party computation) program

Format:

C program

Expected output

Computes a security policy for the given program such that the number of secret variables that are declared is as low as possible. The program is transformed into Obliv-C such that it can be compiled into executable implementations.

Internals

Uses KLEE as symbolic execution engine.