sangel

This is the entire formal verification effort, as far as I can tell: https://codeberg.org/gregburd/aether/src/branch/main/aether/...

They use TLA+ with TLC which model checks the write ahead log (a component of the system). But that only models the WAL protocol, not the actual Rust code and not the other 99% of the system.

Any formal verification is of course awesome to see though.

My totally uneducated guess is that they leak exaggerated numbers on purpose to make the real numbers look less bad in comparison. The idea being that a few days before the official news everyone is talking about a potential 30 or 40K people layoff. Then, when the official news come out and state that they are laying off 14K people, it sounds less dramatic (in relative terms). This makes people (who are not affected by this) to feel like the news were overblown and are not as significant.

Obviously not. Suppose the input to my function is a 64-bit integer. My test cannot possibly try every possible 64-bit integer. It would take years for such a test to finish.

This is why tools like formal verification and symbolic analyses can help you establish that for all possible integers X, your function does the right thing (for some definition of “right”). You get this assurance without having to actually enumerate all X.

Very inefficient. Like wildly so. Specifically if you have a very small database and you preprocess it with their techniques, the resulting database is petabytes in size. But the results are very beautiful.

There are no obvious ways to improve on this work, so it is not a matter of engineering. We really do need another breakthrough result to get us closer to practicality.

At least in my department, this will not work as long as the applicant's supervisor or dissertation committee members are still in the department. The crux of the issue, in my mind, is that it is hard to have candid and unbiased discussion about a candidate when the supervisor / dissertation committee is part of that discussion.

This is strange to me. Many universities, including mine, avoid interviewing applicants with a PhD or postdoc from the same institution to which they are applying.

This is basically what we did in our project: https://www.cis.upenn.edu/~sga001/papers/pung-osdi16.pdf.

We never built it into a product because we couldn't figure out a way to monetize it to pay for the servers.

From my experience your first number is off by 3X and sometimes more depending on the university.

But yes, you make less as a professor than you do in industry.

They are called PIR with sublinear online computation or offline/online PIR.

Key idea is the client issues a query that is independent of what they really want. This is the “offline” query. This query is linear (unavoidable) and the client gets some hints as a result

Then later, the client can issue one or more queries for elements they want and those queries can be sublinear in terms of computation. The client uses hints to make that happen.

Some papers on this are:

https://eprint.iacr.org/2019/1075.pdf

https://eprint.iacr.org/2021/1438

https://eprint.iacr.org/2022/081.pdf

High risk compared to what? The alternative is absolutely no privacy (status quo) or no/limited functionality (not very useful). Seems like strictly better than having no privacy.

You can formally verify all the way to C, C#, Haskell, or even assembly if you use tools like Dafny, Coq, or Vale (for verified assembly). Several projects do this. It’s a lot of work for sure though.

Non interactive zero knowledge allows one proof to be checked by many verifiers. I think folks would still consider that to be a zero knowledge proof no?

That said, yeah this hashing example is not zero knowledge because, among other things, the hash is not hiding.

This hasn’t really been my experience at all. I find students at my university (an ivy) to be pretty reasonable and only complain if there is a mistake during grading. In that case they are absolutely entitled to do so. They also seem to really enjoy challenging classes.

It is 40 degrees F right now… in mid May. And has been all month and basically all year since last November.

I don’t see how you can call that good temperature.

I don't know if the allegations in this antitrust are true or not. However, about a decade ago I wrote a paper (https://www.cis.upenn.edu/~sga001/papers/vex-sigcomm13.pdf) discussing all the ways in which ad exchanges could misbehave without such actions being detectable and some technical mechanisms to prevent violations. I recall some colleagues telling me that surely ad exchanges would never misbehave because deviations from honest behavior would affect companies' reputations, and ethical people within these companies would whistle-blow immediately.

I'm really curious to see where the government acquired their evidence (and what solid evidence do they have), and whether it ends up holding up in court.

I think this requires assuming H is a random oracle, no?

Suppose H(s||k) is a collision-resistant hash function. Let's build another CRHF from H as follows: H'(s || k) = H(s || k) || last-bit-of-k.

Now let's instantiate the cryptosystem you proposed with H'. Suppose m is message and that it is of length equal to the length of the bitstring produced by H'.

We have C = H'(s||k) XOR m.

The ciphertext is thus: (k, C).

What can an attacker do? Well, the attacker can XOR the last bit of C with the last bit of k and get the last bit of m. This is already enough to violate semantic security.

You are right. I'm missing an H at the end.

You first compare target-digest with all endpoints. If it's a match with any of them, good. Then you know a pre-image is in that column.

If not, then try H(R_last(target-digest)). Does it match any endpoint?

If not, then try H(R_last(H(R_second-to-last(target-digest))).

Rinse and repeat.

The table looks like this:

Column 1 Column 2

start-text1 start-text2

<intermediate> <intermediate>

last-hash1 last-hash2

You only store the start text and the last hash for each column. <intermediate> consists of a mix of passwords ("text ") and hashes. To see how they are computed, let us narrow our attention to a single column.

text1

<hash-1> computed using H(text1)

<text-2> computed using R_1(hash-1)

<hash-2> computed using H(text-2)

<text-3> computed using R_2(hash-2)

last-hash computed using H(text-3)

Each column will look like that. I'm using <stuff> to denote things that are not stored. H is the hash function you are creating the rainbow table for. R_1, R_2, etc. are the reduction functions. Each column uses the same hash function and reduction functions but uses a different starting text.

Note that in a rainbow table that consists of k columns, there is no need to recompute hash/reduction functions for each chain. Instead, the attacker computes R_last(target-digest), and checks that against all the endpoints (last hash) of all column. If it matches any endpoint, then that chain likely has the corresponding password. Otherwise, compute R_last(H(R_second_to_last(target-digest))), and compare the result with all endpoints. Rinse and repeat. In the worst case, you have to compute as many hash/reduction functions as there are rows (regardless of the number of columns since all columns use the same hash and reduction functions).

How would you compare this toolkit to something like SEAL? Are there particular selling points or things that I should be aware as a potential user?

ah, this is indeed quite neat. thanks for sharing.

I think you are a bit confused. They are very different in what they guarantee.

The goal of MPC is to hide the inputs of the program. But it is okay for an adversary to make all sorts of inferences by looking at the outputs.

The goal of differential privacy is to limit the kind of inferences that an adversary can make about a particular user/input from the output itself.

> *sender anonymity

Sender anonymity means that the server (or any recipient) cannot determine who sent a particular message. In your example, the centralized server absolutely knows which tweet-sized message was sent by each sender. So your proposal does not provide sender anonymity. Unless of course, the senders use an actual anonymity system to send their messages to the server...