Correctness proof for new bandwidth-weights (bug 1952)

[Mike Perry]

Recently, Tor 0.2.2.x-alpha has suffered from a serious bug that
caused the directory authorities to produce incorrect
bandwidth-weights for use by 0.2.2.x clients.

The process used is described in 3.4.3 of dir-spec.txt
https://gitweb.torproject.org/tor.git/blob_plain/HEAD:/doc/spec/dir-spec.txt

To achieve balance, we start with 5 equations for 7 unknowns, and then
we add 2 extra equations depending upon the amount of capacity in the
network, as described by the cases in 3.4.3.

The problem is that the extra constraints added for case 1, case 2b,
and case 3b can lead to solutions outside of the range of
0..weight_scale in some cases. These solutions are invalid for use as
selection weights.

Because these invalid solution situations have begun to appear on the
current network, I've spent the past few days redoing these cases to
solve this bug: https://trac.torproject.org/projects/tor/ticket/1952

The new extra constraints are:

Case 1: Wmg == Wmd, Wed == 1/3.
Case 2b:
  Wgg == 1, Wee == 1
Case 3b:
  If G<E: Wgg = 1, Wmd == Wed
  If E<G: Wee == 1, Wmd == Wgd

To prove they are correct, we simply consider the cases where each
weight might exceed weight_scale, and where each might fall below 0.


For Case 1, the solution to the 7 equations is:
  Wgd = weight_scale/3
  Wed = weight_scale/3
  Wmd = weight_scale/3
  Wee = (weight_scale*(E+G+M))/(3*E)
  Wme = weight_scale - Wee
  Wmg = (weight_scale*(2*G-E-M))/(3*G)
  Wgg = weight_scale - Wmg

Now, let's examine those weights that can either exceed weight_scale,
or fall below 0. We derive conditions for valid solution ranges, and
then compare these conditions to the case requirements:

Wee <= weight_scale:
  E+G+M <= 3*E               # From (weight_scale*(E+G+M))/(3*E)
  E+G+M+D <= 3*E+D
  T <= 3*E+D                 # From T=G+M+E+D
  (T-D)/3 <= E

  Since Case 1 is only in effect while E >= T/3, this constraint is
  clearly always true.
  
Wme >= 0:
  2*E-G-M >= 0              # From Wme's denominator
  2*E+D+E > = G+M+E+D
  3*E+D >= T
  E >= (T-D)/3
  
  This is true because of the conditions for Case 1: E >= T/3 && G >= T/3.
 
Wmg <= weight_scale:
  2*G-E-M <= 3*G
  0 <= G+E+M
  D <= G+E+M+D
  D <= T

Wmg >= 0:
  2*G-E-M >= 0
  2*G+D+G >= E+M+D+G
  3*G+D >= T
  G >= (T-D)/3 

  This is true because of the conditions for Case 1: E >= T/3 && G >= T/3.


Case 2b:

  Wgg = Wee = weight_scale
  Wed = (weight_scale*(D - 2*E + G + M))/(3*D)
  Wmd = (weight_Scale*(D - 2*M + G + E))/(3*D)
  Wme = Wmg = 0
  Wgd = weight_scale - Wed - Wmd

In this case, we need to check the following:

Wed >= 0:
  D+G+M-2*E >= 0
  D+G+M+E >= 3*E
  T/3 >= E

  This is one of the conditions for Case 2b.

Wgd >= 0:
  Wed + Wmd <= 1
  2*D-2*E-2*M+2*G+M+E <= 3*D
  2*G-M-E-D <= 0
  3*G <= M+E+D+G
  G <= T/3

  This is one of the conditions for Case 2b.

Wmd >= 0:
  D+G+E-2*M > 0
  T/3 >= M

  If your eyes haven't glazed over yet, you'll notice that this last
  condition can actually be true. If we don't hand out enough Guard
  flags, there may be too many middle nodes. In this case, the code just
  warns and suggests that the WFU parameters be lowered.


Case 3b:

For case 3b, there are two subcases, but they are the same formula
set, just with E and G reversed. Thus, we only need to prove one of
them. For simplicity, let's do the E scarce case, as that is the only
one of the two we have ever seen:

  Wee = weight_scale;
  Wed = (weight_scale*(D - 2*E + G + M))/(3*D);
  Wme = 0;
  Wgg = (weight_scale*(G+M))/(2*G);
  Wmg = weight_scale - Wgg;
  Wmd = (weight_scale - Wed)/2;


Wed >= 0:
  D - 2*E + G + M >= 0
  D + E + G + M >= 3E
  T/3 >= E

  This is one of the conditions for Case 3b.

Wed <= weight_scale:
  D - 2*E + G + M <= 3*D
  G + M <= 2*D + 2*E
  G + E + M + D <= 3*D + 3*E
  T/3 <= D+E

  This is also one of the conditions for Case 3b, when E is scarce.

Wgg <= weight_scale:
  G+M <= 2*G
  M <= G

  Since G >= T/3, and E+D >= T/3, we know that M <= T/3. So M <= G.


-- 
Mike Perry
Mad Computer Scientist
fscked.org evil labs
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 189 bytes
Desc: not available
URL: <http://lists.torproject.org/pipermail/tor-dev/attachments/20100926/4b01c1bb/attachment.pgp>