Roadmap

Language Extensions

Availability Labels

Necessary to support more complicated replication schemes (e.g. quorum replication) and crypto with availability guarantees (e.g. MPC with output fairness).

Custom Datatypes

Need to support datatypes like Set for protocols like PSI. Might also want to support user-defined datatypes, which would look like restricted version of classes.

Downgrade Inference

Currently, downgrading boundaries must be explicitly defined in Viaduct source programs. It would be nice to determine these downgrading boundaries, which would make the effective label annotation burden of Viaduct programs to be zero---then the only labels that need to be written are the authority labels in the host configuration, which encodes the trust assumptions between parties. Prior work have used knowledge-based inference to determine what parts of an MPC computation can be hoisted out to plaintext computation. Recent work on "belief-programming" might also be relevant to determining downgrading boundaries.

Delegation

Extend source language and label inference algorithm.

See Silei's writeup for more information.

First-class object references

Current implementation of functions is very messy because object references are not really first-class. Would make this a lot cleaner if there are actual first-class object references in the language. Instead of syntactic restrictions that guarantee the protocol for a particular object is always known statically, can perform an alias analysis to enforce equality constraints during protocol selection---e.g. each object reference would be associated with an abstract identifier, and there would be a protocol that performs storage for an abstract identifier. Thus all objects with the same identifier are stored in the same protocol.

Persistence

Allow storage of data to persist across multiple executions of a Viaduct program.

Possible implementations:

input/output to "fake" hosts. To read persisted value x, do input x; to write to x, do output e to x.
persistent annotations on declarations: e.g. persistent var x: int{A}

Cost Profiling

Given a particular workload, determine whether to offload storage to remote machines and require the use of protocols like SGX, ORAM, or FHE. Would require knowledge about the size of inputs and then analysis to see how that propagates computation cost throughout the program.

Circuit Optimizations

Eliminate sources of overhead of ABY (MPC) back end.

Static Circuit Generation

Current implementation of ABY back end must compute transitive dependencies of an output gate, which can be costly if circuit is large. This dependency computation performs a topological sort of circuit components, and then builds the ABY circuit according to this order. Can avoid this overhead cost by statically generating the circuit ahead of time. Doing this would involve partially evaluating the compiled program to unroll loops and whatnot. (Building a good topological sort algorithm might help in the short term -- see the Polyglot dataflow analysis code.)

Multiple Outputs

Current implementation of ABY back end can only support execution of circuits with one output gate, whic (see k-means example in PLDI 2021 paper). Need to perform analysis for compiler to determine when outputs can be grouped together into one circuit. Can also extend source language to allow for multiple outputs at the same time.

New Backends

Hash-and-Salt

Can store salted hashes of data. The host performing storage should not be able to access the cleartext value of the data. The protocol can support equality checks between salted hashes and cleartext data.

Motivated by the password example, where the natural implementation is to store the password as a salted hash.

FHE

Would look something similar to MPC, but has different performance characteristics (high compute cost, low communication overhead).

ORAM

What are the labels?

Also need to find a library implementation. Might be easy enough to implement on our own.

Malicious MPC

Need to find a library. SCALE-MAMBA is its own virtual machine, unfortunately; maybe there is a library implementation of SPDZ?

Private Set Intersection

Need to extend source language with Custom Datatypes for this to work.

Library?

Trusted Enclaves (SGX)