4 ms·

Homepage seems to focus mostly on temporal memory safety; there isn't much said about spatial memory safety or memory-safe-but-unsound primitives, like type con

Homepage seems to focus mostly on temporal memory safety; there isn't much said about spatial memory safety or memory-safe-but-unsound primitives, like type confusion. These should be table stakes when talking about "safe" languages (or subsets thereof); I hope these authors have or propose plans for these classes as well! (I agree with the more general critique here, that any adaptation invasive enough to provide these properties in C might as well be its own programming language.)

adamrezich 3y ago
There is no universally-accepted definition for the term "safe" as it applies to programming languages.
- gpderetta 3y ago
  While we can of course always bikeshed the minutiae, memory safety is a fairly well accepted and well defined term. And so are temporal and spatial safety (as subsets of memory safety). I would add that temporal safety is significantly harder than spatial safety (spatial safety is only hard in C if you do not want to break the ABI), so it is nice that this project is focusing on it.
- tialaramex 3y ago
  True and yet useless. When "that's not safe" turns into a "discussion" about what safety means (e.g. at basically every C++ conference for over a year) what that signals is that you're much more interested in preserving the status quo than improving safety.
  - adamrezich 3y ago
    Alternatively, it signals that "safety" as a broad concept as it applies to programming languages, is pretty incoherent and ultimately useless. "Safe" and "safety" are very overloaded English words that come with a lot of baggage, and perhaps it would be prudent to stop using these broad, nonspecific terms for things like programming languages. "Memory safety" is a coherent, reasonably well-defined concept, and it's fine to talk about something like that. But what does a broadly, generically "safe" programming language even mean?
    - tialaramex 3y ago
      Oh! That's easy, although a little uncomfortable for some people. A program is safe if it remains well-behaved regardless of inputs. A safe language necessarily constructs such programs. It turns out Memory Safety is a necessary part of this. The reason this is awkward is that it turns out that languages such as Go do not meet this requirement because they exhibit UB under some data races. There are three ways out of this, which are interesting to contemplate 1. No concurrency. Languages which simply don't have concurrency are fine in this respect, e.g. Python, as are (so long as you don't try to have concurrency) older versions of C and even C++ which simply decline to explain how concurrency is even possible - if you're using say POSIX threads from C89 that's a problem because in C89 concurrency doesn't exist so none of your programs have any meaning whatsoever even if they don't race... 2. Rust's trick, mutation XOR multiple references - you can't write a data race in (safe) Rust, so even though the language has concurrency it's fine, you can't trip yourself this way. 3. Java and OCaml's trick, survive despite loss of Sequential Consistency. The proof we have is SC/DRF - using this construction a program is Sequentially Consistent if it is Data Race Free, but if we can survive loss of Sequential Consistency then this proof isn't important. This is enormously difficult, like it's easily the sort of work that could earn you a PhD if you don't have one already. We also still don't know whether it's potentially worth it. For Java the answer was "No" but for OCaml it's too early to say. Edited to add: Marked that just not having concurrency only avoids data races, it doesn't magically fix all the other problems C and C++ have for example.
- Drup 3y ago
  Actually, there is a rather pervasive notion of "soundness" in programming language theory. It has many flavors (because, as you hint, programming languages are quite varied). One of the most simple way of stating it, often dubbed "progress and preservation" is: a well typed program can execute (i.e., it doesn't crash) and returns a value of the same type. This obviously covers type safety, but also spatial memory safety, and can be extended to temporal memory safety, and even some concurrency aspects. This has been proven for fairly large subsets of programming languages and even some full languages (like SML). Unfortunately, it doesn't hold for most mainstream ones, because programming language theory is often ... under-used ... among language designers.
- woodruffw 3y ago
  This can simultaneously be true and for spatial memory safety to be a necessary condition of any coherent definition of “safe.”
betz47 3y ago
We chose to start with temporal safety (use-after-free, uninitialised memroy etc) but are going to implement spacial safety (buffer overflows/underflows) soon (See roadmap https://xr0.dev/vision-roadmap https://xr0.dev/vision-roadmap). Xr0 is not limited to memory-safety, its goal is to eliminate the possibility of writing C code that results in undefined behaviour. A good analogy can be drawn to how Typescript wraps Javascript and provides type safety. Think of Xr0 as a wrapper to C that guarantees you don't violate C's safety semantics.
- scns 3y ago
  > A good analogy can be drawn to how Typescript wraps Javascript and provides type safety. Like this idea a lot. Does that mean it could be used to convert C projects in a strangler pattern style?
- woodruffw 3y ago
  C doesn’t particularly strong safety guarantees of its own around type punning, which is logic bugs that aren’t themselves memory corruption so frequently result in exploitable vulnerabilities in C (and C++) codebases. How do you plan to handle things like that? (Other proposals that I’m aware of seek to forbid those parts of the language outright, or add some kind of runtime instrumentation like isoheaps. Neither of these is particularly palatable for pre-existing codebases with deep, undocumented language feature and ABI assumptions!)

adamrezich 3y ago

There is no universally-accepted definition for the term "safe" as it applies to programming languages.

gpderetta 3y ago
While we can of course always bikeshed the minutiae, memory safety is a fairly well accepted and well defined term. And so are temporal and spatial safety (as subsets of memory safety). I would add that temporal safety is significantly harder than spatial safety (spatial safety is only hard in C if you do not want to break the ABI), so it is nice that this project is focusing on it.
tialaramex 3y ago
True and yet useless. When "that's not safe" turns into a "discussion" about what safety means (e.g. at basically every C++ conference for over a year) what that signals is that you're much more interested in preserving the status quo than improving safety.
- adamrezich 3y ago
  Alternatively, it signals that "safety" as a broad concept as it applies to programming languages, is pretty incoherent and ultimately useless. "Safe" and "safety" are very overloaded English words that come with a lot of baggage, and perhaps it would be prudent to stop using these broad, nonspecific terms for things like programming languages. "Memory safety" is a coherent, reasonably well-defined concept, and it's fine to talk about something like that. But what does a broadly, generically "safe" programming language even mean?
  - tialaramex 3y ago
    Oh! That's easy, although a little uncomfortable for some people. A program is safe if it remains well-behaved regardless of inputs. A safe language necessarily constructs such programs. It turns out Memory Safety is a necessary part of this. The reason this is awkward is that it turns out that languages such as Go do not meet this requirement because they exhibit UB under some data races. There are three ways out of this, which are interesting to contemplate 1. No concurrency. Languages which simply don't have concurrency are fine in this respect, e.g. Python, as are (so long as you don't try to have concurrency) older versions of C and even C++ which simply decline to explain how concurrency is even possible - if you're using say POSIX threads from C89 that's a problem because in C89 concurrency doesn't exist so none of your programs have any meaning whatsoever even if they don't race... 2. Rust's trick, mutation XOR multiple references - you can't write a data race in (safe) Rust, so even though the language has concurrency it's fine, you can't trip yourself this way. 3. Java and OCaml's trick, survive despite loss of Sequential Consistency. The proof we have is SC/DRF - using this construction a program is Sequentially Consistent if it is Data Race Free, but if we can survive loss of Sequential Consistency then this proof isn't important. This is enormously difficult, like it's easily the sort of work that could earn you a PhD if you don't have one already. We also still don't know whether it's potentially worth it. For Java the answer was "No" but for OCaml it's too early to say. Edited to add: Marked that just not having concurrency only avoids data races, it doesn't magically fix all the other problems C and C++ have for example.
Drup 3y ago
Actually, there is a rather pervasive notion of "soundness" in programming language theory. It has many flavors (because, as you hint, programming languages are quite varied). One of the most simple way of stating it, often dubbed "progress and preservation" is: a well typed program can execute (i.e., it doesn't crash) and returns a value of the same type. This obviously covers type safety, but also spatial memory safety, and can be extended to temporal memory safety, and even some concurrency aspects. This has been proven for fairly large subsets of programming languages and even some full languages (like SML). Unfortunately, it doesn't hold for most mainstream ones, because programming language theory is often ... under-used ... among language designers.
woodruffw 3y ago
This can simultaneously be true and for spatial memory safety to be a necessary condition of any coherent definition of “safe.”

betz47 3y ago

We chose to start with temporal safety (use-after-free, uninitialised memroy etc) but are going to implement spacial safety (buffer overflows/underflows) soon (See roadmap https://xr0.dev/vision-roadmap https://xr0.dev/vision-roadmap). Xr0 is not limited to memory-safety, its goal is to eliminate the possibility of writing C code that results in undefined behaviour. A good analogy can be drawn to how Typescript wraps Javascript and provides type safety. Think of Xr0 as a wrapper to C that guarantees you don't violate C's safety semantics.

scns 3y ago
> A good analogy can be drawn to how Typescript wraps Javascript and provides type safety. Like this idea a lot. Does that mean it could be used to convert C projects in a strangler pattern style?
woodruffw 3y ago
C doesn’t particularly strong safety guarantees of its own around type punning, which is logic bugs that aren’t themselves memory corruption so frequently result in exploitable vulnerabilities in C (and C++) codebases. How do you plan to handle things like that? (Other proposals that I’m aware of seek to forbid those parts of the language outright, or add some kind of runtime instrumentation like isoheaps. Neither of these is particularly palatable for pre-existing codebases with deep, undocumented language feature and ABI assumptions!)