search

mirleft / ocaml-asn1-combinators

Embed typed ASN.1 grammars in OCaml
ISC License
35 stars 20 forks source link

Integer overflows in p_big_tag and p_big_length calculation #2

Closed andreasdotorg closed 10 years ago

andreasdotorg commented 10 years ago

big tags and big lengths can overflow OCaml's integer representation, resulting in wrong values. Unlike in C implementations, this does not result in memory corruption issues, but still might allow for dirty tricks that are based on changing the interpretation of the data.

pqwy commented 10 years ago

This means that:

While it might be worth looking into, I fail to see how is this more of a problem than receiving messages with tags or lengths that are simply wrong?

pqwy commented 10 years ago

Actually, after some thinking I'm beginning to see a problem: it's not in changing the interpretation, it's precisely in redundancy. You get to construct almost arbitrary prefixes for your tags and lengths, which could be used to mine the message space in the spirit of this.

pqwy commented 10 years ago

Tightened via https://github.com/pqwy/ocaml-asn1-combinators/commit/c9ca9b87a9946c97fe27c287ad3b2dee0f0b8574. Thank you!

andreasdotorg commented 10 years ago

Actually, I was thinking more along the lines of getting a signature on an X.509 certificate with a mangled tag field that is meaningless to the CA, so they will sign it, but which translates into subjectAltName=* in an implementation that wraps integers. Presto, certificate valid for all domains.

Also, can you find out whether you're actually running on a 64 bit platform? Your fix is only valid on 64 bit (you're probably aware of this...).

andreasdotorg commented 10 years ago

Turns out this is a known attack: https://www.viathinksoft.de/~daniel-marschall/asn.1/oid_facts.html#chap8

pqwy commented 10 years ago

Wow oh wow.

The CA won't ever sign a cert with a mangled tag, because in its interpretation the cert is unparsable (or at least non-grammar-conformant). That's why I couldn't wrap my head around why this would matter, initially.

But I just started realizing how bad things can get with overflows in other places, and in particular in the OID code which uses the same encoding scheme the tags use...

( See https://github.com/pqwy/ocaml-asn1-combinators/blob/f26b1e48b604733ca82982bae2cdf5f25d8b2196/src/prim.ml#L263 )

This is actually a very, very good catch.

( And yes, I know the bound is 64-bit specific. The "XXX 7 bytes" comment above the check is meant to remind me of that, when proper architecture support lands. I don't want to hack in a quick [and local] runtime check, it's something that needs to be dealt with in a more principled way. )

andreasdotorg commented 10 years ago

http://caml.inria.fr/pub/docs/manual-ocaml/libref/Big_int.html might make your life easier here.

pqwy commented 10 years ago

It's already making it harder. (Num)

My life is made easier by zarith these days and num is on the way out.

I am contemplating using bignums here too, actually. It's a balancing act.

hannesm commented 10 years ago

@andreas23 mentioned this was demonstrated in http://events.ccc.de/congress/2009/Fahrplan/events/3658.en.html by dan kaminsky... where unfortunately only video exists, but no slides

pqwy commented 10 years ago

Latest in this saga: large tags and lengths are parsed as Int64, then converted into int with size-checking.

Tags and lengths still can't exceed OCaml's native int (giving sizes of up to about 4EB and tags up to 9,223,372,036,854,775,807 on x86_64).

Given that no tags I've ever seen go above 30, this limitation is more reasonable than it might seem.