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

Blue Team Rust: What Is “Memory Safety”, Really?

tiemoko.com

Post reply on HN
Print view View original

71–80 of 105 posts

Re: Blue Team Rust: What Is “Memory Safety”, Really?

#71

Post by Jweb_Guru »

steveklabnik wrote: post #63
Jweb_Guru wrote: post #62

Earlier quoted context omitted.

Unsafe Rust can be (and has been) formally verified to satisfy its Rust type, meaning calling it from safe code can't violate memory unsafety. We don't need to trust manual inspection.

IMHO, this is going a bit too far. Some parts of unsafe Rust have had a model produced that can check some of the invariants required for safe Rust. For example, in my understanding, traits were not modeled at all. Still very promising work, but don't want to overstate it either!

I never said all unsafe Rust code was verified, but we certainly have verified the parts required for stuff like Arc and RwLock beyond reasonable doubt.

Re: Blue Team Rust: What Is “Memory Safety”, Really?

#72

Post by steveklabnik »

Jweb_Guru wrote: post #71
steveklabnik wrote: post #63

Earlier quoted context omitted.

IMHO, this is going a bit too far. Some parts of unsafe Rust have had a model produced that can check some of the invariants required for safe Rust. For example, in my understanding, traits were not modeled at all. Still very promising work, but don't want to overstate it either!

I never said all unsafe Rust code was verified, but we certainly have verified the parts required for stuff like Arc and RwLock beyond reasonable doubt.

How, when they rely on semantics that are not fully locked down? Are you referring to something other than the Rust Belt work?

Re: Blue Team Rust: What Is “Memory Safety”, Really?

#73

Post by Jweb_Guru »

steveklabnik wrote: post #72
Jweb_Guru wrote: post #71

Earlier quoted context omitted.

I never said all unsafe Rust code was verified, but we certainly have verified the parts required for stuff like Arc and RwLock beyond reasonable doubt.

How, when they rely on semantics that are not fully locked down? Are you referring to something other than the Rust Belt work?

You mean, if they were used with dynamic trait objects or unsized types or something? I suppose theoretically there could be some issue, since they aren't modeled yet, but in that case it would almost certainly be a (much more worrisome) issue with the safe part of Rust itself, not the specific unsafe code involved in those types. I don't think any proposal for how to model trait objects, for example, would change the model of how semantic types are defined, it would involve adding new semantic types and new theorems about them.

Re: Blue Team Rust: What Is “Memory Safety”, Really?

#74

Post by steveklabnik »

Jweb_Guru wrote: post #73
steveklabnik wrote: post #72

Earlier quoted context omitted.

How, when they rely on semantics that are not fully locked down? Are you referring to something other than the Rust Belt work?

You mean, if they were used with dynamic trait objects or unsized types or something? I suppose theoretically there could be some issue, since they aren't modeled yet, but in that case it would almost certainly be a (much more worrisome) issue with the safe part of Rust itself, not the specific unsafe code involved in those types. I don't think any proposal for how to model trait objects, for example, would change th…

Cool, then yes, we’re on the same page here, I am just extremely cautious when talking about this. It is true that that stuff would indicate a larger problem, but it’s not like we haven’t discovered unexpected larger problems in the past.

Re: Blue Team Rust: What Is “Memory Safety”, Really?

#75

Post by bluejekyll »

dthul wrote: post #37
nullc wrote: post #28

Earlier quoted context omitted.

It's that kind of thinking that likely contributes to the low software quality. The software failed and did so in a user uninformative way. Except in things like network facing software or whatnot --where a segfault might also be an RCE--, a panic is not superior to a segfault. A panic can even still be a vulnerability: DOS attacks are attacks too. That the failure isn't one that could have resulted in an RCE is only…

Not to discredit you, but you postulate things like "9 out of 10 times" and generally "low software quality" but don't support your statements. It certainly is not my experience that this is (more, or at all) common in the Rust ecosystem. If an application author uses things like unwrap or expect (two of the most common ways to abort the program with a panic) that is indeed lazy software engineering. But these are al…

> lazy software engineering

For production code, I agree with you. When writing PoC software, using those can speed up development, rather than forcing you to figure out the best way to deal with those options or errors upfront. Refactoring in Rust tends to also make it reliably produce production quality code when you go back and fix all that.

On the “?” In examples, that can also lead to annoyance for a new to Rust Dev, getting error return types correct, or knowing to leverage crates like anyhow, can be complex at first. Unwrap and expect are great ways to get started. I also make heavy use of them in test code.

Re: Blue Team Rust: What Is “Memory Safety”, Really?

#76

Post by bluejekyll »

XMPPwocky wrote: post #33
nullc wrote: post #28

Earlier quoted context omitted.

It's that kind of thinking that likely contributes to the low software quality. The software failed and did so in a user uninformative way. Except in things like network facing software or whatnot --where a segfault might also be an RCE--, a panic is not superior to a segfault. A panic can even still be a vulnerability: DOS attacks are attacks too. That the failure isn't one that could have resulted in an RCE is only…

There's also just not that much Rust software out there, and 80% of everything is crap. If you compare the best, say, C tool to do something against the best Rust tool, the odds that the Rust tool will be lower-quality are higher - the Rust tool is probably the only Rust tool written to do that, while the C tool is probably the best C tool that's survived over the years.

As someone who has worked with a lot of Rust libraries and applications, your estimate on quality is completely made up hyperbole with the clear intention of maligning Rust.

I have experienced far more success in using Rust and its library ecosystem than I ever have in other languages.

Yes there are bugs in somethings, yes there are others that don’t follow best practices, but throwing out a number of “80%” completely dismisses how solid and capable so many pieces of Rust software are.

Re: Blue Team Rust: What Is “Memory Safety”, Really?

#77

Post by doonesbury »

foota wrote: post #29
dataking wrote: post #7

Earlier quoted context omitted.

While some patterns that call for unsafe today might be eliminated in whole or part, code that violates the ownership and borrowing rules will have to remain unsafe. I think fuzzing is not guaranteed to reach all unsafe code paths, nor provide full test coverage. Ideally, you want a) some sort of formal proof that the unsafe code cannot violate memory safety, b) 100% branch coverage for unsafe code, or c) both (becau…

What I really want is an integration of automated proof checking with unsafe code, allowing completely safe rust programs. Additionally, this could be extended to safe code to allow removing overhead from safety in things like bounds checks and Rc.

Amen to that. Integrated formal systems giving the spec working with the programming language on the implementation side is the holy grail.

Re: Blue Team Rust: What Is “Memory Safety”, Really?

#79

Post by doonesbury »

zozbot234 wrote: post #30
foota wrote: post #29

Earlier quoted context omitted.

What I really want is an integration of automated proof checking with unsafe code, allowing completely safe rust programs. Additionally, this could be extended to safe code to allow removing overhead from safety in things like bounds checks and Rc.

This requires a formal semantics for Unsafe Rust. It's a hard problem, albeit one that's being worked on.

Any references?

Re: Blue Team Rust: What Is “Memory Safety”, Really?

#80

Post by doonesbury »

touisteur wrote: post #53
Animats wrote: post #6

Earlier quoted context omitted.

The key thing with bounds checks is to hoist them out of inner loops. If you don't have that optimization, people will turn them off because of the performance impact. Except in inner loops, the performance penalty isn't usually that bad.

Or prove the impossibility of bounds-check failing and then disable them. The perfect use-case for silver-level SPARK. It would make sense to require some proof effort when you want to disable runtime checks...

Agree!
Post reply on HN