ZKgen is a ZK platform that aggregates multiple ZK protocols into a single solution, giving the user the flexibility to chose which ZK protocol best fit its application scenario. It supports the evaluation of ZK relations written in SIEVE IR format.
EasyCrypt formalization and corresponding verified implementation of the Yao’s Secure Function Evaluation protocol.
The Pathkit toolset, that patches an ELF binary using one or more simple Python scripts.
EVOCrypt is a library that provides verified, high-assurance implementations of a series of cryptographic algorithms/protocols, including
EasyCrypt to OCaml extraction tool, focused on the functional core of EasyCrypt. It takes as input an EasyCrypt script and produces a WhyML file that matches the EasyCrypt file (and appropriate dependencies). Finally, it is possible to obtain verified OCaml code by relying on Why3 own extraction mechanism.
EasyCrypt formalization of the AWS Key Management Service.
The key features of ALICE are: i. automatically detecting and extracting implementations of weak or broken cryptographic primitives from binaries without requiring source code or debugging symbols; ii. identifying the context and scope in which such primitives are used, and performing program analysis to determine the effects of replacing such implementations with more secure ones; and iii. replacing implementations of weak primitives with those of stronger or more secure ones.