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.
Building on Rock, Not Sand
21–30 of 112 posts
Re: Building on Rock, Not Sand
#22Note 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...
Anyway, PolarSSL is definitely not transpiled. Its source language is C.
Re: Building on Rock, Not Sand
#23Note 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.
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
#24C/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
#25If 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.
"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
#26Note 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...
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
#27Another rust proponent lecturing the world on how they should rewrite everything in rust. yawn
Re: Building on Rock, Not Sand
#28Talk 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.
Re: Building on Rock, Not Sand
#29Note 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.…
Re: Building on Rock, Not Sand
#30Talk 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
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.