Hacker News Reader

Comment by sanxiyn | Hacker News Reader

Note that you can write safe C code. seL4 is written in C! (And verified in Isabelle.) If that is too hard core, PolarSSL is a normal looking C code, which still has been proved to lack any buffer overflow. https://trust-in-soft.com/polarssl-verification-kit/ has details.

On the other hand, it probably is less effort to rewrite PolarSSL in Rust than doing that proof.

View on HN

> On the other hand, it probably is less effort to rewrite PolarSSL in Rust than doing that proof.

It's probably even less effort to convert to SaferCPlusPlus[1] (essentially a memory-safe subset of C++). There's even an tool[2] (under construction, but functional) to do a lot of the conversion for you.

[1] shameless plug: https://github.com/duneroadrunner/SaferCPlusPlus

[2] https://github.com/duneroadrunner/SaferCPlusPlus-AutoTransla...

SaferCPlusPlus is not memory safe, according to your documentation.

For one thing, the "this" pointer problem is pretty much unsolvable in C++.

> For one thing, the "this" pointer problem is pretty much unsolvable in C++.

Well, you could just avoid/prohibit the explicit and implicit use of the "this" pointer. I.e. prohibit non-static member functions[1], right?

[1] https://github.com/duneroadrunner/SaferCPlusPlus#practical-l...

Does anyone actually want to program in "C++ with instance methods banned"?

Why not just use a language designed for memory safety (which is most of them)? It's a whole lot easier, plus you get an ecosystem of actually safe code.

> Does anyone actually want to program in "C++ with instance methods banned"?

Well, passing a "safe this" pointer as the first parameter to a (static) member function isn't that hard to get used to, is it?

But I don't disagree with your gist. If memory-safety is your only concern and you're not trying to salvage an existing codebase, then Rust might be a better choice.

But if you're trying to add memory safety to, say, an existing C implementation of SSL, the SaferCPlusPlus route would probably be less effort. Even when non-static member functions are banned.

> (which is most of them)

Personally, I consider RAII (deterministic destructors) an essential feature for safe, efficient programming at scale. That leaves only two choices, C++ and Rust, right?

And if there's a memory-safe C++ option available, there are some arguments for choosing it over Rust.

I think the seL4 kernel rather proves that you can write safe haskell, verify it, and then transpile that to C.

That's different from directly writing C...

Well, you aren't directly writing C anyway. Unless you are https://xkcd.com/378/ -- using tools is perfectly okay.

Anyway, PolarSSL is definitely not transpiled. Its source language is C.

http://www.cvedetails.com/vulnerability-list/vendor_id-12001...

... and your point is?

EDIT: more recent bugs:

https://tls.mbed.org/security

These bugs include double-free and use-after-free - which are not covered by the original analysis, right?

in the end the idea is that if you are semantic aware, then everything is safe; it's just operations from exp -> env -> store to env -> store etc etc

Indeed! You can write safe programs for e.g. the original Turing Machine.

But I bet you'll end up writing tools to make creating a safe program of any non-trivial size feasible. A large class of these tools is usually called "programming languages".

There are several safe dialects of C. The issue is that almost no one is using them and they're not about to start to either.

A lot of infrastructure software has not been built with security in mind, but the game has changed, and this old C software is getting eviscerated.

If one looks at the fixes for these buffer overflows in dnsmasq, no other conclusion can be drawn except that holes are plugged in a leaky sieve. This could work for software that's done, eventually. But if something's under maintenance, using plain C is security suicide.

I think PolarSSL showed it can be done with reasonable effort and it is not a suicide.

I would really like to see a comparison of the efforts of a) writing a program in a safe language like rust and b) writing the language in C and verifying it with a toolset like the one used by the polarssl guys.

Given that the number of C projects that use similar toolsets is... low (?), I'd guess that said comparison would favor rust, but I'm prepared to be surprised :-)

Correct me if I'm wrong, but is this Frama-C and ACSL? That doesn't look like plain C to me.

In the ACSL manual in Example 2.10, does the programmer have to add the asserts? What if they make a mistake in the annotation?

So, where does this come in: http://www.securityweek.com/high-severity-vulnerability-foun...

Easy, it was out of scope. Quoting the report, "This report states the immunity of the PolarSSL software component to widespread CWEs, provided that PolarSSL is deployed in a context where... The server is configured as to never ask for client-side certificates". Quoting the news, "Servers that don't ask for client certificates are not impacted".

TrustInSoft could prove that part of code too. There's nothing special about it. It's just that they didn't bother.

It doesn't. It's not a buffer overflow issue.

It's an uninitialized read, and PolarSSL is actually also proven to lack uninitialized reads. It's just that asn1_get_sequence_of was not included in verification (as it is unreachable in verified configuration).

Which shows you the limit of verification toolsets vs. a verifying compiler. To verify that the code is 100% free of uninitialized reads or uses-after-free the static analyzer would have to scan through all possible permutations.

Sure, you can get very close to 100% in practice, but even if you're fine with this level of guarantee, the amount of discipline and cognitive overhead required for doing that in C makes Rust's learning seem like a piece of cake.

Reply on news.ycombinator.com