Openssl : The heartbleed bug

Google Group
1

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

2

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.On Wednesday, April 9, 2014 4:19:50 AM UTC-4, chotu s wrote:

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.

On Wed, Apr 9, 2014 at 11:55 AM, gmhwxi <gmh...@gmail.com <javascript:>>wrote:

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 :frowning:

On Wednesday, April 9, 2014 2:04:03 AM UTC-4, Chris Double wrote:

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

–
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...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com<javascript:>
.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/5077bf13-19ea-4e78-b011-cd8355cddb65%40googlegroups.comhttps://groups.google.com/d/msgid/ats-lang-users/5077bf13-19ea-4e78-b011-cd8355cddb65%40googlegroups.com?utm_medium=email&utm_source=footer
.

3

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.On Wed, Apr 9, 2014 at 6:57 PM, gmhwxi gmh...@gmail.com wrote:

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.

On Wednesday, April 9, 2014 4:19:50 AM UTC-4, chotu s wrote:

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.

On Wed, Apr 9, 2014 at 11:55 AM, gmhwxi gmh...@gmail.com wrote:

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 :frowning:

On Wednesday, April 9, 2014 2:04:03 AM UTC-4, Chris Double wrote:

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

–
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...@googlegroups.com.
To post to this group, send email to ats-l...@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.comhttps://groups.google.com/d/msgid/ats-lang-users/5077bf13-19ea-4e78-b011-cd8355cddb65%40googlegroups.com?utm_medium=email&utm_source=footer
.

–
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/c3b8786f-73f0-482d-ae78-5f7c2a870ee6%40googlegroups.comhttps://groups.google.com/d/msgid/ats-lang-users/c3b8786f-73f0-482d-ae78-5f7c2a870ee6%40googlegroups.com?utm_medium=email&utm_source=footer
.

4

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.On Wed, Apr 9, 2014 at 11:55 AM, gmhwxi gmh...@gmail.com wrote:

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 :frowning:

On Wednesday, April 9, 2014 2:04:03 AM UTC-4, Chris Double wrote:

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

–
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.comhttps://groups.google.com/d/msgid/ats-lang-users/5077bf13-19ea-4e78-b011-cd8355cddb65%40googlegroups.com?utm_medium=email&utm_source=footer
.

5

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.On Thursday, April 10, 2014 11:55:26 AM UTC-4, Chris Double wrote:

On Thu, Apr 10, 2014 at 12:41 PM, Chris Double <chri…@double.co.nz <javascript:>> 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

6

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 :slight_smile:

Cheer,

–HongweiOn Wednesday, April 9, 2014 8:41:41 PM UTC-4, Chris Double wrote:

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

7

typo :
It also allows us to control how expressive the spec system we want
depending on the nature of the system.On Wednesday, April 9, 2014 10:41:05 AM UTC+5:30, chotu s wrote:

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

8

@Chris Double nice! .On Fri, Apr 11, 2014 at 5:09 PM, Chris Double chris....@double.co.nzwrote:

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:

<
Preventing heartbleed bugs with safe programming languages

–
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
.

9

This is clearly something that one can expect to prevent if ATS is used.On Wednesday, April 9, 2014 1:19:49 AM UTC-4, chotu s wrote:

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

On Wed, Apr 9, 2014 at 10:44 AM, chotu s <cho...@gmail.com <javascript:>>wrote:

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

On Wednesday, April 9, 2014 10:41:05 AM UTC+5:30, chotu s wrote:

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

–
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...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com<javascript:>
.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/c61766a6-00bf-4072-908a-424e899f511f%40googlegroups.comhttps://groups.google.com/d/msgid/ats-lang-users/c61766a6-00bf-4072-908a-424e899f511f%40googlegroups.com?utm_medium=email&utm_source=footer
.

10

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.

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

11

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.On Wednesday, April 9, 2014 9:52:08 AM UTC-4, chotu s wrote:

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.

On Wed, Apr 9, 2014 at 6:57 PM, gmhwxi <gmh...@gmail.com <javascript:>>wrote:

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.

On Wednesday, April 9, 2014 4:19:50 AM UTC-4, chotu s wrote:

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.

On Wed, Apr 9, 2014 at 11:55 AM, gmhwxi gmh...@gmail.com wrote:

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 :frowning:

On Wednesday, April 9, 2014 2:04:03 AM UTC-4, Chris Double wrote:

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

–
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...@googlegroups.com.
To post to this group, send email to ats-l...@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.comhttps://groups.google.com/d/msgid/ats-lang-users/5077bf13-19ea-4e78-b011-cd8355cddb65%40googlegroups.com?utm_medium=email&utm_source=footer
.

–
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...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com<javascript:>
.
To view this discussion on the web visit
https://groups.google.com/d/msgid/ats-lang-users/c3b8786f-73f0-482d-ae78-5f7c2a870ee6%40googlegroups.comhttps://groups.google.com/d/msgid/ats-lang-users/c3b8786f-73f0-482d-ae78-5f7c2a870ee6%40googlegroups.com?utm_medium=email&utm_source=footer
.

12

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,
GregOn Thu, Apr 10, 2014 at 9:10 AM, gmhwxi gmh...@gmail.com wrote:

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.

On Thursday, April 10, 2014 11:55:26 AM UTC-4, Chris Double wrote:

On Thu, Apr 10, 2014 at 12:41 PM, Chris Double chri...@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

–
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.

13

This is great. Thanks!

Judging from the comments, I saw way too many “programming philosophers”.On Friday, April 11, 2014 7:39:31 AM UTC-4, Chris Double wrote:

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:

<
Preventing heartbleed bugs with safe programming languages>

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

14

Yes, it ensures non-overlapping.On Thursday, April 10, 2014 1:57:49 PM UTC-4, Greg Fitzgerald wrote:

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

On Thu, Apr 10, 2014 at 9:10 AM, gmhwxi <gmh...@gmail.com <javascript:>> wrote:

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.

On Thursday, April 10, 2014 11:55:26 AM UTC-4, Chris Double wrote:

On Thu, Apr 10, 2014 at 12:41 PM, Chris Double chri...@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

–
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...@googlegroups.com <javascript:>.
To post to this group, send email to ats-l...@googlegroups.com<javascript:>.

To view this discussion on the web visit

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

15

Some details here :
http://blog.existentialize.com/diagnosis-of-the-openssl-heartbleed-bug.htmlOn Wed, Apr 9, 2014 at 10:44 AM, chotu s chot...@gmail.com wrote:

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

On Wednesday, April 9, 2014 10:41:05 AM UTC+5:30, chotu s wrote:

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

–
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.comhttps://groups.google.com/d/msgid/ats-lang-users/c61766a6-00bf-4072-908a-424e899f511f%40googlegroups.com?utm_medium=email&utm_source=footer
.

16

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 :(On Wednesday, April 9, 2014 2:04:03 AM UTC-4, Chris Double wrote:

On Wed, Apr 9, 2014 at 5:53 PM, gmhwxi <gmh...@gmail.com <javascript:>> wrote:

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

This is the patch that fixed the heartbleed bug:

<
git.openssl.org Git - openssl.git/commitdiff>

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