Hacker News Reader

This is a teaser / preview and not necessarily what is going to come. But Rust could evolve to providing checks like this:

https://i.imgur.com/oqtEDoV.png

From miri, page 27 in their slide deck. The miri project has changed a lot since the slides were written — and it is now close to being merged into rustc.

miri: https://github.com/solson/miri

The usual problem in C is ambiguity over "how big is it", the cause of most buffer overflows. Rust tries to contain that, but doesn't solve the problem at the language level. Part of the trouble is that there's no way to talk about uninitialized memory in Rust. If you implement something like a growable array (rust calls this a "Vector", a poorly chosen name), it has space in use and space that's uninitialized and unused. There's no way to express that concept within the language. If you had a way in Rust to say that only elements 0..N are initialized, and only they can be accessed, you could express that situation. Initializing another slot means more elements are now initialized. This is run-time checkable with some overhead.

Once you can say that, you can prove it. The proof techniques are well known. The first step is to be able to talk about it within the language. A predicate like

    initialized(A,i,j)

meaning that array A is initialized from elements i to j inclusive is all that's needed. Then, when you write

    assert(initialized(A,i,j));
    A[j+1] = 0;
    assert(initialized(A,i,j+1);

you've expressed how much of the array is now initialized. Then automatic theorem proving takes over and proves that if the first assert is true, so is the second.

This eliminates the need for "unsafe" in many places. A fancier type system is not needed.

It only takes one wrong piece of unsafe code to enable a buffer overflow attack.

> (rust calls this a "Vector", a poorly chosen name),

What exactly makes it "poorly chosen"?

I think it’s based on the C++ name? (a name which Stepanov supposedly now regrets, https://stackoverflow.com/questions/581426/why-is-a-c-vector...)

But it disagrees with all past use of the name “vector” in mathematics and numerical computing, which is reasonably consistent and well defined and dates from the mid-19th century.

I think it agrees pretty well with the mathematical definition, it's just a slight generalization.

A Rust (C++, etc) Vec<T> of length n where T implements addition and multiplication in a way that satisfies field laws is the "reasonable" representation of a n length "mathematical" vector over the field T. It just generalizes that storage type to situations where T is not a field.

It doesn't support addition of two vectors and multiplication by a element of T using the normal mathematical syntax, but that's a fairly reasonable choice given how we regularly use vectors as a sequence of independent numbers and the different priorities for math syntax and programming language syntax.

Just to clarify, a vector space is defined over a field but vectors themselves do not form a field.

Also more importantly in mathematics vectors aren’t really growable. When you change the number of elements you change the dimension (and thus the “type” for that vector). It is then ill-defined to add two vectors of different dimensions.

What makes a C++/Rust/etc vector distinct from an array is that it's resizable. That is its defining property.

On the other hand, a mathematical vector is not a resizable thing: a vector in R² is of a fundamentally different type from a vector in R³.

A type named "vector" should be more like Vec<T, n> for some type T and some integer n. Failing that, the reasonable representation of an n-length mathematical vector, in C++/whatever, is an array.

The whole idea of mutation is not common in mathematics, so of course mathematical vectors don't commonly resize.

The idea of appending an element to make a new vector is however extremely common, particularly in induction like proofs.

Vec<T, n> is in a sense already what we have, it's just that we are not capable of storing the n in the type information^0 so we store it at runtime.

^0 For a number of reasons. n can change with mutation while types can't. We don't necessarily know n ahead of time when building a vector (which happens in math too) but we have to know types at compile time. And we just don't have a great way of storing numbers in types in Rust anyways.

This is quite standard in the functional programming world; Common LISP, Scala, and Haskell all use "vector" to refer to (usually growable) contiguous-memory arrays with efficient random access, as opposed to "lists" with efficient append and prepend but inefficient random access.

I might be nitpicking but in Haskell and typical lisps “lists” don’t have efficient append. They are basically singly linked lists. A structure with efficient append and prepend (sometimes called a deque) is implemented as a finger tree in Haskell (with logarithmic random access), and as a vector of arrays in C++ (constant random access).

Good point. Sometimes efficient append, but usually just efficient prepend ^_^

> The usual problem in C is ambiguity over "how big is it", the cause of most buffer overflows

Buffer overflows in C are caused by accessing uninitialized memory, regardless of why the program does it (how big is it vs null pointer derefs vs various other ways).

Rust does solve that problem at the language level. There's no such thing as an uninitialized pointer, which is the only right solution I'd argue. If you do access out-of-bounds in a safe block, you panic, not cause a vulnerability. How is the problem not solved by this, combined with iterators?

What you're talking about, tracking uninitialized/initialized at runtime, can totally be done in rust too, e.g. with a [Option<T>] or such... but then you'll obviously pay the runtime price of doing such checking.

The more common case though is someone wishes to have a mutable vector which has a capacity and an accessible subset of data, which Vec implements.

What you're claiming can be proven easily is not so trivial to prove for the common case; it may be `j+n` where `n` may derive from user input.

It would be cool if blocks of rust now could be "theorem-proved-unsafe", but I think realistically it's a huge amount of work for a small win.

Writing and proving theorems about code is typically much more time-consuming than exhaustively testing or informally verifying a block of code via review, and when the unsafe code is small and simple enough, the results we get are already "good enough".

> It only takes one wrong piece of unsafe code to enable a buffer overflow attack.

Yup, though for many programs you can entirely avoid unsafe code (outside of the well-reviewed and well-tested stdlib), and you can pay special attention to unsafe code in review and testing.

That's a damn sight better than other low level non-gc'd languages like C++/C where the default is unsafe and all code is suspect.

Ah, no, buffer overflows are caused by failure to check bounds. Practically, this is usually only a serious problem when the buffer overflows into an area that has been initialized with something like a return address.

> Part of the trouble is that there's no way to talk about uninitialized memory in Rust.

You mentioned Vec right after that. Which is interesting, because Vec deals with uninitialized memory just fine. https://doc.rust-lang.org/std/vec/struct.Vec.html#method.res... allocates more space, but doesn't allow you to read it unless you explicitly add elements.

> It only takes one wrong piece of unsafe code to enable a buffer overflow attack.

Isn't that the case for every language? Here, you can limit the unsafe bit to the underlying datastructure if any unsafe actions are required. Maybe Vec uses some unsafe bits, maybe not - but the usage of it is all safe code.

In many other languages `unsafe` taints the block of code it is in, which propagates upwards. Rust is the other way around, where `unsafe` means "I'm doing something unsafe here, but let's not tell anyone who doesn't look". It can be a lot harder in Rust (than other languages I've used) to know whose code you have to trust: language implementors (probably ok) or random crates (urk).

Could you give some examples of these other languages? My only exposure to a similar feature is D's @safe/@trusted, where if you're writing @safe code, you'll always wrap unsafe code with @trusted stopping any propagation.

C#

C# has both unsafe blocks and unsafe methods. The behaviour is the same as in Rust. (Unsafe function can be called only from unsafe scope and safe functions can contain unsafe blocks)

I don't think you are correct, unless the language has changed substantially.

https://docs.microsoft.com/en-us/dotnet/csharp/language-refe...

Among other things, you need to opt in to unsafe with the `/unsafe` compiler flag. I'm pretty much 100% certain that the `unsafe` keyword applied to scopes does not mean "treat the contained scope as if it were safe, but permit the use of unsafe operators" which is how it works in Rust.

Edit: to put some more words here, I think what you may be saying is "the unsafe fragment of C# behaves like Rust", which sounds sane to me: `unsafe` decorates regions and the compiler will complain at you if you use unsafe things outside such scopes. When I said "C#" I meant the larger language in which programs are either "safe" (verifiable) or not, and for which `unsafe { .. }` forces you into the unsafe fragment.

Rust doesn't have safe and unsafe language fragments; there is one language which follows rules similar to (as you say) unsafe C#, but which advertises itself as safe. In that language, `unsafe` moves you back in to "safe" code (or we could agree that it was never safe in the same sense that languages like C# are).

You're wrong, and that's exactly what "unsafe" block does in C# - it does not affect the outer blocks. So, for example, if you wrap your pointer arithmetic inside "unsafe", you don't need the "unsafe" modifier on the method. If you put the modifier on the method, then you don't need the modifier on the class. And the code that uses your "unsafe" classes and methods doesn't need to be in "unsafe" context.

If it were otherwise, no C# program would compile without "unsafe", because large parts of the standard library core (stuff in System) is unsafe. The only reason why "unsafe" is useful is precisely because it lets you isolate unsafe operations in a way that lets safe code invoke into them (assuming that you uphold your safety guarantees).

The /unsafe switch is a different thing - it needs to be turned out for the C# compiler to allow "unsafe" anywhere in its input, and is basically a project-level declaration that "this has some unsafe code somewhere in it".

Sure it does, Assemblies with unsafe code are tainted and fail verification.

There are deployment scenarios, like IIS, where admins can disable the execution/loading of Assemblies with unsafe code.

"unsafe" is a C# feature. Verification is a CLR feature. And they are only related in a sense that things that you can do inside "unsafe" blogs generally produce unverifiable assemblies. But the reverse is not true, you don't have to use an "unsafe" block to consume an unverifiable assembly.

Nor does "unsafe" breaks verification by itself - it's only the specific features that you might use inside (like pointer arithmetic) that would do so, and even then not all of them. For example, C# requires "unsafe" for any use of sizeof() that is not known at compile-time, and for which it needs to emit the sizeof IL opcode. So e.g. sizeof(int) is okay, but sizeof(IntPtr) is unsafe; also, sizeof all structs are considered unsafe. However, the IL opcode for sizeof is not unverifiable, and so such an assembly would pass verification, despite requiring "unsafe" in C#.

I know that, but unless one wants to become a MSIL and verification engine expert, the simplest explanation is that unsafe taints Assemblies.

Yes, but that's not what OP was talking about. Within an assembly, an unsafe block still doesn't taint any code that calls into it. And between assemblies, an unsafe assembly doesn't taint a safe one that depends on it. So it doesn't "propagate outwards".

I work on proving things about unsafe Rust for my day job, and you really don't know what you're talking about if you think what you're proposing would be remotely sufficient to guarantee safety in a modern systems language. I'm not saying a way to deal with uninitialized data would not help, but that is not the primary source of potential unsafety in Rust, and it's completely infeasible for the language to include all the features that would be required to prove all unsafe Rust code safe (at least, given what we know now--if you have ideas about weak memory that I'm not aware of, feel free to ping me!). However, it is possible to do machine-checked proofs about unsafe Rust, and once those proofs are done, they remain valid forever, so I'd prefer the current approach (which is to verify the standard library and some major third party ones, and make the tooling for proving correctness of other Rust libraries as easy as possible).

Of course it's not sufficient. It does make possible to talk about partially initialized arrays, which is a necessary step to checking their access, either at run time or by formal methods.

The "Weak" problem is mostly a back-pointer problem. If you had some way to talk about a back pointer locked in an invariant relationship with a forward pointer, that would deal with back pointers for trees and such. I sketched out a solution for this on YC earlier this year.[1] This doesn't deal with true circular lists, but those are relatively rare; people tend to use arrays for that today.

It's good to hear this criticized from someone who does program proving. I used to do that, a long time ago. What I usually get from the Rust crowd is macho assertion that they don't need checking of their unsafe code. History and the CERT archives indicate they do.

[1] https://news.ycombinator.com/item?id=14302823

Weak memory isn't related to weak pointers. What you're referring to is actually pretty easy to deal with (well, not easy, it's pretty tedious to prove in most of the individual cases, but it's not conceptually difficult). Weak memory refers to atomic operations with weak consistency (like relaxed, release-acquire, and perhaps most confoundingly consume). Modeling them along with lifetimes and ownership tracking requires a fairly sophisticated language model with lots of intermediate tokens and ghost state, which would be a tremendous burden to include in a programming language. Fortunately, it looks like most features of safe Rust extend straightforwardly to weak memory models, but that isn't always the case for unsafe Rust.

I think it's wrong to say that unsafe blocks "contain" the unsafety. Unsafety can't really be contained once it's there -- that's what makes it unsafe.

The advantage is that you should be able to write application code without unsafe blocks; they should be in a library. And the library has a contract: if unsafe behavior does leak outside the library, it is clearly the fault of the library, and can't be blamed on the (safe) caller.

Unsafe blocks "contain the possible sources of unsafety" may be a more correct way to phrase it.

It is better to know that only a specific subset of the codebase could be responsible for memory unsafety even if that behavior may leak. If nothing else, it helps focus reviewing and testing effort.

I'm pretty sure y'all are saying the same thing. :-) my favorite way of describing it is "Rust lets you build safe abstractions, even if its core uses unsafe."

Terrific, in-depth, answer...and I appreciate it.

A really nice answer. It's too bad, I suppose, that the same abstraction can't be used "all the way down". I suppose then we'd be stuck with some high-level encoding of the chip's ISA, perhaps generalized to allow the programmer the ability to define new instructions, and an increased number of registers, etc.