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

RustBelt: securing the foundations of the Rust programming language

dl.acm.org

Post reply on HN
Print view View original

51–60 of 109 posts

Re: RustBelt: securing the foundations of the Rust programming language

#51

Post by weberc2 »

rntz wrote: post #29
dmix wrote: post #22

Earlier quoted context omitted.

One thing about formal verification, and a lesser extent automated testing, is that you often end up spending the majority of the time adapting the program or language to work with verification rather than actually solving a real-world problem or fixing a real bug. His third comment fits this category well. The problem set he describes was that the code is designed in a way that's ill suited for formal verification.…

We regard "this program is hard to test" as a problem that's worth refactoring to fix; why shouldn't we regard "this program is hard to verify" the same way?

This is a good question. I'm inclined to say that the value proposition for testing is better than for verification. First of all, if your unit is hard to test, it is likely to cause other issues, but probably more importantly, testing finds a lot more bugs per unit effort than formal verification. That last point is based exclusively on my intuition and it could well be wrong--it would be good to hear from people with more experience with both testing and formal verification.

Also, now that I think about it, the value proposition isn't fixed for all applications. Testing is the better value proposition if you need to catch the easiest 95% of your bugs (arbitrary number for example purposes), but if you need to catch 99.999% of your bugs, the testing effort may likely be much greater than the formal verification effort. That said, open source projects like Rust get tons of testing for free by virtue of being very, very popular, so I'm not sure how to weigh one against the other.

Re: RustBelt: securing the foundations of the Rust programming language

#52

Post by [deleted] »

carapace wrote: post #50

> Rust is a new systems programming language that promises to overcome the seemingly fundamental tradeoff between high-level safety guarantees and low-level control over resource management. Unfortunately, none of Rust’s safety claims have been formally proven, and there is good reason to question whether they actually hold. Aw, c'mon!? Rust is Sudoku for super-smarties. - - - - I'm going to "double-down" on that: Ru…

[deleted]

Re: RustBelt: securing the foundations of the Rust programming language

#53

Post by gpm »

nukeop wrote: post #41
pcwalton wrote: post #33

Earlier quoted context omitted.

> The most ironic part is that so many restrictions and problems are likely to provoke people to rely on whatever option happens to work, which might not be the best/safest one. Programs written in Rust are empirically safer than programs written in C or C++. > The higher the freedom, the better the results delivered by a sensible/knowledgeable person. If that were true, then C and C++ code would be safer and more se…

I don't see too many job offers for Rust developers, I see plenty for C and C++ though.

With the exception of swift - which has the distinct advantage of being one of two languages you can write programs in for the most popular (? probably true since Android's market share is scattered across many models) piece of consumer hardware in the world - I can't think of a language of similar age to or younger than rust with as many job ads.

You see plenty for C/C++ because they've existed forever, have a huge amount of code written in them, and a huge number of programmers who already know them. Just like with Cobal you will almost certainly see plenty for C/C++ many years into the future. That doesn't really say much about Rust.

Re: RustBelt: securing the foundations of the Rust programming language

#54

Post by gpm »

haberman wrote: post #49
pcwalton wrote: post #30

Earlier quoted context omitted.

You can't prove safety properties of something that isn't safe. LLVM IR sure isn't.

This raises an interesting question of whether Rust would make sense as a code generation target for other languages or runtimes. It is conceivable that you could compile and run untrusted Rust (with no unsafe blocks and restricted imports) the same way web browsers run untrusted JavaScript? It could be the only GC-less IR that you can run with a reasonable defense against memory corruption. Looks like people have ha…

Raising logic bugs from "this is maybe occasionally an annoyance, or cool piece of trivia" to "this is a security issue" seems like a bad idea in something as complex as Rust's compiler.

Especially when there are many currently known bugs of this sort:

https://github.com/rust-lang/rust/issues?q=is%3Aopen+is%3Ais...

Re: RustBelt: securing the foundations of the Rust programming language

#55

Post by quotheth »

carapace wrote: post #50

> Rust is a new systems programming language that promises to overcome the seemingly fundamental tradeoff between high-level safety guarantees and low-level control over resource management. Unfortunately, none of Rust’s safety claims have been formally proven, and there is good reason to question whether they actually hold. Aw, c'mon!? Rust is Sudoku for super-smarties. - - - - I'm going to "double-down" on that: Ru…

I work for a company with a massive rust codebase. Rust is very much about building production code.

What is 'good production code' ?

* Few errors * Readable, well documented * Testable, has tests, has testing tools like quickcheck, fuzzing, etc * Meets performance constraints

Rust hits those better than any language I've used. The downside is, oh gosh, you'll have to actually learn a programming language that isn't just another variation of the ones you learned in school.

Re: RustBelt: securing the foundations of the Rust programming language

#56

Post by emn13 »

phkahler wrote: post #32
rntz wrote: post #29

Earlier quoted context omitted.

We regard "this program is hard to test" as a problem that's worth refactoring to fix; why shouldn't we regard "this program is hard to verify" the same way?

But "this language is hard to verify" should not trump the usability of the language. The verification only needs to be done once, while the language will be used to write code again and again. If it doesn't negatively affect the language users then sure, change it to make verification easier.

You're not verifying a language, you're verifying a program (or some part of one). Sure- that part in this instance may be implementing a language standard library, but who cares? That program also has tests, docs, types and all the other things people use to convince themselves of correctness.

It really is like unit testing. There too you could make the argument that in some cases untestable code might be worth it if the alternative is an api that's hard to use. And there too an api may well be used many orders of magnitudes more frequently than it is changed. I think you have to decide that on a case by case basis (at least, I can't think of any convincing general argument there).

Re: RustBelt: securing the foundations of the Rust programming language

#57

Post by zzzcpan »

haberman wrote: post #49
pcwalton wrote: post #30

Earlier quoted context omitted.

You can't prove safety properties of something that isn't safe. LLVM IR sure isn't.

This raises an interesting question of whether Rust would make sense as a code generation target for other languages or runtimes. It is conceivable that you could compile and run untrusted Rust (with no unsafe blocks and restricted imports) the same way web browsers run untrusted JavaScript? It could be the only GC-less IR that you can run with a reasonable defense against memory corruption. Looks like people have ha…

I'm not sure I understand your idea, how can code generation benefit from memory safe abstractions of target languages? The whole point of code generation or rather compilation is to fit one representation into something else, doesn't matter what it is, but it has to satisfy its constraints no matter what, even if you have to use a giant global array to emulate pointers via indexes. In other words, the goal is to work around any constraints of the target language to fit yours, but not to design your language to fit any constraints of the target.

Safety guarantees can only work if you carefully choose and rely on appropriate abstractions for your problem.

Re: RustBelt: securing the foundations of the Rust programming language

#58

Post by fmap »

matt_d wrote: post #11
fovc wrote: post #2

Adrian Colyer did a good write up of this paper recently on The Morning Paper : https://blog.acolyer.org/2018/01/18/rustbelt-securing-the-fo...

Two recent talks about the project: - Derek Dreyer, Workshop on Software Correctness and Reliability 2017 (48 min): https://www.youtube.com/watch?v=Y9vemQmVeLI - Ralf Jung, POPL 2018 (25 min): https://plv.mpi-sws.org/rustbelt/popl18/

Derek also gave a terrific keynote talk at POPL 2018 about the big picture: https://www.youtube.com/watch?v=8Xyk_dGcAwk

Re: RustBelt: securing the foundations of the Rust programming language

#59

Post by dawg »

steveklabnik wrote: post #47
ZenoArrow wrote: post #40

Earlier quoted context omitted.

> "There are effectively two Ds" Could you not also say there are effectively two Rusts? https://doc.rust-lang.org/book/second-edition/ch19-01-unsafe... "Rust has a second language hiding out inside of it, unsafe Rust, which does not enforce these memory safety guarantees. Unsafe Rust works just like regular Rust does, but it gives you extra superpowers not available in safe Rust code." By the way, I don't say this a…

You can, but there is a big difference: betterC is a subset of D, whereas unsafe Rust is a superset of safe Rust. That is, when you use unsafe, you don't lose any language features. When you drop into betterC, you do lose a bunch of stuff from D.

You don't have to restrict yourself to betterC to use manual memory management. BetterC is mainly targetted at embedded programming and to port components of existing C applications. Malloc vs. GC vs. stdx-allocator is a separate topic, though betterC doesn't link with the GC by default.

Re: RustBelt: securing the foundations of the Rust programming language

#60

Post by khuey »

tom_mellior wrote: post #46
dmix wrote: post #22

Earlier quoted context omitted.

One thing about formal verification, and a lesser extent automated testing, is that you often end up spending the majority of the time adapting the program or language to work with verification rather than actually solving a real-world problem or fixing a real bug. His third comment fits this category well. The problem set he describes was that the code is designed in a way that's ill suited for formal verification.…

> But he never mentions any other benefits or justification for changing how it works. I read "it lets me write a program that has a data race", accompanied by a program that has a data race, as saying that the bug is that a language feature meant to provide mutual exclusion does not provide mutual exclusion. In a language one of whose main selling points is "you always get mutual exclusion". How is this not a bug? T…

It's absolutely a legitimate bug.
Post reply on HN