Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Building on Rock, Not Sand

robert.ocallahan.org

Post reply on HN
Print view View original

31–40 of 112 posts

Re: Building on Rock, Not Sand

#31

Post by titzer »

Nokinside wrote: post #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.

> C/C++ is used to write safe code for medical and aerospace applications every day.

Crack is smoked by humans every day. This is an Argumentum ad Populum (https://web.cn.edu/kwheeler/fallacies_list.html).

And I dispute the statement anyway; what is "safe" code without a guarantee of memory safety?

Re: Building on Rock, Not Sand

#32

Post by huhtenberg »

bsder wrote: post #21
sanxiyn wrote: 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...

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

Re: Building on Rock, Not Sand

#33

Post by bjz_ »

kosma wrote: 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.

Servo, Firefox, Redox-OS, libsvg, Linker-d, GNOME, Maidsafe, pieces of Fuchsia... it's a huge effort, but it's beginning to pick up steam. I'm certainly trying to play my part as well (still private, but will be OSS).

Re: Building on Rock, Not Sand

#35

Post by xelxebar »

I'm always confused by the "safe language" evangelism. Reducing cognitive load is a Good Thing TM; I get that. But aren't we just trusting the Rust compiler and JVM to not have subtle bugs that introduce memory management errors into our programs?

Centralizing the memory management code to some well tested core---like the Rust compiler or some C lib---sounds to be the crux of wiring memory safe code, not the language.

Re: Building on Rock, Not Sand

#36

Post by sanxiyn »

huhtenberg wrote: post #32
bsder wrote: post #21

Earlier quoted context omitted.

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

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

Re: Building on Rock, Not Sand

#37

Post by bjz_ »

xelxebar wrote: post #35

I'm always confused by the "safe language" evangelism. Reducing cognitive load is a Good Thing TM; I get that. But aren't we just trusting the Rust compiler and JVM to not have subtle bugs that introduce memory management errors into our programs? Centralizing the memory management code to some well tested core---like the Rust compiler or some C lib---sounds to be the crux of wiring memory safe code, not the language…

Trouble is that in C there is no way to encapsulate the unsafe code. Rust has tools that let you do that - it's not perfect, but depending on the level you are working at you can even build operating systems like Redox with the majority of the code in safe Rust.

The language has not been formally specified which is a concern, but this is an active area that is also being worked on in collaboration with universities. This should make it easier to write unsafe code in combination with theorem provers like Lean or Coq for even greater confidence, and ensure that any soundess holes in the type system are found.

Re: Building on Rock, Not Sand

#38

Post by sanxiyn »

xelxebar wrote: post #35

I'm always confused by the "safe language" evangelism. Reducing cognitive load is a Good Thing TM; I get that. But aren't we just trusting the Rust compiler and JVM to not have subtle bugs that introduce memory management errors into our programs? Centralizing the memory management code to some well tested core---like the Rust compiler or some C lib---sounds to be the crux of wiring memory safe code, not the language…

You are right. On the other hand, in practice, implementing it in language (really, compiler) seems more effective than in library, as in reducing number of bugs. Why it is so is an interesting question, but is not very relevant to empirical basis of safe language evangelism.

Re: Building on Rock, Not Sand

#40

Post by Nokinside »

rkangel wrote: post #25
Nokinside wrote: post #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.

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

Memory safe code is the basic requirement of of safety critical code. Btw. memory safety includes checking for stack and heap exhaustion.
Post reply on HN