[zeveb]

It's yet another in a long line of bugs due to C. It is, of course, possible to have bugs in every language. Even in a theoretical bug-free language it'd be possible to flawlessly implement a buggy algorithm or standard. But some languages make some sorts of bug difficult, and others make them easy: C is in the latter group.

I suspect that assembler for the primitives and a good, sane high-level language (Haskell? Caml? Lisp?) would yield far more secure software than C. There are issues with relocatable memory and zeroing of keys, but those are, I think, addressable at the implementation level.

[acqq]

I don't have an impression that any of the mentioned languages can provide reasonable alternative to the library written in C or the equivalently compatible language, and the only language that it appears to me to have a chance to have such an implementation could be Rust, but somehow even there it appears to be too hard to do so and/or too little commercial interest to make something "good enough" for the most of the potential users. The Rust community doesn't have to implement all the functionality of Open SSL, but if it would produce at least just a proof of concept (e.g. just a minimal set of algorithms) which would prove both the capability to achieve the same speed and the provably higher security, that would be, I think, a huge start.

That would mean not wrapping the whole OpenSSL library in Rust calls but having some as minimal as possible, the tightest of the tightest loops implemented in ASM and everything else in clean and "secure" (not downgraded to the C freedom) Rust which would also pass the benchmarks and be capable to be called "on the high level" from the C code to which that library could be linked (probably the Rust code would not use GC or if it would it would have to be some so simple and minimal one that it would work by eventually calling the C malloc for bigger blocks and cause no different delays than the good written C). Not easy but I think theoretically possible for Rust. Once it would be achieved, implementing other algorithms would be possible to be done by different people and organizations.

I guess in order to achieve these goals the language designers would have to directly decide to support them, but I'd be glad if the status is already different. But I really believe that would be a huge argument for Rust: being provably more secure than C and achieving ability to implement effective drop-in replacements for C security libraries. Is it too high a goal?

I don't know how far we are from something like that, but maybe some Rust insider can estimate? What's still missing and how far we are from the point where what I described would be possible to implement?

[nickpsecurity]

Already done in Ocaml for projects willing to use something other than OpenSSL:

https://github.com/mirleft/ocaml-tls

It's performance was within 80% or so of regular TLS with Ocaml's safety and easier verification. Quite a few components were purely functional, too. I've seen SML embedded in LISP's and PreScheme compiled to efficient C or ASM. So, that means a static LISP could handle it piggybacking on C compilers. Ivory embeds a subset of C in Haskell to keep things easy to analyze and automatically safe. Parts of a SSL library could use it.

http://ivorylang.org/ivory-introduction.html

So, Haskell, LISP, and ML are already capable of replacing our SSL libraries if people choose. One is already done in Ocaml. COGENT, if people apply it to this, will take it further by having an easier-to-verify implementation in functional language with certified compilation to C or assembly.

[pjmlp]

There is also the F* version, which can be made to target C via their KreMlin compiler.

https://project-everest.github.io/

https://fstarlang.github.io/general/2016/09/30/introducing-k...

Presented at this year's ICFP conference.

https://www.youtube.com/watch?v=sP7PRHn9iEA

[nickpsecurity]

I reposted your link on Lobste.rs. I noted that COGENT already was doing verified functional with certified translation to C or assembly. Also that F star to C seems to be Microsoft and INRIA's route. So, at least two projects are making it much easier to verify algorithms or protocols in functional way with C code resulting.

The other thing I noted is that most code meant for verification is designed to be easy for humans or machines. The F star and C is one of few that is easy for both. I rarely see that.

[pjmlp]

On the talk that they did, the guy from F* team mentioned that their goal was to be able to validate that the C code is correct and they can match 1:1 the language constructs, to allow for proper verification of the generated code.

[acqq]

Thanks, but which of those can be simply taken as the library linked to C code and called from the C code, and so that it doesn't depend on GC? Because as long as that step doesn't exist, it can't be used as the possible substitution for the current libraries?

[nickpsecurity]

Ocaml is only one that uses GC IIRC. Others produce C.

[acqq]

Links please? Any actual library produced and linkable, even with just one algorithm? I can't find it behind that Ivory link? Thanks!

Edit: also thanks for explaining the nature of the solutions you mention ("custom jobs").

[nickpsecurity]

I dont have those. They're used for custom jobs by people who know the language. Im not in that category. ;)

[nickpsecurity]

Wait, I just remembered COGENT people did a case study by doing ext2 filesystem in COGENT. They have COGENT on Github. The filesystem source or binary might be in repo(s) of COGENT team allng with other examples. So, Google that.

[steveklabnik]

See https://crates.io/crates/ring , which is a fork of boringSSL, porting the C over to Rust. Endgame is 100% Rust and asm.

https://crates.io/crates/rustls is a TLS library built on top of ring.

[acqq]

Can it be used from C, e.g. C that statically links the library? Does it depend on the GC? What is the current speed? Thanks!

Edit: Re "just know they exist" (meaning libraries) in the answer: That's why I started the topic, the people who use only C wouldn't have chance to try the library unless the people who know enough Rust give something explicit that works and can be actually tested in linkability, functionality and speed.

[steveklabnik]

  > Does it depend on the GC?

Rust has no GC.

I am not sure about your other questions, as I haven't used them directly, I just know they exist. :) The former is possible, but I don't know if the authors have done any work on that.

[nickpsecurity]

They can even use a typed, assembly language if they want to have handwritten ASM and prove memory safety. Just no interest outside CompSci types.