moose icon indicating copy to clipboard operation
moose copied to clipboard

Initial support for secrecy analysis

Open mortendahl opened this issue 3 years ago • 0 comments

We plan on using information flow analysis to allow users (and workers) to verify logical computations against a desired secrecy policy. However, we can also use it as an internal consistency check of the compiler, especially around our cryptographic protocols.

This issue is about the design and potential implementation of a first use of secrecy labels to annotate and check values as they're used in the system. Concretely, the goal might be to add labels to ring tensors and prf keys, and make sure that these are respected when placed. This would also likely require adding a declassify mechanism which must be explicitly called (in cryptographic kernels) when eg revealing data.

mortendahl avatar Aug 12 '21 12:08 mortendahl