Have you ever wondered is there a way to compute without ever revealing the inputs? For example, you can use a mobile phone to navigate, without the server knowing where you actually are!

It is truly intriguing and has occurred to me several times. This problem, while easy to understand on the surface, turns out harder than I expected at first. I believe it's been studied extensively by crypto experts, but I know little about crypto so I don't even know the keyword to search with. I'll appreciate it if somebody could tell me something about this...

Nevertheless, I will describe my attempt below.

## Problem Statement

Intuitively: How to compute (evaluate a function) without the computer knowning the inputs?

One way to achieve this is to simply encrypt the input with a (public) key, and different users shall have different keys, so that the computer wouldn't have the chance to ever reveal the plaintext inputs. (I'd like to point out here, this is just one way I came up with upon, on which the rest of this article is based, and there might be other ways that I didn't think of.)

Simply put, given a function $f(x)$, an encryption algorithm $E(x)$, and a decryption $D(x)$, we would like to find a function $F(x)$, satisfying $D(F(E(x))) = f(x)$, where $E(x)$ and $D(x)$ depend on the user (the input provider). Since $E(x)$ and $D(x)$ should adopt the same encryption scheme, $D(E(x)) = x$ holds. Note that I intentionlly leave some details undefined.

It's easy to show that, if we could find a standardized procedure to find such a function $F$ for all $D(x)$ and $E(x)$, we would have solved this problem perfectly. However, this task is too terrifying, isn't it? I would be completely satisfied if I could find a solution when a specific encryption scheme is given.

## Trivial

Firstly, let's think about the trivial cases: what if $E(x)$ and $D(x)$ do absolutely nothing?

$$E(F(D(x))) = F(x) = f(x)$$

Similarly, if $f$ does nothing:

$$E(F(D(x))) = f(x) = x$$

We can just take $F(x) = x$.

## 1-bit, XOR, Not

Simple cases are not really simple, as you can build a Turing machine if it contains sufficiently powerful operations. I would like to know if we can build an adder with this "secure computation" thing. Let's start with NOT.

First consider only the symmetric XOR encryption, and let the variable $x$ to be boolean. The key is also boolean.

The original NOT function is defined as $f(x) = 1-x$, which negates the boolean variable. Simple truth-table computations show that, well, it's actually feasible! We can take $F(x) = x$.

The same reasoning can be applied to any $n$-bit vector easily.

## 2-bit, XOR, And

Now we've got NOT, let's see if we can solve for AND.

Here comes the first problem: how to represent a binary function? Easy, make the function take one argument which is a 2-bit vector, whose result is boolean. Unfortunately, this naive approach will get in the way of encryption, as encryption takes 2 bits as key, while the output only needs 1 bit, breaking the symmetry. But worry not, since both the key and the 1-bit vec can be padded to 2 bits, there is no problem.

Different from the 1-bit case, this time the truth table is much bigger. I didn't bother to check by hand, and just verified the assertion with Z3, which happens to support binary functions.

from z3 import *

x1, x2 = Bools('x1 x2')
k1, k2 = Bools('k1 k2')
F = Function('F', BoolSort(), BoolSort(), BoolSort())

s = Solver()
ForAll(x2,
ForAll(k1,
ForAll(k2,
Xor(F(Xor(x1, k1), Xor(x2, k2)), k2) == And(x1, x2))))))
if s.check() == sat:
print(s.model())


Since we pad consistently, the decryption only uses k2. What if we use asymmetrical XOR, where decryption uses an arbitrary function that fuses k1 and k2 together? Well, see for yourself, still no solution. What if we relax the condition, and only uses 1-bit key? While I strongly doubt the security and usefulness of such a crypto system, unfortunately, no solution found. Code:

from z3 import *

x1, x2 = Bools('x1 x2')
k = Bool('k')
F = Function('F', BoolSort(), BoolSort(), BoolSort())

s = Solver()
s.add(ForAll(k, ForAll(x1, ForAll(x2, Xor(F(Xor(x1, k), Xor(x2, k)), k) == And(x1, x2)))))
if s.check() == sat:
print(s.model())
else:
print('infeasible')


AND is just too powerful, I guess. :-/ Or maybe the universe just forbids us doing such kind of "secure computation"...

## RSA

From the constraint $E(F(D(x))) = f(x)$, we can conclude $F$ can preserve some information from $D$, and the information about private key is cancelled out by $E$.

I worked on the maths (omitted) when $f(x) = x + c$, but I don't know how to cancel out the private bits.

## Z3 to rescue

Z3 is a sophisticated SMT solver, which can solve large models in seconds. Z3 comes with its own Sexp-based DSL, but it's very quirky, so I used the Python binding. Well, it still sucks. Hey, maybe you could design a better DSL!

Generally speaking, we don't have to deal with arbitrarily large numbers, so I drove Z3 to check if there are any solutions when we only consider n-bit vector and don't specify a crypto (let z3 figure it out instead).

from z3 import *

def check(sz, f):
x, k = BitVecs('x k', sz)
k1, k2 = BitVecs('k1 k2', sz)
F = Function('F', BitVecSort(sz), BitVecSort(sz))
E = Function('E', BitVecSort(sz), BitVecSort(sz), BitVecSort(sz))
D = Function('D', BitVecSort(sz), BitVecSort(sz), BitVecSort(sz))

s = Solver()
And(D(k, E(k, x)) == x,                      # (1)
E(k, F(D(k, x))) == f(x)))))             # (2)
s.add(Not(ForAll(k1, ForAll(k2, ForAll(x, E(k1, x) == E(k2, x)))))) # (3)
if s.check() == sat:
print(s.model())

check(1, lambda x: 1-x)   # f(x) = Not(x)


Constraints explained:

1. Decrypting a encrypted message will return you the plaintext.
2. What "secure computation" is all about.
3. Rule out trivial cases, where E and D don't depend on the key at all.

(Constraint 3 tells us coding z3 is not as easy as it seems. Z3 will happily accept your formulae, but the validity remains unchecked for your specific scenarios. You just don't get it right easily. Actually, there were some bugs in my first attempt, and they weren't discovered until I started writing this article. Z3 is indeed a great listener...)

Believe it or not, this piece of code can automatically solve the problem at hand, giving you a solution when one is found, or reporting unsat when no solution is possible. However, it can take centuries to finish when sz is large.

Running the script above gives back the simple case we analyzed before: D(k,x) = E(k,x) = k^x, and f(x) = not x. Magic, right?

There are two problems with this approach.

1. The crypto is not flexible, as it comes "bundled" with the function we want to evaluate. This could lead z3 to finding an E or an D that encodes the computation in itself with F being a no-op. Absolutely against our will.
2. The crypto is symmetrical. To make it asymmetrical, we must write down the relation between a public key and a private key, in the language of first-order logic.

## Conclusion

This is an (unfinished) attempt, on which I spent about two hours of my spare time. There are still hundreds of problems yet to be solved or even proposed. Like, we know F must preserve information about D, but how much? Which class of functions can have solutions?

What about RSA? What about AND? Maybe our universe just forbids us doing such kind of computation, but there might be other ways around, I don't know.

I believe this topic has been extensively studied. Garbled circuits seem to be relevant, but I haven't understood the Wikipedia page on that subject so I can't say for sure...