Today I get to celebrate that I'm two years done with my three year stint as "Area Dean for Computer Science" (chair). Whoever the new person is, they're supposed to start July 1, 2013. I've already starting encouraging the possible successors to step up. (Indeed, I've already started to become a bit more ambitious. I'm hoping to line up the next 3 or 4 people for the position; no tag backs for a decade...)
It's not that I'm unhappy with the job. (I realize that statement is a no-op; I have to say that. I'm trying to get others to take over.) I'm pleased with what I've been able to do. We tenured two faculty last year (Hanspeter Pfister and Radhika Nagpal); we promoted another (Yiling Chen); we hired a new faculty member (Yaron Singer); and we've just had a junior faculty search for next year approved. We're (still) a relatively small department with a lot of demands on us, and I came in with a clear goal for us for faculty growth. I feel we've been successful in this regard. There have been some other nice successes, such as the new SEAS Design Fair I helped manage and organize, which I expect will be an annual event. And I'm able to act as the faculty interface with the administration in various ways, helping, I hope, keep things running smoothly.
But I'll also be happy to step down. I'm overdue for a sabbatical already (the price of agreeing to a 3-year job). I'll enjoy getting the time back for other things. (Though I expect I'm being unrealistic, and that some other committee or administrative task will try to absorb the time.) I like the "serve 3 years and out" model (though I see weaknesses in it too, in terms of setting up longer term infrastructures). I enjoy taking on new experiences and challenges, so trying out "management" (if that's what this job is) has been interesting and educational. But in one more year, another change will be good.
Saturday, June 30, 2012
Monday, June 18, 2012
Simons Institute Call
Alistair Sinclair asked me to post the call at http://simons.berkeley.
Worth noting -- two semester-long programs for Fall 2013 are already decided: these are "Real Analysis in Computer Science," organized by Gil Kalai, Subhash Khot, Michel Ledoux, Elchanan Mossel, Prasad Raghavendra and Luca Trevisan; and "Theoretical Foundations of Big Data Analysis," organized by Stephen Boyd, Peter Buehlmann, Michael Jordan, Ravi Kannan, Michael Mahoney and Muthu Muthukrishnan. Get your tickets now.
Worth noting -- two semester-long programs for Fall 2013 are already decided: these are "Real Analysis in Computer Science," organized by Gil Kalai, Subhash Khot, Michel Ledoux, Elchanan Mossel, Prasad Raghavendra and Luca Trevisan; and "Theoretical Foundations of Big Data Analysis," organized by Stephen Boyd, Peter Buehlmann, Michael Jordan, Ravi Kannan, Michael Mahoney and Muthu Muthukrishnan. Get your tickets now.
Friday, June 08, 2012
New SIGACT Officers
Lance informs me we have newly elected officers at SIGACT.
Chair: Paul Beame
Members-at-Large:
Venkatesan Guruswami
Rocco Servedio
Avrim Blum
Tal Rabin
Congratulations/condolences to the winners. I'm sure Paul will do a great job --
he's a regular commenter here, and I always find his opinions incredibly well thought out,
even in (rare) cases where I disagree. I can't wait to see what he does.
I'd also like to thank Lance for his service as chair the last few years. He had the unenviable
job of keeping the community happy, preserving the structures that have served us well while
trying to introduce new ideas where there looked to be room for improvement. I think he's
done a great job, generating some controversy and discussion while keeping everything moving forward. He (and the other SIGACT volunteers) deserve our thanks. So, thanks!
Chair: Paul Beame
Members-at-Large:
Venkatesan Guruswami
Rocco Servedio
Avrim Blum
Tal Rabin
Congratulations/condolences to the winners. I'm sure Paul will do a great job --
he's a regular commenter here, and I always find his opinions incredibly well thought out,
even in (rare) cases where I disagree. I can't wait to see what he does.
I'd also like to thank Lance for his service as chair the last few years. He had the unenviable
job of keeping the community happy, preserving the structures that have served us well while
trying to introduce new ideas where there looked to be room for improvement. I think he's
done a great job, generating some controversy and discussion while keeping everything moving forward. He (and the other SIGACT volunteers) deserve our thanks. So, thanks!
Thursday, June 07, 2012
Mihai Memorial Blog
I received the following note from Mikkel Thorup and Alexandr Andoni.
I believe it's appropriate to share:
Dear friends of Mihai,
We made a blog in Mihai's memory. Celebrating Mihai's energy and
spirit, please cheer him with a glass of wine (or other spirits), and
send in a picture to be posted on the page:
http://mipmemorial.blogspot.
Best regards,
Mikkel and Alex
Many of you have left wonderful comments about Mihai here. I hope you'll copy them over and possibly add to them at the memorial site.
I believe it's appropriate to share:
Dear friends of Mihai,
We made a blog in Mihai's memory. Celebrating Mihai's energy and
spirit, please cheer him with a glass of wine (or other spirits), and
send in a picture to be posted on the page:
http://mipmemorial.blogspot.
Best regards,
Mikkel and Alex
Many of you have left wonderful comments about Mihai here. I hope you'll copy them over and possibly add to them at the memorial site.
Wednesday, June 06, 2012
Sad Passing: Mihai Patrascu
[** UPDATE **]
Dear friends of Mihai,
We made a blog in Mihai's memory. Celebrating Mihai's energy and
spirit, please cheer him with a glass of wine (or other spirits), and
send in a picture to be posted on the page:
http://mipmemorial.blogspot.
Best regards,
Mikkel and Alex
[** UPDATE END **]
Mikkel Thorup just sent me the following to post regarding Mihai Patrascu.
---------------
Mihai Patrascu, aged 29, passed away on Tuesday June 5, 2012, after a
1.5 year battle with brain cancer. Mihai's carreer was short but
explosive, full of rich and beautiful ideas as witnessed, e.g., in his 19
STOC/FOCS papers.
Mihai was very happy about being co-winner of the 2012 EATCS Presburger Young Scientist Award for his ground-breaking work on data
structure lower-bounds. It was wonderful that the community stood up
to applaud this achievement at STOC'12. Unfortunately he will not make it to the award ceremony on July 10 at ICALP. Mihai's appreciation
for the award shows in the last post on his blog
http://infoweekly.blogspot.
I was fortunate enough to be one of Mihai's main collaborators. One of
the things that made it possible to work on hard problems was having
lots of fun: playing squash, going on long hikes, and having beers
celebrating every potentially useful idea.
On this last note, Mihai's wife Mira tells me that she does not want
any flowers and that his funeral will be back in Romania.
However, she wants people to have a glass of wine in Mihai's memory,
thinking about him as the inspired and fun young man that he was.
Dear friends of Mihai,
We made a blog in Mihai's memory. Celebrating Mihai's energy and
spirit, please cheer him with a glass of wine (or other spirits), and
send in a picture to be posted on the page:
http://mipmemorial.blogspot.
Best regards,
Mikkel and Alex
[** UPDATE END **]
Mikkel Thorup just sent me the following to post regarding Mihai Patrascu.
---------------
Mihai Patrascu, aged 29, passed away on Tuesday June 5, 2012, after a
1.5 year battle with brain cancer. Mihai's carreer was short but
explosive, full of rich and beautiful ideas as witnessed, e.g., in his 19
STOC/FOCS papers.
Mihai was very happy about being co-winner of the 2012 EATCS Presburger Young Scientist Award for his ground-breaking work on data
structure lower-bounds. It was wonderful that the community stood up
to applaud this achievement at STOC'12. Unfortunately he will not make it to the award ceremony on July 10 at ICALP. Mihai's appreciation
for the award shows in the last post on his blog
http://infoweekly.blogspot.
I was fortunate enough to be one of Mihai's main collaborators. One of
the things that made it possible to work on hard problems was having
lots of fun: playing squash, going on long hikes, and having beers
celebrating every potentially useful idea.
On this last note, Mihai's wife Mira tells me that she does not want
any flowers and that his funeral will be back in Romania.
However, she wants people to have a glass of wine in Mihai's memory,
thinking about him as the inspired and fun young man that he was.
Verification in the Cloud [Guest Post by Justin Thaler]
[Justin talks about his upcoming work, to be presented at HotCloud.]
For the past few years, Michael and I, along with our awesome collaborators, have worked towards developing practical protocols for verifying outsourced computations. In roughly chronological order, the relevant papers are here , here , here , here , and most recently here . In this last paper (joint work with Mike Roberts and Hanspeter Pfister ), we really tried to push these protocols into practice, largely by taking advantage of their inherent parallelizability: we'll be presenting it at HotCloud next week, and it is the main impetus for this blog post. My hope here is to give a (somewhat) brief, unified overview of what we've accomplished with this line of work, and how it relates to some exciting parallel lines of inquiry by other researchers.
Our main motivation is that of Alice, who stores a large data set on the cloud, and asks the cloud to perform a computation on the data (say, to compute the shortest path between two nodes in a large graph, or to solve a linear program defined over the data). Of course, Alice may be a company or an organization, rather than an individual. The goal is to provide Alice with a guarantee that the server performed the requested computation correctly, without requiring Alice to perform the requested computations herself, or even to maintain a local copy of the data (since Alice may have resorted to the cloud in the first place because she has more data than she can store). In short, we want to save Alice as much time and space as possible, while also minimizing the amount of extra bookkeeping that the cloud has to do to prove the integrity of the computation.
Alice may want such integrity guarantees because she is concerned about simple errors, like dropped data, hardware faults, or a buggy algorithm, or she may be more paranoid and fear that the cloud is deliberately deceptive or has been externally compromised. So ideally we'd like our protocols to be secure against arbitrarily malicious clouds, but sufficiently lightweight for use in more benign settings. This is an ambitious goal, but achieving it could go a long way toward mitigating trust issues that hinder the adoption of cloud computing solutions.
Surprisingly powerful protocols for verifiable computation were famously discovered within the theory community several decades ago, in the form of interactive proofs , PCPs , and the like. These results are some of the brightest gems of complexity theory, but as of a few years ago they were mainly theoretical curiosities, far too inefficient for actual deployment (with the notable exception of certain zero-knowledge proofs).
We've been focusing on interactive proof methods, and have made substantial strides in improving their efficiency. One direction we've focused on is the development of highly optimized protocols for specific important problems, like reporting queries (what value is stored in memory location x of my database?), matrix multiplication, graph problems like perfect matching, and certain kinds of linear programs. Many of these are provably optimal in terms of space and communication costs, consist of a single message from the cloud to Alice (which can be sent as an email attachment or posted on a website), and already save Alice considerable time and space while imposing minimal burden on the cloud, both in theory and experimentally. But for the rest of this post I will focus on *general-purpose* methods, which are capable of verifying arbitrary computations.
The high-order insights of this line of work are as follows. The statements below have precise theoretical formulations, but I'm referring to actual experimental results with a full-blown implementation. Note that a lot of engineering work went into making our implementations fast, like choosing the "right" finite field to work over, and working with the right kinds of circuits.
1) We can save Alice substantial amounts of space essentially for free. The reason is that existing interactive proof protocols (such as Interactive Proofs for Muggles by Goldwasser, Kalai, and Rothblum, which is the protocol underlying our implementation) only require Alice to store a fingerprint of the data. This fingerprint can be computed in a single, light-weight streaming pass over the input (say, while Alice uploads her data to the cloud), and serves as a sort of "secret" that Alice can use to catch the cloud in a lie. The fingerprint doesn't even depend on the computation being outsourced, so Alice doesn't need to know what computation she's interested in until well after she's seen the input, and she never needs to store the input locally.
2) Our implementation already saves Alice a lot of time relative to doing the computation herself. For example, when multiplying two 512x512 matrices, Alice requires roughly a tenth of a second to process the input, while naive matrix multiplication takes about seven times longer. And the savings increase substantially at larger input sizes (as well as when applying our implementation to more time-intensive computations than matrix multiplication) since Alice's runtime in the protocol grows roughly linearly with the input size. So I'd argue that verifiable computation is essentially a solved problem in settings where the main focus is saving Alice time, and the runtime of the cloud is of secondary importance. At least this the case for problems solvable by reasonably small-depth circuits, for which our implementation is most efficient.
3) We've come a long way in making the prover more efficient. Theoretically speaking, in our ITCS paper with Graham Cormode , we brought the runtime of the cloud down from polynomial in the size of a circuit computing the function of interest, to quasilinear in the size of the circuit. Practically speaking, a lot of work remains to be done on this aspect (for example, our single-threaded cloud implementation takes about 30 minutes to multiply two 256 x 256 matrices, and matrix multiplication is a problem well-suited to these sorts of protocols), but we are in much better shape than we were just a few years ago.
4) All of the protocols (special-purpose and general-purpose alike) are extremely amenable to parallelization on existing hardware. This holds for both Alice and the cloud (although Alice runs extremely quickly even without parallelization, see Point 1). For example, using GPUs we can bring the runtime of the cloud to < 40 seconds when multiplying two 256 x 256 matrices. Obviously this is still much slower than matrix multiplication without integrity guarantees, but we're now just one or two orders of magnitude away from undeniable usefulness.
The extended abstract appearing in HotCloud (which should be viewed largely as an advertisement for the arxiv version) can be found here . We tried hard to give an accessible, if very high level, overview of the powerful ideas underlying interactive proofs, which I hope will be useful for researchers who are encountering verifiable computation for the first time. Slides describing the entirety of this line of work in more detail can be found here .
I want to close by mentioning two exciting lines of work occurring in parallel with our own. First, Ben-Sasson, Chiesa, Genkin, and Tromer are working toward developing practical PCPs, or probabilistically-checkable proofs (see their new paper here ). The PCP setting is much more challenging than the interactive proof setting we have been working in above: in a PCP, there is no interaction to leverage (i.e. the cloud sends a single message to Alice), and moreover Alice is only permitted to look at *a few bits* of the proof. The latter may seem like an artificial constraint that doesn't matter in real outsourcing scenarios, but it turns out that building a practical PCP system would buy you quite a bit. This is because one can throw certain cryptographic primitives on top of a PCP system (like collision-resistant hash functions) and get a wide variety of powerful protocols, such as succinct arguments for all of NP (i.e., protocols requiring very little communication, which are secure against computationally bounded adversaries). The work of BSCGT appears to still be in the theoretical stage, but is very exciting nonetheless. Check out their paper for more details.
Second is work of Setty, McPherson, Blumberg, and Walfish, from NDSS earlier this year (see their project page here ). They implemented an argument system originally due Ishai, Kushilevitz, and Ostrovsky, and bring the runtime of the cloud down by a factor of 10^20 relative to a naive implementation (yes, I said 10^20; this again highlights the considerable engineering work that needs to be done on top of the theory to make proof or argument systems useful). Our protocols have several advantages not shared by SMBW (like security against computationally unbounded adversaries, and the ability to save the verifier time even when outsourcing a single computation), but this is another big step toward a practical implementation for verified computation. It looks like related work by Setty, Vu, Panpalia, Braun, Blumberg, and Walfish will be presented at USENIX Security 2012 as well (see the conference page here ).
The golden age for negative applications of interactive proofs and PCPs (such as hardness of approximation results) arrived over 15 years ago, and continues to this day. Perhaps the time for positive applications is now.
For the past few years, Michael and I, along with our awesome collaborators, have worked towards developing practical protocols for verifying outsourced computations. In roughly chronological order, the relevant papers are here , here , here , here , and most recently here . In this last paper (joint work with Mike Roberts and Hanspeter Pfister ), we really tried to push these protocols into practice, largely by taking advantage of their inherent parallelizability: we'll be presenting it at HotCloud next week, and it is the main impetus for this blog post. My hope here is to give a (somewhat) brief, unified overview of what we've accomplished with this line of work, and how it relates to some exciting parallel lines of inquiry by other researchers.
Our main motivation is that of Alice, who stores a large data set on the cloud, and asks the cloud to perform a computation on the data (say, to compute the shortest path between two nodes in a large graph, or to solve a linear program defined over the data). Of course, Alice may be a company or an organization, rather than an individual. The goal is to provide Alice with a guarantee that the server performed the requested computation correctly, without requiring Alice to perform the requested computations herself, or even to maintain a local copy of the data (since Alice may have resorted to the cloud in the first place because she has more data than she can store). In short, we want to save Alice as much time and space as possible, while also minimizing the amount of extra bookkeeping that the cloud has to do to prove the integrity of the computation.
Alice may want such integrity guarantees because she is concerned about simple errors, like dropped data, hardware faults, or a buggy algorithm, or she may be more paranoid and fear that the cloud is deliberately deceptive or has been externally compromised. So ideally we'd like our protocols to be secure against arbitrarily malicious clouds, but sufficiently lightweight for use in more benign settings. This is an ambitious goal, but achieving it could go a long way toward mitigating trust issues that hinder the adoption of cloud computing solutions.
Surprisingly powerful protocols for verifiable computation were famously discovered within the theory community several decades ago, in the form of interactive proofs , PCPs , and the like. These results are some of the brightest gems of complexity theory, but as of a few years ago they were mainly theoretical curiosities, far too inefficient for actual deployment (with the notable exception of certain zero-knowledge proofs).
We've been focusing on interactive proof methods, and have made substantial strides in improving their efficiency. One direction we've focused on is the development of highly optimized protocols for specific important problems, like reporting queries (what value is stored in memory location x of my database?), matrix multiplication, graph problems like perfect matching, and certain kinds of linear programs. Many of these are provably optimal in terms of space and communication costs, consist of a single message from the cloud to Alice (which can be sent as an email attachment or posted on a website), and already save Alice considerable time and space while imposing minimal burden on the cloud, both in theory and experimentally. But for the rest of this post I will focus on *general-purpose* methods, which are capable of verifying arbitrary computations.
The high-order insights of this line of work are as follows. The statements below have precise theoretical formulations, but I'm referring to actual experimental results with a full-blown implementation. Note that a lot of engineering work went into making our implementations fast, like choosing the "right" finite field to work over, and working with the right kinds of circuits.
1) We can save Alice substantial amounts of space essentially for free. The reason is that existing interactive proof protocols (such as Interactive Proofs for Muggles by Goldwasser, Kalai, and Rothblum, which is the protocol underlying our implementation) only require Alice to store a fingerprint of the data. This fingerprint can be computed in a single, light-weight streaming pass over the input (say, while Alice uploads her data to the cloud), and serves as a sort of "secret" that Alice can use to catch the cloud in a lie. The fingerprint doesn't even depend on the computation being outsourced, so Alice doesn't need to know what computation she's interested in until well after she's seen the input, and she never needs to store the input locally.
2) Our implementation already saves Alice a lot of time relative to doing the computation herself. For example, when multiplying two 512x512 matrices, Alice requires roughly a tenth of a second to process the input, while naive matrix multiplication takes about seven times longer. And the savings increase substantially at larger input sizes (as well as when applying our implementation to more time-intensive computations than matrix multiplication) since Alice's runtime in the protocol grows roughly linearly with the input size. So I'd argue that verifiable computation is essentially a solved problem in settings where the main focus is saving Alice time, and the runtime of the cloud is of secondary importance. At least this the case for problems solvable by reasonably small-depth circuits, for which our implementation is most efficient.
3) We've come a long way in making the prover more efficient. Theoretically speaking, in our ITCS paper with Graham Cormode , we brought the runtime of the cloud down from polynomial in the size of a circuit computing the function of interest, to quasilinear in the size of the circuit. Practically speaking, a lot of work remains to be done on this aspect (for example, our single-threaded cloud implementation takes about 30 minutes to multiply two 256 x 256 matrices, and matrix multiplication is a problem well-suited to these sorts of protocols), but we are in much better shape than we were just a few years ago.
4) All of the protocols (special-purpose and general-purpose alike) are extremely amenable to parallelization on existing hardware. This holds for both Alice and the cloud (although Alice runs extremely quickly even without parallelization, see Point 1). For example, using GPUs we can bring the runtime of the cloud to < 40 seconds when multiplying two 256 x 256 matrices. Obviously this is still much slower than matrix multiplication without integrity guarantees, but we're now just one or two orders of magnitude away from undeniable usefulness.
The extended abstract appearing in HotCloud (which should be viewed largely as an advertisement for the arxiv version) can be found here . We tried hard to give an accessible, if very high level, overview of the powerful ideas underlying interactive proofs, which I hope will be useful for researchers who are encountering verifiable computation for the first time. Slides describing the entirety of this line of work in more detail can be found here .
I want to close by mentioning two exciting lines of work occurring in parallel with our own. First, Ben-Sasson, Chiesa, Genkin, and Tromer are working toward developing practical PCPs, or probabilistically-checkable proofs (see their new paper here ). The PCP setting is much more challenging than the interactive proof setting we have been working in above: in a PCP, there is no interaction to leverage (i.e. the cloud sends a single message to Alice), and moreover Alice is only permitted to look at *a few bits* of the proof. The latter may seem like an artificial constraint that doesn't matter in real outsourcing scenarios, but it turns out that building a practical PCP system would buy you quite a bit. This is because one can throw certain cryptographic primitives on top of a PCP system (like collision-resistant hash functions) and get a wide variety of powerful protocols, such as succinct arguments for all of NP (i.e., protocols requiring very little communication, which are secure against computationally bounded adversaries). The work of BSCGT appears to still be in the theoretical stage, but is very exciting nonetheless. Check out their paper for more details.
Second is work of Setty, McPherson, Blumberg, and Walfish, from NDSS earlier this year (see their project page here ). They implemented an argument system originally due Ishai, Kushilevitz, and Ostrovsky, and bring the runtime of the cloud down by a factor of 10^20 relative to a naive implementation (yes, I said 10^20; this again highlights the considerable engineering work that needs to be done on top of the theory to make proof or argument systems useful). Our protocols have several advantages not shared by SMBW (like security against computationally unbounded adversaries, and the ability to save the verifier time even when outsourcing a single computation), but this is another big step toward a practical implementation for verified computation. It looks like related work by Setty, Vu, Panpalia, Braun, Blumberg, and Walfish will be presented at USENIX Security 2012 as well (see the conference page here ).
The golden age for negative applications of interactive proofs and PCPs (such as hardness of approximation results) arrived over 15 years ago, and continues to this day. Perhaps the time for positive applications is now.
Subscribe to:
Posts (Atom)