4 ms·

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 un

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 (because profilers and proofs can be wrong too :) edit: grammar.

EE84M3i 6y ago
Why does code violating the rules have to stay unsafe? Haven't the rules been improved before? Why won't they be improved again?
foota 6y ago
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.
- zozbot234 6y ago
  This requires a formal semantics for Unsafe Rust. It's a hard problem, albeit one that's being worked on.
  - foota 6y ago
    I'm aware that however it's done it'll be hard. Does it really require formal semantics for unsafe rust though? I'm not familiar enough with rust to give an example, but if you imagine there's the unsafe rust level and beneath that the "machine code" (not actually machine code, just at the abstraction level equivalent to it) you should be able to hand write what the rust code is doing, without requiring the compiler to construct the machine level operations. With a formal semantics the proof checker just checks that the written proof (at rust level) matches with the rust code, but requires as you said an understanding of how unsafe rust interacts with the proof, whereas with a proof written at machine level, you don't need to understand the rust semantics, you just need to translate the rust to machine level and then check the proof there. Perhaps the machine level could be some layer in llvm? I'm only a little familiar with compilers, and hardly at all with more complicated compiler theory, but this seems reasonable to me.
    - kd5bjo 6y ago
      > With a proof written at machine level, you don't need to understand the rust semantics, you just need to translate the rust to machine level and then check the proof there. This approach would only be able to verify a particular compilation result as safe. If you want to verify that it will always be safe, you need to be comparing against the behavior of future compilers, which requires some kind of contract about their behavior. “Formal semantics” is the technical term for that contract.
    - bennofs 6y ago
      The problem is that the unsafe-safe boundary needs to be specified. Unsafe code often relies on invariants ensured due to safe rust's checks. Also, there are properties that unsafe code has to satisfy which are special to rust, for example involving rules around special traits like `Drop`. So even if the unsafe code itself could be proven to have no memory corruptions, if it does not satisfy these invariants, it could lead to wrong behaviour in other parts of the program.
  - doonesbury 6y ago
    Any references?
- doonesbury 6y ago
  Amen to that. Integrated formal systems giving the spec working with the programming language on the implementation side is the holy grail.
Jweb_Guru 6y ago
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.
- steveklabnik 6y ago
  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!
  - Jweb_Guru 6y ago
    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.
    - steveklabnik 6y ago
      How, when they rely on semantics that are not fully locked down? Are you referring to something other than the Rust Belt work?
      - Jweb_Guru 6y ago
        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.
        steveklabnik 6y ago

EE84M3i 6y ago

Why does code violating the rules have to stay unsafe? Haven't the rules been improved before? Why won't they be improved again?

foota 6y ago

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.

zozbot234 6y ago
This requires a formal semantics for Unsafe Rust. It's a hard problem, albeit one that's being worked on.
- foota 6y ago
  I'm aware that however it's done it'll be hard. Does it really require formal semantics for unsafe rust though? I'm not familiar enough with rust to give an example, but if you imagine there's the unsafe rust level and beneath that the "machine code" (not actually machine code, just at the abstraction level equivalent to it) you should be able to hand write what the rust code is doing, without requiring the compiler to construct the machine level operations. With a formal semantics the proof checker just checks that the written proof (at rust level) matches with the rust code, but requires as you said an understanding of how unsafe rust interacts with the proof, whereas with a proof written at machine level, you don't need to understand the rust semantics, you just need to translate the rust to machine level and then check the proof there. Perhaps the machine level could be some layer in llvm? I'm only a little familiar with compilers, and hardly at all with more complicated compiler theory, but this seems reasonable to me.
  - kd5bjo 6y ago
    > With a proof written at machine level, you don't need to understand the rust semantics, you just need to translate the rust to machine level and then check the proof there. This approach would only be able to verify a particular compilation result as safe. If you want to verify that it will always be safe, you need to be comparing against the behavior of future compilers, which requires some kind of contract about their behavior. “Formal semantics” is the technical term for that contract.
  - bennofs 6y ago
    The problem is that the unsafe-safe boundary needs to be specified. Unsafe code often relies on invariants ensured due to safe rust's checks. Also, there are properties that unsafe code has to satisfy which are special to rust, for example involving rules around special traits like `Drop`. So even if the unsafe code itself could be proven to have no memory corruptions, if it does not satisfy these invariants, it could lead to wrong behaviour in other parts of the program.
- doonesbury 6y ago
  Any references?
doonesbury 6y ago
Amen to that. Integrated formal systems giving the spec working with the programming language on the implementation side is the holy grail.

Jweb_Guru 6y ago

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.

steveklabnik 6y ago
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!
- Jweb_Guru 6y ago
  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.
  - steveklabnik 6y ago
    How, when they rely on semantics that are not fully locked down? Are you referring to something other than the Rust Belt work?
    - Jweb_Guru 6y ago
      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.
      - steveklabnik 6y ago