Add Amazon s2n

[jldodds]

Amazon released a reasonably compact TLS library that has apparently already undergone a few external security audits: https://blogs.aws.amazon.com/security/post/TxCKZM94ST1S6Y/Introducing-s2n-a

https://github.com/awslabs/s2n

[TomMD]

As I said on twitter, notice this library still leverages parts of OpenSSL - largely for the algorithms. I'm not saying there isn't anything here to audit, but as far as automated SAW-like analysis this is covered by any review of OpenSSL (and for the sake of the internet buzz today - the notion being headlined, that you can drop the OpenSSL library, is premature at best).

[dagit]

Tom,

According to the announcement, you can (or will be able to in the future) drop libssl, but libcrypto is meant to stick around. From their announcement:

s2n isn’t intended as a replacement for OpenSSL, which we remain committed

to supporting through our involvement in the Linux Foundation’s Core Infrastructure Initiative. OpenSSL provides two main libraries: “libssl”, which implements TLS, and “libcrypto,” which is a general-purpose cryptography library. Think of s2n as an analogue of “libssl,” but not “libcrypto.”

So I would conclude that the internet buzz is simply mistaken. Also, I could be wrong, but it also sounds like analyzing the s2n portion of OpenSSL is much easier than doing a blanket analysis of OpenSSL. If for no other reason that it should be much smaller and simpler. But who knows how much of OpenSSL gets reused as primitives for s2n.

On Tue, Jun 30, 2015 at 2:50 PM, Thomas M. DuBuisson < notifications@github.com> wrote:

As I said on twitter, notice this library still leverages parts of OpenSSL

• largely for the algorithms. I'm not saying there isn't anything here to audit, but as far as automated SAW-like analysis this is covered by any review of OpenSSL (and for the sake of the internet buzz today - the notion being headlined, that you can drop the OpenSSL library, is premature at best).

— Reply to this email directly or view it on GitHub https://github.com/GaloisInc/hacrypto/issues/97#issuecomment-117354952.

[atomb]

From my brief look at the code, s2n re-implements the TLS protocol implementation, but uses one of several possible underlying libraries for the key cryptographic primitives. However, I think those primitives tend to be pretty trustworthy. We've verified a few of the ones in OpenSSL and could relatively easily verify others using SAW. The s2n code itself is probably largely outside of the domain that SAW is currently good at, but I think a proof of the absence of undefined behavior using Frama-C is close to being feasible. There are a few places where we might have to axiomatize some things, but after that I think a lot of the rest of the code might go through relatively well.