sangel

7 ms·

1.
by sangel 4mo ago
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 lo
2.
by sangel 11mo ago
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 peopl
3.
by sangel 1y ago
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
4.
by sangel 3y ago
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 impr
5.
Retentive Network: A Successor to Transformer for Large Language Models(arxiv.org)
112 points by sangel 3y ago|19 comments
6.
by sangel 3y ago
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 discu
7.
by sangel 3y ago
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.
8.
by sangel 4y ago
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 serv
9.
by sangel 4y ago
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.
10.
by sangel 4y ago
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 cl
11.
by sangel 4y ago
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.
12.
by sangel 4y ago
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.
13.
by sangel 4y ago
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
14.
by sangel 4y ago
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 re
15.
by sangel 4y ago
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.
16.
by sangel 5y ago
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
17.
by sangel 5y ago
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 c
18.
by sangel 6y ago
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 i
19.
by sangel 6y ago
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. <intermediat
20.
by sangel 6y ago
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?
21.
by sangel 7y ago
ah, this is indeed quite neat. thanks for sharing.
22.
by sangel 7y ago
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
23.
by sangel 9y ago
> *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