Openssl : The heartbleed bug

[chotu s]

Hello,

I have not looked at this bug details(I quickly glanced) , but here are some of my thought.

People should seriously start looking at ATS2 .  I think big organization/companies need to take a look  ATS2 and may be fund its development and training .  I think ATS2 is more practical since proofs and specs does not stop you in anyway writing a efficient program in most of the cases. It also allows us to control the expressive the spec system we want depending on the nature of the system.

It is true that no one has magic wand and one can get specification also wrong, but specs as a type is a good idea .

This year I am very busy , but next year I will plan to spread word about ATS with demos.

Thanks

[chotu s]

typo :
It also allows us to control how expressive the spec system we want depending on the nature of the system.

[chotu s]

Some details here : http://blog.existentialize.com/diagnosis-of-the-openssl-heartbleed-bug.html

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/c61766a6-00bf-4072-908a-424e899f511f%40googlegroups.com.

[gmhwxi]

This is clearly something that one can expect to prevent if ATS is used.

[Chris Double]

On Wed, Apr 9, 2014 at 5:53 PM, gmhwxi <gmh...@gmail.com> wrote:
> This is clearly something that one can expect to prevent if ATS is used.

This is the patch that fixed the heartbleed bug:

<http://git.openssl.org/gitweb/?p=openssl.git;a=commitdiff;h=96db9023b881d7cd9f379b0c154650d6c108e9a3>

An exercise for someone interested might be to reimplement the
affected function in ATS and show how it would have prevented the
error. You could even integrate this with the openssl source such that
it builds with the ATS function.

--
http://www.bluishcoder.co.nz

[gmhwxi]

I saw the following line of code:

r = dtls1_write_bytes(s, TLS1_RT_HEARTBEAT, buffer, write_length);

In ATS, it is reasonable to expect that one would give [dtls1_write_bytes] an interface
that requires a proof showing that it is safe to write out the bytes in [s].


r = dtls1_write_bytes(pf | s, TLS1_RT_HEARTBEAT, buffer, write_length);

It really takes a superman to write safe code in C :(

[chotu s]

Not too sure if I understand it properly  but from what I gather is that it a kind of ping reply where memory leaks across network , where sender claims that his payload buffer B has length L which is actually fake but has length L'  which is less than L.  Receiver creates a buffer of length L and copies data from B whose actual length is L'  , this copies extra bytes L-L' after L' bytes.

--

You received this message because you are subscribed to the Google Groups "ats-lang-users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/5077bf13-19ea-4e78-b011-cd8355cddb65%40googlegroups.com.

[gmhwxi]

By the reading the code, I see that the problem is essentially like a dual to
the well-known buffer overrun problem. The bottom line is a very old lesson:
one needs to be extremely careful when using memcpy:

memcpy (dst, src, n)

Usually, a problem with memcpy is that dst is shorter than n, which causes buffer overrun.
In this case, src is shorter than n, which can cause bytes containing secrets to be copied out.

Basically, if the requester wants N bytes, then the sender *always* gives him N
bytes even when the sender himself does not have N bytes. The fix is simple: the sender
makes sure that he can only give out bytes that he really has:

if (1 + 2 + payload + 16 > s->s3->rrec.length) return 0; /* silently discard per RFC 6520 sec. 4 */

Another (more lenient) way to do it is to re-adjust payload to be s->s3->rrec.length-16-2-1, the maximal allowed value.


[chotu s]

Just for discussion and quick ref only ,  a quick grep give me 779 instances of memcpy in source code of latest openssl.

I believe  in ATS2 when copying memory from source to destination , proof will be need for both src and dst and this should not happen in  ATS2.

Of course when using unsafe code in ATS2 all bets are off.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/c3b8786f-73f0-482d-ae78-5f7c2a870ee6%40googlegroups.com.

[gmhwxi]

>> Of course when using unsafe code in ATS2 all bets are off.

The first layer of defence is always the programmer.

Even if you use unsafe code, you could be required to provide a proof
by introducing a praxi. Following such a process can already stop a large majority of
such bugs.

[Chris Double]

I've created a branch of openssl with the bugfix reverted and some
infrastructure to implement code in ATS2:

<https://github.com/doublec/openssl/tree/ats>

This branch just replaces the dtls1_process_heartbeat function with an
ATS version. The ATS version is in 'ssl/d1_both.dats'. It just a
copy/paste of the buggy C code wrapped in a %{ ... %} block. The
ssl/Makefile uses patsopt to compile this to C and include it in the
openssl library. I comment out the old C function in ssl/d1_both.c.

To build:

$ git clone git://github.com/doublec/openssl
$ cd openssl
$ git checkout -b ats ats
$ ./config
$ make
$ make test

The next step would be to modify d1_both.dats to implement the
function in ATS and show some ATS features that would detect the bug.
Then implement the fix and show how this then compiles (hopefully!).
I'm hoping to get time to write a blog post about this to show some
ATS features. Any thoughts on the approach and ways to use ATS
welcome.

--
http://www.bluishcoder.co.nz

[gmhwxi]

I took a look.

The C code is really "wild" and it would require a big effort to translate
it into ATS. Also, the ATS code translated from the C code would probably
scare people.

I propose a less demanding approach that may be much easier to gain
acceptance by C programmers.

First, let us see some code:

typedef region_proof = int
extern region_proof region_assert (void *p, size_t n) ;
extern region_proof region_contain (int proof, void* p, size_t n, void* p1, size_t n1);

extern
void *memcpy_safe (region_proof, region_proof, void *dst, void* src, int n);

The idea is very simple:

region_assert is like a crypto hash function; it generates a hash value for p and n
combined.

region_contain (pf, p, n, p1, n1) does three things:

1) it checks that [pf] is the hash value for p and n;
2) it checks that p <= p1 and p1+n1 <= p+n
3) it generates a hash value for p1 and n1

memcpy_safe (pf_dst, pf_src, dst, src, n) does 3 three things

1) it checks that pf_dst is a region proof for (dst, n)
2) it checks that pf_src is a region proof for (src, n)
3) it calls memcpy (dst, src, n)

Of course, proof construction and proof-checking can be readily
erased in production code.

The point of having such a mechanism is to allow C programmers
can at least start to think like ATS programmers. I have a hunch that this
may initiate a trend that can greatly enhance memory safety in C programming
and possibly lure people into learning ATS :)

Cheer,

--Hongwei

[Chris Double]

On Thu, Apr 10, 2014 at 12:41 PM, Chris Double
<chris....@double.co.nz> wrote:
>
> <https://github.com/doublec/openssl/tree/ats>

This branch now contains a rough cut at an 'unsafe' version of the
dtls1_process_heartbeat function written in ATS:

<https://github.com/doublec/openssl/blob/ats/ssl/d1_both.dats>

This branch contains a safer version that does buffer size checking:

<https://github.com/doublec/openssl/blob/ats_safe/ssl/d1_both.dats>

The core of the code, without the helper functions, is in this gist:

<https://gist.github.com/doublec/10395713>

Without the assertloc's, which would be error handling checks in real
code, it doesn't compile which was the goal. There's still lots more
that could be done. I really wanted to see how well the bounds
checking worked to prevent the heartbeat attack and it seems to. I'll
implement the rest of the fix and give it a run on a live server
tomorrow and run some tests.

This is my first real use of ATS2 (vs ATS1) so I was quite unsure of
what library support and idioms exist - I'm sure I've reimplemented
things in my helper functions in places.

--
http://www.bluishcoder.co.nz

[gmhwxi]

It looks good!

I have started to design an interface for array_p (non-linear
version of array_v). I will try to turn your code into a version
that uses array_p. Using array_p can only stop bounds
violations but not memory leaks. However, the technique is
so straightforward, I have a high hope that C programmers
may actually adopt it. The heartbleed bug is just providing the
impetus we need.

[Greg Fitzgerald]

> extern fun safe_memcpy {l,l2:addr} {n1,n2:int} {n:int | n <= n1; n <= n2}
> (pf_dst: !array_v (byte?, l, n1) >> array_v (byte, l, n1), pf_src: !array_v(byte, l2, n2) |
> dst: ptr l, src: ptr l2, n: size_t n): void = "mac#memcpy"

I'm an ATS newb so having trouble reading this, but does safe_memcpy()
ensure the source and destination buffers do not overlap? If they do
overlap, it would be impressive to see that code reroute to memmove()
(instead of failing to type-check). Is that possible with ATS?

Thanks,
Greg

> --
> You received this message because you are subscribed to the Google Groups
> "ats-lang-users" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to ats-lang-user...@googlegroups.com.
> To post to this group, send email to ats-lan...@googlegroups.com.
> To view this discussion on the web visit

> https://groups.google.com/d/msgid/ats-lang-users/956b3de3-cc6d-4e5e-bd9d-8c8fa6531829%40googlegroups.com.

[gmhwxi]

Yes, it ensures non-overlapping.

[Chris Double]

I wrote a blog post about the OpenSSL work with ATS and it hit hacker news:

<https://news.ycombinator.com/item?id=7571385>

Original post is:

<http://bluishcoder.co.nz/2014/04/11/preventing-heartbleed-bugs-with-safe-languages.html>

--
http://www.bluishcoder.co.nz

[chotu s]

@Chris Double nice! .

--
http://www.bluishcoder.co.nz

--
You received this message because you are subscribed to the Google Groups "ats-lang-users" group.

To unsubscribe from this group and stop receiving emails from it, send an email to ats-lang-user...@googlegroups.com.
To post to this group, send email to ats-lan...@googlegroups.com.

To view this discussion on the web visit https://groups.google.com/d/msgid/ats-lang-users/CALn1vHGvUO2jodKqOAz49Ba2zBwCbDMpRO9WBxGq0X0B7kga6Q%40mail.gmail.com.

[gmhwxi]

This is great. Thanks!

Judging from the comments, I saw way too many "programming philosophers".

[Kiwamu Okabe]

Hi Chris,

On Fri, Apr 11, 2014 at 8:39 PM, Chris Double <chris....@double.co.nz> wrote:
> Original post is:
>
> <http://bluishcoder.co.nz/2014/04/11/preventing-heartbleed-bugs-with-safe-languages.html>

I have translated it into Japanese.

https://github.com/jats-ug/translate/blob/master/Web/bluishcoder.co.nz/2014/04/11/preventing-heartbleed-bugs-with-safe-languages.md

Thank's for your precious things,
--
Kiwamu Okabe at METASEPI DESIGN