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

Application domain/field

Type of tool

Synthesis tool

Expected input


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.


Uses KLEE as symbolic execution engine.
C Security Synthesis


- Repository: https://github.com/SPoS4/PoS4MPC

Related papers

https://doi.org/10.1007/978-3-031-13185-1 (CAV 2022)

Last publication date

7 August 2022

ProVerB specific

ProVerB is a part of SLEBoK. Last updated: February 2023.