4 ms·

Maybe I'm missing something, but I could write an interface labelled sage on top of any unsafe code I want. Why doesn't it matter that my unsafe implementation

Maybe I'm missing something, but I could write an interface labelled sage on top of any unsafe code I want. Why doesn't it matter that my unsafe implementation is proven correct?

kibwen 9y ago
This is going to sound tautological, but the unsafe keyword is for operations that the compiler can't prove. The unsafe keyword only unlocks a very small number of possible new operations (it doesn't turn off any existing checks), and those operations make unsafe Rust as freeform as C; if you could prove unsafe Rust correct then you could just prove C code correct.
- nickpsecurity 9y ago
  Which Frama-C, Simpl/C, and Astree Analyzer all do. Then that C code is quite trustworthy. Rust has stuff like Simpl in the works but needs something like Frama-C or SPARK for unsafe.
  - kibwen 9y ago
    Can you give me an example of something that safe Rust doesn't allow, thereby requiring the unsafe keyword to implement, but that also contains an error that passes the Rust compiler silently but that Frama-C or SPARK would statically detect?
    - nickpsecurity 9y ago
      That's a trick question: you know I don't know know Rust enough to answer it. :P However, I fo know the things I mentioned can prove safety properties about unsafe code. Rust compiler can't per these threads. So, If A then B...?
      - kibwen 9y ago
        But whether SPARK et al can prove properties about unsafe code isn't the pertinent topic. SPARK and friends are subsets if their respective languages, implying that there are features of those languages that, if their use is not restricted, inhibit the production of correctness proofs. Rust already has such a thing, by default, in the form of non-unsafe Rust, and the notion of "unsafe" in the context of Rust and Frama-C is not guaranteed to be the same. So what I'm asking is for you to demonstrate something that these other languages can prove that safe Rust can't. By the way, you've been in Rust threads enough years now championing safe languages that you really no longer have any excuse for not learning Rust. :P
        nickpsecurity 9y ago
        "But whether SPARK et al can prove properties about unsafe code isn't the pertinent topic. " I thought that these worries about unsafe code in Rust indicated people wanted a way to ensure it's as safd as possible. Traditionally, unsafety the language itself cant handle is dealt with via external tools for analysis, proving, and testing. These exist for unsafe code in Ada, C, C+×, Java, and SPARK. Tool-assisted, subsets of each are deployed in safety-critical industries. Anyone doing unsafe codd in them will get more robustness than unsafe code in Rust. So, you already have protection measures in safe Rust. Other tools, esp SPARK Ada and C enhancements, have them for unsafe code that Rust does nothing to protect. That's a gap in capabilities Rust needs to close. Until then, it's on the table when choosing which to use for unsafe code. Note that Im also a big fan of mixing and matching where we used the C or SPARK provers on unsafe Rust coded to be semantically equivalent. I just know most will prefer Rust to handle this itself. "By the way, you've been in Rust threads enough years now championing safe languages that you really no longer have any excuse for not learning Rust. :P" Haha. I do plan to learn it for my Brute Force Assurance concept. Remember I have a brain injury, though, that knocked out memory and good chunk of learning pace on top of full-time job. That plus a shit-ton of broad R&D leaves little time for coding.
  - solidsnack9000 9y ago
    It wouldn't surprise me if even Frama-C and SPARK have a "trust me" annotation.
    - nickpsecurity 9y ago
      Pretty much all languages w/ formal specifications do. The reason is that some specification claims are assumed/reasonable, proven outside the tool, or too hard to handle immediately. This can also be used as a maybe later. I'm not sure what theirs are.
dbaupp 9y ago
It would be great if it was, but it's also infeasible for a lot of code (at the moment anyway): it takes too much time and effort, and, in the FFI case, requires proving a whole external library correct too.

Maybe I'm missing something, but I could write an interface labelled sage on top of any unsafe code I want. Why doesn't it matter that my unsafe implementation is proven correct?

kibwen 9y ago

This is going to sound tautological, but the unsafe keyword is for operations that the compiler can't prove. The unsafe keyword only unlocks a very small number of possible new operations (it doesn't turn off any existing checks), and those operations make unsafe Rust as freeform as C; if you could prove unsafe Rust correct then you could just prove C code correct.

nickpsecurity 9y ago
Which Frama-C, Simpl/C, and Astree Analyzer all do. Then that C code is quite trustworthy. Rust has stuff like Simpl in the works but needs something like Frama-C or SPARK for unsafe.
- kibwen 9y ago
  Can you give me an example of something that safe Rust doesn't allow, thereby requiring the unsafe keyword to implement, but that also contains an error that passes the Rust compiler silently but that Frama-C or SPARK would statically detect?
  - nickpsecurity 9y ago
    That's a trick question: you know I don't know know Rust enough to answer it. :P However, I fo know the things I mentioned can prove safety properties about unsafe code. Rust compiler can't per these threads. So, If A then B...?
    - kibwen 9y ago
      But whether SPARK et al can prove properties about unsafe code isn't the pertinent topic. SPARK and friends are subsets if their respective languages, implying that there are features of those languages that, if their use is not restricted, inhibit the production of correctness proofs. Rust already has such a thing, by default, in the form of non-unsafe Rust, and the notion of "unsafe" in the context of Rust and Frama-C is not guaranteed to be the same. So what I'm asking is for you to demonstrate something that these other languages can prove that safe Rust can't. By the way, you've been in Rust threads enough years now championing safe languages that you really no longer have any excuse for not learning Rust. :P
      - nickpsecurity 9y ago
        "But whether SPARK et al can prove properties about unsafe code isn't the pertinent topic. " I thought that these worries about unsafe code in Rust indicated people wanted a way to ensure it's as safd as possible. Traditionally, unsafety the language itself cant handle is dealt with via external tools for analysis, proving, and testing. These exist for unsafe code in Ada, C, C+×, Java, and SPARK. Tool-assisted, subsets of each are deployed in safety-critical industries. Anyone doing unsafe codd in them will get more robustness than unsafe code in Rust. So, you already have protection measures in safe Rust. Other tools, esp SPARK Ada and C enhancements, have them for unsafe code that Rust does nothing to protect. That's a gap in capabilities Rust needs to close. Until then, it's on the table when choosing which to use for unsafe code. Note that Im also a big fan of mixing and matching where we used the C or SPARK provers on unsafe Rust coded to be semantically equivalent. I just know most will prefer Rust to handle this itself. "By the way, you've been in Rust threads enough years now championing safe languages that you really no longer have any excuse for not learning Rust. :P" Haha. I do plan to learn it for my Brute Force Assurance concept. Remember I have a brain injury, though, that knocked out memory and good chunk of learning pace on top of full-time job. That plus a shit-ton of broad R&D leaves little time for coding.
- solidsnack9000 9y ago
  It wouldn't surprise me if even Frama-C and SPARK have a "trust me" annotation.
  - nickpsecurity 9y ago
    Pretty much all languages w/ formal specifications do. The reason is that some specification claims are assumed/reasonable, proven outside the tool, or too hard to handle immediately. This can also be used as a maybe later. I'm not sure what theirs are.

dbaupp 9y ago

It would be great if it was, but it's also infeasible for a lot of code (at the moment anyway): it takes too much time and effort, and, in the FFI case, requires proving a whole external library correct too.