[PATCH][RFC] tcp: fix ambiguity in the `before' relation

[PATCH][RFC] tcp: fix ambiguity in the `before' relation

[Gerrit Renker]

While looking at DCCP sequence numbers, I stumbled over a problem with
the following definition of before in tcp.h:

static inline int before(__u32 seq1, __u32 seq2)
{
        return (__s32)(seq1-seq2) < 0;
}

Problem: This definition suffers from an an ambiguity, i.e. always
                   
           before(a, (a + 2^31) % 2^32)) = 1
           before((a + 2^31) % 2^32), a) = 1
 
         In text: when the difference between a and b amounts to 2^31,
         a is always considered `before' b, the function can not decide. 
         The reason is that implicitly 0 is `before' 1 ... 2^31-1 ... 2^31
      
Solution: There is a simple fix, by defining before in such a way that 
          0 is no longer `before' 2^31, i.e. 0 `before' 1 ... 2^31-1
          By not using the middle between 0 and 2^32, before can be made 
          unambiguous. 
          This is achieved by testing whether seq2-seq1 > 0 (using signed
          32-bit arithmetic).

I attach a patch to codify this. Also the `after' relation is basically 
a redefinition of `before', it is now defined as a macro after before.

Signed-off-by: Gerrit Renker <gerrit@erg.abdn.ac.uk>
---
 tcp.h |    9 ++-------
 1 file changed, 2 insertions(+), 7 deletions(-)


diff --git a/include/net/tcp.h b/include/net/tcp.h
index c99774f..b7d8317 100644
--- a/include/net/tcp.h
+++ b/include/net/tcp.h
@@ -242,14 +242,9 @@ extern int tcp_memory_pressure;
 
 static inline int before(__u32 seq1, __u32 seq2)
 {
-        return (__s32)(seq1-seq2) < 0;
+        return (__s32)(seq2-seq1) > 0;
 }
-
-static inline int after(__u32 seq1, __u32 seq2)
-{
-	return (__s32)(seq2-seq1) < 0;
-}
-
+#define after(seq2, seq1) 	before(seq1, seq2)
 
 /* is s2<=s1<=s3 ? */
 static inline int between(__u32 seq1, __u32 seq2, __u32 seq3)

Re: [PATCH][RFC] tcp: fix ambiguity in the `before' relation

[David Miller]

From: Gerrit Renker <gerrit@erg.abdn.ac.uk>
Date: Thu, 14 Dec 2006 15:07:06 +0000

> While looking at DCCP sequence numbers, I stumbled over a problem with
> the following definition of before in tcp.h:
> 
> static inline int before(__u32 seq1, __u32 seq2)
> {
>         return (__s32)(seq1-seq2) < 0;
> }
> 
> Problem: This definition suffers from an an ambiguity, i.e. always
>                    
>            before(a, (a + 2^31) % 2^32)) = 1
>            before((a + 2^31) % 2^32), a) = 1
>  
>          In text: when the difference between a and b amounts to 2^31,
>          a is always considered `before' b, the function can not decide. 
>          The reason is that implicitly 0 is `before' 1 ... 2^31-1 ... 2^31
>       
> Solution: There is a simple fix, by defining before in such a way that 
>           0 is no longer `before' 2^31, i.e. 0 `before' 1 ... 2^31-1
>           By not using the middle between 0 and 2^32, before can be made 
>           unambiguous. 
>           This is achieved by testing whether seq2-seq1 > 0 (using signed
>           32-bit arithmetic).
> 
> I attach a patch to codify this. Also the `after' relation is basically 
> a redefinition of `before', it is now defined as a macro after before.
> 
> Signed-off-by: Gerrit Renker <gerrit@erg.abdn.ac.uk>

Applied, thanks Gerrit.

I went over this patch and analysis a dozen times, because I
couldn't believe something like this has been broken for
so long :-)

Even BSD suffers of this issue, since the beginning.  See
SEQ_LT() in tcp_seq.h, and it seems that BSD's timestamp
sequence checking has the issue too (see TSTMP_LT() macro
in OpenBSD's tcp_input.c)

It seems that our PAWS timestamp checks are ok because we do:

(s32)(tp->rx_opt.ts_recent - tp->rx_opt.rcv_tsval) > TCP_PAWS_WINDOW

and

(s32)(tp->rx_opt.rcv_tsval - tp->rx_opt.ts_recent) >= 0

Thanks again Gerrit.

Re: [PATCH][RFC] tcp: fix ambiguity in the `before' relation

[Christoph Hellwig]

On Thu, Dec 14, 2006 at 03:07:06PM +0000, Gerrit Renker wrote:
> diff --git a/include/net/tcp.h b/include/net/tcp.h
> index c99774f..b7d8317 100644
> --- a/include/net/tcp.h
> +++ b/include/net/tcp.h
> @@ -242,14 +242,9 @@ extern int tcp_memory_pressure;
>  
>  static inline int before(__u32 seq1, __u32 seq2)
>  {
> -        return (__s32)(seq1-seq2) < 0;
> +        return (__s32)(seq2-seq1) > 0;
>  }
> -
> -static inline int after(__u32 seq1, __u32 seq2)
> -{
> -	return (__s32)(seq2-seq1) < 0;
> -}
> -
> +#define after(seq2, seq1) 	before(seq1, seq2)

Btw, these macfox/inlines are named quite a bit too generic for
something that is in tcp.h

Re: [PATCH][RFC] tcp: fix ambiguity in the `before' relation

[Gerrit Renker]

Hi David,

many thanks for taking the matter seriously and investigating
it further. 

|  I went over this patch and analysis a dozen times, because I
|  couldn't believe something like this has been broken for
|  so long :-)
It gave me some grief too, when I looked at DCCP sequence numbers %-)
RFC 1982 provides some definitions, but leaves the case a = (b + 2^31) % 2^32
open to the implementation (suggests `undefined').

I think the new definition is more conformant with RFC 1982 than the old one,
since the ambiguity is now removed with regard to a = (b + 2^31) % 32, and it
is not "unnecessarily burdensome to implement" (section 3.2 of RFC 1982).
  
|  Even BSD suffers of this issue, since the beginning.  See
|  SEQ_LT() in tcp_seq.h, and it seems that BSD's timestamp
|  sequence checking has the issue too (see TSTMP_LT() macro
|  in OpenBSD's tcp_input.c)
I didn't know about OpenBSD, but in Stevens vol 2 (sec. 24.7) it is
already defined in this way. 

Best regards & merry Christmas
Gerrit

Re: [PATCH][RFC] tcp: fix ambiguity in the `before' relation

[Herbert Xu]

David Miller <davem@davemloft.net> wrote:
> From: Gerrit Renker <gerrit@erg.abdn.ac.uk>
> Date: Thu, 14 Dec 2006 15:07:06 +0000
> 
>> While looking at DCCP sequence numbers, I stumbled over a problem with
>> the following definition of before in tcp.h:
>> 
>> static inline int before(__u32 seq1, __u32 seq2)
>> {
>>         return (__s32)(seq1-seq2) < 0;
>> }
>> 
>> Problem: This definition suffers from an an ambiguity, i.e. always
>>                    
>>            before(a, (a + 2^31) % 2^32)) = 1
>>            before((a + 2^31) % 2^32), a) = 1
>>  
>>          In text: when the difference between a and b amounts to 2^31,
>>          a is always considered `before' b, the function can not decide. 
>>          The reason is that implicitly 0 is `before' 1 ... 2^31-1 ... 2^31
>>       
>> Solution: There is a simple fix, by defining before in such a way that 
>>           0 is no longer `before' 2^31, i.e. 0 `before' 1 ... 2^31-1
>>           By not using the middle between 0 and 2^32, before can be made 
>>           unambiguous. 
>>           This is achieved by testing whether seq2-seq1 > 0 (using signed
>>           32-bit arithmetic).
>> 
>> I attach a patch to codify this. Also the `after' relation is basically 
>> a redefinition of `before', it is now defined as a macro after before.
>> 
>> Signed-off-by: Gerrit Renker <gerrit@erg.abdn.ac.uk>
> 
> Applied, thanks Gerrit.
> 
> I went over this patch and analysis a dozen times, because I
> couldn't believe something like this has been broken for
> so long :-)

Sorry, I still don't get the point of this change.

Prior to the patch, we have values x and y such that both
before(x, y) and before(y, x) are true.  Now for those same
values both before(x, y) and before(y, x) are false.

It's still as ambiguous as ever.  Surely to resolve the
ambiguity we want to make before(x, y) = !before(y, x), no?

Cheers,
-- 
Visit Openswan at http://www.openswan.org/
Email: Herbert Xu ~{PmV>HI~} <herbert@gondor.apana.org.au>
Home Page: http://gondor.apana.org.au/~herbert/
PGP Key: http://gondor.apana.org.au/~herbert/pubkey.txt

Re: [PATCH][RFC] tcp: fix ambiguity in the `before' relation

[Gerrit Renker]

Hi Herbert,


|  >> While looking at DCCP sequence numbers, I stumbled over a problem with
|  >> the following definition of before in tcp.h:
|  >> 
|  >> static inline int before(__u32 seq1, __u32 seq2)
|  >> {
|  >>         return (__s32)(seq1-seq2) < 0;
|  >> }
|  >> 
|  >> Problem: This definition suffers from an an ambiguity, i.e. always
|  >>                    
|  >>            before(a, (a + 2^31) % 2^32)) = 1
|  >>            before((a + 2^31) % 2^32), a) = 1
|  >>  
|  >>          In text: when the difference between a and b amounts to 2^31,
|  >>          a is always considered `before' b, the function can not decide. 
|  >>          The reason is that implicitly 0 is `before' 1 ... 2^31-1 ... 2^31
|  >>       
|  >> Solution: There is a simple fix, by defining before in such a way that 
|  >>           0 is no longer `before' 2^31, i.e. 0 `before' 1 ... 2^31-1
|  >>           By not using the middle between 0 and 2^32, before can be made 
|  >>           unambiguous. 
|  >>           This is achieved by testing whether seq2-seq1 > 0 (using signed
|  >>           32-bit arithmetic).
| 
|  Sorry, I still don't get the point of this change.
|  
|  Prior to the patch, we have values x and y such that both
|  before(x, y) and before(y, x) are true.  Now for those same
|  values both before(x, y) and before(y, x) are false.
|
|  It's still as ambiguous as ever.  Surely to resolve the
|  ambiguity we want to make before(x, y) = !before(y, x), no?
Please let me restate:
 Ambiguity here means that for those numbers x,y such that  (x + 2^31) % 2^32) = y
 before(x, y) = 1 and before(y, x) = 1. With the previous implementation, one could 
 not tell the difference here: and there are 2^32 such cases where this occurs.

 With the implementation now, the output of before(x,y) is reliable: it returns true
 if (and only if) x is indeed `before' y.

 If before(x,y) is false then there are now two possibilities:
  (a) before(y, x) is true   and y != (x + 2^31) % 2^32
  (b) before(y, x) is false  and y == (x + 2^31) % 2^32
 This means that the cases can be clearly separated out, which was not possible before.

		To summarize the differences:
		-----------------------------

1) Possible cases in the old implementation (exclusive-or list):
    * x == y                            -  identity
    * before(x, y) && !before(y, x)     -  x is `before' y
    * before(y, x) && !before(x, y) 	-  y is `before' x
    * before(x, y) && before(y, x)      -  y == (x + 2^31) % 2^32
    
2) Possible cases in the new implementation (exclusive-or list):
    * x == y 				-  identity
    * before(x, y)			-  x is `before' x
    * before(y, x)			-  y is `before x
    * !before(x, y) && !before(y, x)    -  y == (x + 2^31) % 2^32

As can be seen (2) requires fewer test cases while (1) would need extra checks to disambiguate
before(x, y) from the case "before(x,y) && before(y,x)".

I do believe that this is useful, since now speeds of 10 Gigabits are in use, which means that
sequence numbers wrap around faster; and also with regard to the issue of selecting an initial
sequence number; and protection against sequence number attacks.

A related discussion is in RFC 1982, but with regard to the case y == (x + 2^31) % 2^32 it 
recommends to leave this `undefined' -- the new solution is in agreement with this, and is
even less complicated to implement.

Gerrit

Re: [PATCH][RFC] tcp: fix ambiguity in the `before' relation

[Herbert Xu]

Gerrit Renker <gerrit@erg.abdn.ac.uk> wrote:
>
> |  Prior to the patch, we have values x and y such that both
> |  before(x, y) and before(y, x) are true.  Now for those same
> |  values both before(x, y) and before(y, x) are false.
> |
> |  It's still as ambiguous as ever.  Surely to resolve the
> |  ambiguity we want to make before(x, y) = !before(y, x), no?
>
> Please let me restate:
> Ambiguity here means that for those numbers x,y such that  (x + 2^31) % 2^32) = y
> before(x, y) = 1 and before(y, x) = 1. With the previous implementation, one could 
> not tell the difference here: and there are 2^32 such cases where this occurs.
> 
> With the implementation now, the output of before(x,y) is reliable: it returns true
> if (and only if) x is indeed `before' y.

Sorry but I don't think you've answered my question.

Let y = (x + 2^31) % 2^32, how is making

	before(x, y) == before(y, x) == 0

any better than

	before(x, y) == before(y, x) == 1

For an unambiguous before, we must have before(x, y) != before(y, x)
if x != y.

For a more concrete example, look at the code in tcp_ack:

        /* If the ack is newer than sent or older than previous acks
         * then we can probably ignore it.
         */
        if (after(ack, tp->snd_nxt))
                goto uninteresting_ack;

        if (before(ack, prior_snd_una))
                goto old_ack;

Here we have two checks that weed out cases that we do not wish to
process.  When all data have been acknowledged, we have

	snd_nxt == snd_una

At this point, we only want the value of ack == snd_nxt == snd_una
to pass this check.  With your change, the value snd_nxt + 2^31 can
also pass this check, which may have security implications.

Granted I have not looked at other checks in the TCP path that may
prevent this code from being invoked in that case.  However, this
does illustrate the need to audit every single before/after check
if they were ambiguous.

Cheers,
-- 
Visit Openswan at http://www.openswan.org/
Email: Herbert Xu ~{PmV>HI~} <herbert@gondor.apana.org.au>
Home Page: http://gondor.apana.org.au/~herbert/
PGP Key: http://gondor.apana.org.au/~herbert/pubkey.txt

Re: [PATCH][RFC] tcp: fix ambiguity in the `before' relation

[Gerrit Renker]

|  > With the implementation now, the output of before(x,y) is reliable: it returns true
|  > if (and only if) x is indeed `before' y.
|  
|  Sorry but I don't think you've answered my question.
|  
|  Let y = (x + 2^31) % 2^32, how is making
|  
|  	before(x, y) == before(y, x) == 0
|  
|  any better than
|  
|  	before(x, y) == before(y, x) == 1
|  
|  For an unambiguous before, we must have before(x, y) != before(y, x)
|  if x != y.
I now see where you are coming from. This requirement

 * is fulfilled in both definitions as long as y != (x + 2^31) % 2^32
 * does not hold in both definitions when      y == (x + 2^31) % 2^32

The reason is in the underlying principle: due to sequence number wrapping, we are dealing
with circular arithmetic, and in circular arithmetic the mid of the range is ambiguous
(example: clock minute hands - 30 is as much `after' as it is `before').

This problematic case has been discussed before: RFC 1982 provides some background, and we
had quite some discussion about similar issues (48 bit sequence numbers) on dccp@vger.

So the short answer is - this kind of unambiguous `before' can not be implemented (see in
particular also the notes in sec. 3.2 of RFC 1982). 

The key point where the new definition differs from the old is that _the relation_
before(x,y) is unambiguous: the case "before(x,y) && before(y,x)" will no longer occur.

|  For a more concrete example, look at the code in tcp_ack:
|  
|          /* If the ack is newer than sent or older than previous acks
|           * then we can probably ignore it.
|           */
|          if (after(ack, tp->snd_nxt))
|                  goto uninteresting_ack;
|  
|          if (before(ack, prior_snd_una))
|                  goto old_ack;
|  
|  Here we have two checks that weed out cases that we do not wish to
|  process.  When all data have been acknowledged, we have
|  
|  	snd_nxt == snd_una
|  
|  At this point, we only want the value of ack == snd_nxt == snd_una
|  to pass this check.  With your change, the value snd_nxt + 2^31 can
|  also pass this check, which may have security implications.
This is true: with the old definition it is at this point certain that ack == snd_nxt.
The reason is that the code implicitly relies on the way `before' is defined. 

That has been the reason why this has been sent as an `RFC' patch: I am sure that the
new definition is is in itself better, but was not sure how it would work with the
existing code. 

With DCCP the case is different: it is a new protocol and an unambiguous `before' relation
is beneficial, since this can increase the accuracy of detecting loss. 

Since there is likely more code which implicitly relies on the old definition,
I will send a patch shortly.

Many thanks,
Gerrit

Re: [PATCH][RFC] tcp: fix ambiguity in the `before' relation

[Herbert Xu]

On Thu, Jan 04, 2007 at 12:49:02PM +0000, Gerrit Renker wrote:
> 
> The key point where the new definition differs from the old is that _the relation_
> before(x,y) is unambiguous: the case "before(x,y) && before(y,x)" will no longer occur.

This is highly dependent on how the before macro is used in actual code.
There is nothing to suggest that this change won't create new security
holes in DCCP or any other protocol that uses this macro.  The only
way to be sure is to audit every single use.

So I think we need to do one of two things:

1) Audit every single before/after check to ensure that it works
correctly with the new definition.
2) Change before/after such that before(x, x+2^31) == !before(x+2^31, x).

Cheers,
-- 
Visit Openswan at http://www.openswan.org/
Email: Herbert Xu ~{PmV>HI~} <herbert@gondor.apana.org.au>
Home Page: http://gondor.apana.org.au/~herbert/
PGP Key: http://gondor.apana.org.au/~herbert/pubkey.txt

Re: [PATCH][RFC] tcp: fix ambiguity in the `before' relation

[Gerrit Renker]

|  > The key point where the new definition differs from the old is that _the relation_
|  > before(x,y) is unambiguous: the case "before(x,y) && before(y,x)" will no longer occur.
|  
|  This is highly dependent on how the before macro is used in actual code.
|  There is nothing to suggest that this change won't create new security
|  holes in DCCP or any other protocol that uses this macro.  The only
|  way to be sure is to audit every single use.
I fully agree, merely changing the definition means going only half way.
  
|  So I think we need to do one of two things:
|  
|  1) Audit every single before/after check to ensure that it works
|  correctly with the new definition.
For DCCP I will perform such an audit and post the results to dccp@vger. 

With regard to TCP: I am heavily snowed under with other work at the moment. If there
are experienced TCP people on the list who would be happy to look at this, it would be
great. I counted the number of times before() is used - it amounted to 68. There are
of course obvious cases which are quick to dismiss, but in particular the example you
presented yesterday points out that careful analysis is needed.

I asked Dave to revert to the old TCP definition (patch has been committed); for the moment
this seems the safest thing to do.
     
|  2) Change before/after such that before(x, x+2^31) == !before(x+2^31, x).
This is what the new definition does: in the old definition we always have that
before(x, x+2^31) == before(x+2^31, x).

Re: [PATCH][RFC] tcp: fix ambiguity in the `before' relation

[Herbert Xu]

On Fri, Jan 05, 2007 at 11:51:16AM +0000, Gerrit Renker wrote:
>      
> |  2) Change before/after such that before(x, x+2^31) == !before(x+2^31, x).
> This is what the new definition does: in the old definition we always have that
> before(x, x+2^31) == before(x+2^31, x).

Sorry but the new definition has exactly the same problem since

	before(x, x+2^31) == before(x+2^31, x) == 0

While the old definition had

	before(x, x+2^31) == before(x+2^31, x) == 1

Both are equally bad.  It's only unambiguous if

	before(x, x+2^31) == !before(x+2^31, x) == 0

or

	before(x, x+2^31) == !before(x+2^31, x) == 1

Cheers,
-- 
Visit Openswan at http://www.openswan.org/
Email: Herbert Xu ~{PmV>HI~} <herbert@gondor.apana.org.au>
Home Page: http://gondor.apana.org.au/~herbert/
PGP Key: http://gondor.apana.org.au/~herbert/pubkey.txt

Re: [PATCH][RFC] tcp: fix ambiguity in the `before' relation

[Gerrit Renker]

Quoting Herbert Xu:
|  On Fri, Jan 05, 2007 at 11:51:16AM +0000, Gerrit Renker wrote:
|  >      
|  > |  2) Change before/after such that before(x, x+2^31) == !before(x+2^31, x).
|  > This is what the new definition does: in the old definition we always have that
|  > before(x, x+2^31) == before(x+2^31, x).
|  
|  Sorry but the new definition has exactly the same problem since
|  
|  	before(x, x+2^31) == before(x+2^31, x) == 0

You are right. Sorry, I misread the text. Please see below.


|  While the old definition had
|  
|  	before(x, x+2^31) == before(x+2^31, x) == 1
|  
|  Both are equally bad.  It's only unambiguous if
|  
|  	before(x, x+2^31) == !before(x+2^31, x) == 0
|  
|  or
|  
|  	before(x, x+2^31) == !before(x+2^31, x) == 1
Implementing such a solution is a challenge - RFC 1982 suggests here (sec. 3.2):
 "Thus the problem case is left undefined, implementations are free to
  return either result, or to flag an error, and users must take care
  not to depend on any particular outcome."

I think that a definition which satisfies before(x, x+2^31) != !before(x+2^31, x)
will be more complex to implement and will need more instructions.

To illustrate with an example, if we assume that `before' operates on minutes and uses
modulo-60 arithmetic, the above requirement becomes

	before60(x, x+30)   !=   before(x+30, x)

On a clock, one cannot tell this when we merely look at the minute hands: "half before xx o'clock" 
is the same as "xx o'clock before half". Only if we also take the hour hand into consideration, the
statement "half before 2:00 o'clock" becomes unambiguous (although one would rather say "half past 
1:00 o'clock" :-). 

With regard to 31-bit sequence numbers, this would mean that we need additional information to enforce

	before(x, x+2^31) != before(x+2^31, x)

Taking the clock example further, it could be disambiguated by using 33 bits, but then the same problem
crops up with regard to modulo-2^33 arithmetic: how to disambiguate the case for x and x+2^32.

Please let me restate the differences between the old and new definition:

1) Old definition has the following list of exclusive-or cases
	* x == y				- identity
	* before(x, y) && !before(y, x)		- x `before' y and y != (x + 2^31) % 2^32
	* before(y, x) && !before(x, y)		- y `before' x and y != (x + 2^31) % 2^32
	* before(x, y) && before(y, x)		- y == (x + 2^31) % 2^32

2) New definition has the following list of exclusive-or cases
	* x == y				- identity
	* before(x, y)				- x `before' y and y != (x + 2^31) % 2^32
	* before(y, x) 				- y `before' x and y != (x + 2^31) % 2^32
	* !before(x, y) && !before(y, x)	- y == (x + 2^31) % 2^32

Since the old definition is not used in the way "before(x, y) && !before(y, x)", but rather in the
fashion "before(x, y)" or "after(y, x)", the main advantage of the new definition is that it makes
this type of use a safe case. 

My view is that this is as good as one can get; if you have a suggestion of how one could also
disambiguate before(x, x+2^31) != before(x+2^31, x), can you please let me know.


Gerrit

Re: [PATCH][RFC] tcp: fix ambiguity in the `before' relation

[Herbert Xu]

On Fri, Jan 05, 2007 at 12:49:13PM +0000, Gerrit Renker wrote:
> 
> Since the old definition is not used in the way "before(x, y) && !before(y, x)", but rather in the
> fashion "before(x, y)" or "after(y, x)", the main advantage of the new definition is that it makes
> this type of use a safe case. 

This is not true because

	if (before(x, y))
		goto drop;

means that you're effectively using it as !before(x, y).  In other words,
the change is good if our code read

	if (before(x, y))
		process_packet();

Cheers,
-- 
Visit Openswan at http://www.openswan.org/
Email: Herbert Xu ~{PmV>HI~} <herbert@gondor.apana.org.au>
Home Page: http://gondor.apana.org.au/~herbert/
PGP Key: http://gondor.apana.org.au/~herbert/pubkey.txt

Re: [PATCH][RFC] tcp: fix ambiguity in the `before' relation

[Gerrit Renker]

|  > Since the old definition is not used in the way "before(x, y) && !before(y, x)", but rather in the
|  > fashion "before(x, y)" or "after(y, x)", the main advantage of the new definition is that it makes
|  > this type of use a safe case. 
|  
|  This is not true because
|  
|  	if (before(x, y))
|  		goto drop;
|  
|  means that you're effectively using it as !before(x, y).  In other words,
|  the change is good if our code read
|  
|  	if (before(x, y))
|  		process_packet();
|  
That is correct - whether it is indeed safe(r) to use needs to be evaluated in the individual context.