moose
moose copied to clipboard
Initial support for secrecy analysis
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.