Transcript slides - UMIACS - University of Maryland

ALITHEIA:
Towards Practical Verifiable Graph Processing
Yupeng Zhang, Charalampos Papamanthou and Jonathan Katz
University of Maryland
Agenda
• Background of verifiable computation and motivation
• Our contributions
• Alitheia: A system for Verifiable Computation on graphs
• Shortest paths, longest paths and maximum flow
• Different kinds of graphs: general/planar
• Use of non-generic approaches to achieve practicality/scalability
• Experimental results
• Conclusions
What is verifiable computation?
data & function
•
•
preprocessing
time
Correctness
prover time
Soundness
server
storage
query
digest
answer & proof
verification
time
verify(answer, proof, query)
[1] R. Tamassia. Authenticated Data Structures. In ESA, 2003.
proof size
Generic VC systems: circuit-based
query
data & function
VC
answer
Limitation: inefficient dynamic memory accesses
Overhead is linear in the size of the memory
[2] R. Gennaro, C. Gentry, B. Parno, and M. Raykova. Quadratic span programs and succinct NIZKs without PCPs. in EUROCRYPT, 2013.
[3] B. Parno, J. Howell, C. Gentry, and M. Raykova. Pinocchio: Nearly Practical Verifiable Computation. In SSP, 2013.
Generic VC systems: RAM-based
Use witness to access dynamic memory based on Merkle tree.
Logarithmic overhead in the size of the memory, with large constants
[4] B. Braun, A. J. Feldman, Z. Ren, S. T. V. Setty, A. J. Blumberg, and M. Walfish. Verifying Computations with State. In SOSP, 2013.
[5] E. Ben-Sasson, A. Chiesa, D. Genkin, E. Tromer, and M. Virza. SNARKs for C: Verifying Program Executions Succinctly and in Zero
Knowledge. In CRYPTO, 2013.
Why graph algorithms?
Numerous applications in practice
Shortest Path
Maximal Flow
Longest Path
Verifiable shortest path
Many dynamic memory accesses operations
• n vertices and m edges, breadth first search on a unit weight graph
• Prover time
• Circuit-based naïve implementation: O(nm log2 m)
• RAM-based naïve implementation: O(m log3 m) with large constants
Agenda
• Background of verifiable computation and motivation
• Our contributions
• Alitheia: A system for Verifiable Computation on graphs
• Shortest paths, longest paths and maximum flow
• Different kinds of graphs: general/planar
• Use of non-generic approaches to achieve practicality/scalability
• Experimental results
• Conclusions
What is a certifying algorithm?
• Verifying correctness of a computation (possibly given some auxiliary
input) faster than performing the computation.
• E.g., sorting takes O(n log n) time, but a correct sorted sequence can be verified in
O(n) time
[6] R. M. McConnell, K. Mehlhorn, S. Näher, and P. Schweitzer. Certifying Algorithms. Computer Science Review, 2011.
More efficient VC using certifying algorithms
graph G, function F
certifying algorithm CF
query x
Evaluate F(G,x)
x
auxiliary
F(G,x) input for CF
Generic VC
for CF
digest
answer & proof
F(G,x) proof
or reject
verify(answer, proof, query)
[7] R. Tamassia and N. Triandopoulos. Certification and Authentication of Data Structures. In AMW, 2010.
Certifying algorithm: shortest path
D[1,...,n]
s,t
1. D(s) = 0
2. (u, v)  E : D(v)  D(u )  cuv
3. (u, v)  E : D(v)  D(u )  cuv
D(t)
proof
Linear algorithm with NO dynamic memory accesses!
x[1,...,m] D[1,...,n]
s,t
1. D(s) = 0
2. x  {1, 0,1}
3.  (u ,v )E ( D(v)  D(u )  xuv ) 2  0
D(t)
proof
For unit weight undirected graph
O(n) speed up compared to circuit-based generic VC
O(log m) speed up compared to RAM-based generic VC
Agenda
• Background of verifiable computation and motivation
• Our contributions
• Alitheia: A system for Verifiable Computation on graphs
• Shortest paths, longest paths and maximum flow
• Different kinds of graphs: general/planar
• Use of non-generic approaches to achieve practicality/scalability
• Experimental results
• Conclusions
From general to planar graphs
Planar Separator Theorem:
6
a
O( n )
b
1

3
2
1
7
d
2
n & planar
3

2
c
6
3
e
7
2
n & planar
3
4
5
f
4
5
g
d
a
b
c
e
g
f
Planar separator tree
1
Query:
3
2
d
d
d6 ' d7 '
d1 d 2 d3
6
d1 d 2 d3
7
d1 d 2 d3
d
d6 ' d7 '
+
a
d6 ' d7 '
d
d1 d 2 d3
+
d1 d 2 d3
a
a
min1
min2
d6 ' d7 '
d1 d 2 d3
b
a
c
……
min
Shortest path in planar graphs
• Precomputation & Storage : O( n3/2)
• Query: O( n1/2)
What does the server need to prove now?
Verifiable selection of the minimum element from the sum of two vectors
Additively-homomorphic digest
d
A1
d1
+
d2
d
General Hash is slow in Generic VC!
+
A2
  Li Ai
i
[8] C. Papamanthou, E. Shi, R. Tamassia, and K. Yi. Streaming Authenticated Data Structures. In EUROCRYPT, 2013
VC for vector addition and minimum
d
A
1. Digest(A)=d
2. Output min(A)
min(A)
proof
Complexity comparison
n: number of vertices, m: number of edges, |p|: length of the shortest path
Circuit-Based VC
RAM-Based VC
Alitheia:
Certifying
Algorithms
Alitheia:
Planar
Graphs
Preprocessing Time
O(nm)
O(m log m)
O(m)
O(n3/2)
Prover Time
O(nm log2 (mn))
O(m log3 m)
O(m log2 m)
O(n1/2 log2 n)
Proof Size
O(1)
O(1)
O(|p|)
O( log n+|p|)
Verification Time
O(|p|)
O(|p|)
O(|p|)
O( log n+|p|)
Implementation
• Implementation details:
•
•
•
•
Built on top of Pinocchio [2]
Planar separator by E.Fox-Epstein et al. [7]
Graph processing by LEDA library [8]
Amazon EC2 Linux machine with 15GB RAM
• Experiment details:
• A random planar graph is generated
• 10 runs of experiments
[2] B. Parno, J. Howell, C. Gentry, and M. Raykova. Pinocchio: Nearly Practical Verifiable Computation. In SSP, 2013.
[9] E. Fox-Epstein, S. Mozes, P. M. Phothilimthana, and C. Sommer. Short and Simple Cycle Separators in Planar Graphs. In ALENEX, 2013.
[10] http://www.algorithmic-solutions.com/leda/index.htm.
Example: road network of Rome
n = 3353 nodes, m = 8870 edges, |p| = 13
PINOCCHIO
(Circuit-Based VC)
PANTRY
(RAM-Based VC)
SNARKs for C
(RAM-Based VC )
Alitheia:
Certifying
Algorithms
Alitheia:
Planar
Graphs
Preprocessing
Time
19000 hours*
270 hours*
52 hours*
69 minutes
4.1 minutes
Prover Time
7600 hours*
550 hours*
30 hours*
3.3 minutes
13 seconds
Proof Size
288 bytes
288 bytes
288 bytes
704 bytes
3872bytes
Verification
Time
0.08 seconds*
0.08 seconds*
0.05 seconds*
0.19 seconds
0.59 seconds
[6] 9th DIMACS implementation challenge for shortest paths. http://www.dis.uniroma1.it/challenge9/.
* estimated.
Experimental results
106 x 107 x
12 x
On a graph with 105 nodes:
• Certifying algorithm: 106x faster than Pinocchio BFS, 2x faster than Strawman
• Planar Graph: 107x faster than Pinocchio BFS, 12x faster than Strawman
Experimental results
106 x 107 x
100 x 1000 x
On a graph with 105 nodes:
• Certifying algorithm: 106x smaller than Pinocchio BFS, 100x smaller than Strawman
• Planar Graph: 107x smaller than Pinocchio BFS, 1000x smaller than Strawman
Experimental results
107 x
On a graph with 105 nodes:
• Certifying algorithm: 107x faster than Pinocchio BFS
• Planar Graph: 108x faster than Pinocchio BFS, only tens of seconds
108 x
Experimental results
On a graph with 105 nodes:
• Certifying algorithm: slower by a constant factor
• Planar Graph: grows logarithmically with n but still only around 1s
Conclusions
• Alitheia is the first system to scale verifiable graph computation to
large graphs (up to 200,000 nodes)
• We show that by combining non-generic approaches with generic VC
systems can lead to better efficiency
• For graph algorithms, we show speedups by using certifying
algorithms and noncryptographic data structures
[email protected]
Certifying algorithm: maximal flow
Maximum Flow
Flow Assignment
Cut
s,t
Complexity: Ω(nm)
Maximum-flow-min-cut theorem
Maximum Flow
Linear !!
proof