Live data from Hacker News

Building on Rock, Not Sand

robert.ocallahan.org

21–30 of 112 posts

Re: Building on Rock, Not Sand

#21
post #17

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.

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

Re: Building on Rock, Not Sand

#22
post #20
post #17

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.

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.

Re: Building on Rock, Not Sand

#23
post #17

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.

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.

Re: Building on Rock, Not Sand

#24
If someone thinks that compiler for their favorite programming language provides safety they have no idea what safe code is.

C/C++ is used to write safe code for medical and aerospace applications every day. The compiler for the languages like C, C++, Ada, Rust or whatever, is not enough.

You can get better static and dynamic code analysis and test coverage analysis tools for C/C++/Ada than you can for Rust.

Re: Building on Rock, Not Sand

#25

If someone thinks that compiler for their favorite programming language provides safety they have no idea what safe code is. C/C++ is used to write safe code for medical and aerospace applications every day. The compiler for the languages like C, C++, Ada, Rust or whatever, is not enough. You can get better static and dynamic code analysis and test coverage analysis tools for C/C++/Ada than you can for Rust.

The term 'safe' varies a lot based on context. In this context it is being used to mean 'memory safe' - i.e. that the compiler can eliminate a class of behaviour that are the root of a number of recent security issues.

"Safe" in the context of medical and aerospace means something very different, but is much closer to the meaning of "Secure" in this context. No compiler is ever going to prevent you writing insecure code - there can always be a logic problem, bad choice of crypto algorithm etc..

Re: Building on Rock, Not Sand

#26
post #21
post #17

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.

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.

Re: Building on Rock, Not Sand

#27

Another rust proponent lecturing the world on how they should rewrite everything in rust. yawn

It was subtle but he put 'Rewrite in Rust' in caps, which I took to mean that it was a self aware use of a meme, while still making a valid point.

Re: Building on Rock, Not Sand

#29
post #23
post #17

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.

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

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

Re: Building on Rock, Not Sand

#30
post #10

Talk is cheap; show me the code. There's a lot of talk about rewriting some crucial pieces in Rust but no actual work to follow it.

https://github.com/bluejekyll/trust-dns

Fyi... that Rust project doesn't actually cover the functionality of dnsmasq.

Dnsmasq also includes a DHCP server and the ability to read a blacklist to act as an ad blocker. In contrast, the "trust-dns" project is more of a replacement for the "bind" program instead of "dnsmasq".

If your intention was to only show that "non trivial Rust code exists", that's fine. However, some others might get the wrong impression that it's a Rust version of dnsmasq.

Post reply on HN