4 ms·

I don’t understand this at all. MISRA C, model checkers and theorem provers all exist to provide some of these guarantees that are, to my knowledge, widely reco

I don’t understand this at all. MISRA C, model checkers and theorem provers all exist to provide some of these guarantees that are, to my knowledge, widely recognized in applications where “safety” actually entails life safety. F* is a very modern tool, I think, developed for precisely these use cases. I’m not aware that the rust compiler is proven or even specified. Avoiding its mechanisms for validating use-once memory isn’t even that uncommon, especially in low-level library code. That Google is the man behind the curtain here also comes off as weird since they have not, to my knowledge, standardized their own critical infrastructure on Rust.

fsociety 5y ago
MISRA C is just a standard and developing a codebase in it can still result in memory safety issues. Rust has the guarantees built into the compiler, so if it compiles you have a reasonable standard of memory safety.
- grumblenum 5y ago
  You would have to sanitize your entire dependency tree for unsafe invocations and also demonstrate that valid rust programs do, in fact, guarantee memory safety, which might be invalidated by previous or future compiler versions. That also ignores known soundness holes, compiler errors, and silliness like how rust binaries leak the file structure they were built on. I don’t see why that’s reasonable, but auto industry standards are not reasonable or a language with a garbage collector is not reasonable. The work happening in model checking is really incredible. Project Everest is focused on addressing exactly the same problems, and I don’t think the rust compilers guarantees have undergone nearly the rigor of that of F*.
  - Ericson2314 5y ago
    > language with a garbage collector That is reasonable. Rust is not the only safe option. Re everything else....Rust should be seen as the beginning not the end. All those model checking and other "post-hoc" analyses come with major productivity pitfalls. (Wrestling with some solver that may or may not be happy for spooky reasons is profoundly disheartening compared to wrestling with something elegant and compositional like a type system. Just as there is the ML family of languages and then SML with CakeML, Rust should continue being a fast-moving target where the occasional mistake might happen, but there is academic work revolving around the language which should create a CompCert/CakeML with time. Some aviation/auto software regulation is a legit, but frankly a some of it doubles as regularity ossification the industry secretly like as it creates a mote around existing businesses that have "evolved" compliance from the get-go. In that case, unproductivity is a feature, not a bug. I would not hold it up as a realistic model for these sorts of projects to aspire to. Without drastic changes to the way we found unprofitable FOSS foundation infrastructure, whenever productivity and security are at odds, the former will win over the latter.
    - grumblenum 5y ago
      Using a mode checker on existing software is unproductive, but rewriting existing, working software that you have to shoehorn into a shape rustc (which had a miscompilation bug until 1.52.1, has no specifications or alternative implementations, right?) will compile is productive? Rust’s type system is elegant, but Agda, OCaml F#, F* and Haskell, which are in a whole different league of sophistication, are not? Furthermore, I’m not aware of any progress in “sealed rust” or “rust belt” other than raising grant money. I don’t think a certification is coming anytime soon. There are other verified compilers that could be used now, though. This argument sounds like rust for rust’s sake.
      - Ericson2314 5y ago
        > Using a mode checker on existing software is unproductive, but rewriting existing, working software that you have to shoehorn into a shape rustc .... will compile is productive? The rewrite is a 1-time cost. > Rust’s type system is elegant, but Agda, OCaml F#, F* and Haskell, which are in a whole different league of sophistication, are not? I am primarily a Haskell user, and I already said I have nothing against GC. Those other languages (except for F#) are great! > has no specifications or alternative implementations That is a major downside (I work on GHC and wish it wasn't the only game in town) and affects all of those. That's why I put out SML and the CakeML implementation. SML lacks shiny new stuff but the grunt work has been done. I would certainly use SML over any variant of C for anything that needs dynamic allocation.
      - steveklabnik 5y ago
        > which had a miscompilation bug until 1.52.1, All compilers have miscompilation bugs. Even ones that are proven correct. > has no specifications or alternative implementations, right? There is one alternative implementation that is good enough to bitwise reproduce rustc, there are a few other in-progress alternate implementations. > I’m not aware of any progress in “sealed rust” or “rust belt” That doesn't mean they haven't progressed. By the way, "Sealed Rust" is now called "Ferrocene" and is expected to GA in late 2022. https://ferrous-systems.com/ferrocene/ https://ferrous-systems.com/ferrocene/ > There are other verified compilers that could be used now, though. This is true, for sure. A compiler being verified is not a panacea.
  - the_why_of_y 5y ago
    Firstly, for any of the 4 projects that have been announced by Prossimo so far, a garbage collected language would be unsuitable as it would be rejected by almost all current users of the respective projects. Given that, as you correctly point out there are still lots of options that could be used; for example, Ada/SPARK has been around and freely available via GNAT for a long time. For example, here is a DNS server implemented in Ada/SPARK: http://ironsides.martincarlisle.com/ http://ironsides.martincarlisle.com/ Latest download is 5 years old - can you find a single instance of IRONSIDES running in the wild? IMHO the main advantage that Rust has over other approaches that would technically work to create sufficiently secure software is that it has much lower barriers to entry and a much larger community - the hardest part of getting a technology adopted is marketing, and Rust is currently the only option that can compete with C/C++ here. There is already some promising work on formalizing the semantics of Rust, see for example https://plv.mpi-sws.org/rustbelt/popl18/ https://plv.mpi-sws.org/rustbelt/popl18/ and https://people.mpi-sws.org/~jung/phd/thesis-screen.pdf https://people.mpi-sws.org/~jung/phd/thesis-screen.pdf
  - fsociety 5y ago
    > That also ignores known soundness holes, compiler errors, and silliness like how rust binaries leak the file structure they were built on All these issues I've encountered, or heard of, while working on MISRA-compliant code which is expected to run in cars for years without updates. We make do with C, and extensive tests + ASAN/UBSAN/TSAN can take us a long way, but my point is that Rust is a nice incremental step compared to C. I'm not excluding F* from the list of nice incremental steps, and if the developer ecosystem is there maybe that is a compelling option. My other point is that MISRA C helps enforce standards in some of the nasty codebases that run in cars, and trust me they can be scary, but it is only a band-aid and I believe that Rust is generations ahead of it. > but auto industry standards are not reasonable or a language with a garbage collector is not reasonable. We avoided garbage collection because the run-time is harder to predict, and at the same time Java/Android is used a lot in the infotainment units which are now also running some safety-critical code - with a back-up computer thank you standards - and it makes it harder to allocate resources on the embedded system accordingly. I will admit I'm all for Rust and will likely try to seek out jobs which I get to use it in.
tialaramex 5y ago
> MISRA C, model checkers and theorem provers all exist to provide some of these guarantees that are, to my knowledge, widely recognized in applications where “safety” actually entails life safety. So, where do I get the version of curl or similar that in fact provides "some of these guarantees" ? Because ISRG isn't spending money on developing software for the Ford Bronco or US aircraft carriers, it is spending money on curl. MISRA C like a long list of other projects for C or C++ including Bjarne's "Core Guidelines", goes like this: 1. Classify things people will end up needing to do as sinful. 2. Offer them a mechanism to obtain an indulgence, knowing this mechanism will quickly be exhausted. 3. When inevitably this results in tragedy point back at item (1) which absolves you of responsibility. Example #1, MISRA says you mustn't have any unreachable code. Of course deciding whether code is actually reachable requires solving the Halting Problem, so your automated tooling doesn't do that and will either just flag code that might or might not really be unreachable (useless noise that reduces development velocity) or ignore MIRSA here and just leave your programmers to try not to do this, the status quo ante. MISRA often needs to dish out "permits" to violate their guidelines because, in practice, the guidelines are too strict to be usable and somebody's workplace requires the guidelines so... the alternative is incredibly creaky and likely unsafe code that's "compliant" - or a "permit" to just ignore a guideline. This is most common when the language doesn't provide a sane way to do something. Example #2, MISRA forbids hiding variables. If the inner scope has a variable named 'counter' and so does the outer scope, programmers are likely to get confused and mean one when the other is actually in scope, the language compiler won't stop this. But MISRA has to issue a permit because C macros routinely do this and so if your static analysis tool looks at the code it sees lots of such re-use that was (hopefully) harmless. But if you have hygienic macros (Rust declarative macros) then this isn't a problem, the hygienic macro can't accidentally shadow variables. So you don't need these acrobatics in Rust, if you want to ban shadowing, you can do that and not have weird knock-on effects in macros. Example #3 MISRA forbids invariants from appearing as conditionals. MISRA reasons that you couldn't possibly have meant to check that buffer != NULL because you know you set buffer in the constructor, and so this is a coding error. But of course you wrote that because you're worried that a bug elsewhere might null out the buffer and blow up the whole system... So now your static analysis tool is screaming that your defensive coding violate MISRA. Do you go ask the Boss for authority to ignore this rule? Or do you rip out the defensive checks? Tools like F* and WUFFS are different because they've intentionally set their sights low. If you say you want to write the software for your Jet Fighter in WUFFS its authors will carefully explain that this can't be done, and they don't want to help you try. They solve small, well-specified problems in a constrained problem space. They do it very well, you should use them when they're appropriate. They can't be used to replace curl.

fsociety 5y ago

MISRA C is just a standard and developing a codebase in it can still result in memory safety issues. Rust has the guarantees built into the compiler, so if it compiles you have a reasonable standard of memory safety.

grumblenum 5y ago
You would have to sanitize your entire dependency tree for unsafe invocations and also demonstrate that valid rust programs do, in fact, guarantee memory safety, which might be invalidated by previous or future compiler versions. That also ignores known soundness holes, compiler errors, and silliness like how rust binaries leak the file structure they were built on. I don’t see why that’s reasonable, but auto industry standards are not reasonable or a language with a garbage collector is not reasonable. The work happening in model checking is really incredible. Project Everest is focused on addressing exactly the same problems, and I don’t think the rust compilers guarantees have undergone nearly the rigor of that of F*.
- Ericson2314 5y ago
  > language with a garbage collector That is reasonable. Rust is not the only safe option. Re everything else....Rust should be seen as the beginning not the end. All those model checking and other "post-hoc" analyses come with major productivity pitfalls. (Wrestling with some solver that may or may not be happy for spooky reasons is profoundly disheartening compared to wrestling with something elegant and compositional like a type system. Just as there is the ML family of languages and then SML with CakeML, Rust should continue being a fast-moving target where the occasional mistake might happen, but there is academic work revolving around the language which should create a CompCert/CakeML with time. Some aviation/auto software regulation is a legit, but frankly a some of it doubles as regularity ossification the industry secretly like as it creates a mote around existing businesses that have "evolved" compliance from the get-go. In that case, unproductivity is a feature, not a bug. I would not hold it up as a realistic model for these sorts of projects to aspire to. Without drastic changes to the way we found unprofitable FOSS foundation infrastructure, whenever productivity and security are at odds, the former will win over the latter.
  - grumblenum 5y ago
    Using a mode checker on existing software is unproductive, but rewriting existing, working software that you have to shoehorn into a shape rustc (which had a miscompilation bug until 1.52.1, has no specifications or alternative implementations, right?) will compile is productive? Rust’s type system is elegant, but Agda, OCaml F#, F* and Haskell, which are in a whole different league of sophistication, are not? Furthermore, I’m not aware of any progress in “sealed rust” or “rust belt” other than raising grant money. I don’t think a certification is coming anytime soon. There are other verified compilers that could be used now, though. This argument sounds like rust for rust’s sake.
    - Ericson2314 5y ago
      > Using a mode checker on existing software is unproductive, but rewriting existing, working software that you have to shoehorn into a shape rustc .... will compile is productive? The rewrite is a 1-time cost. > Rust’s type system is elegant, but Agda, OCaml F#, F* and Haskell, which are in a whole different league of sophistication, are not? I am primarily a Haskell user, and I already said I have nothing against GC. Those other languages (except for F#) are great! > has no specifications or alternative implementations That is a major downside (I work on GHC and wish it wasn't the only game in town) and affects all of those. That's why I put out SML and the CakeML implementation. SML lacks shiny new stuff but the grunt work has been done. I would certainly use SML over any variant of C for anything that needs dynamic allocation.
    - steveklabnik 5y ago
      > which had a miscompilation bug until 1.52.1, All compilers have miscompilation bugs. Even ones that are proven correct. > has no specifications or alternative implementations, right? There is one alternative implementation that is good enough to bitwise reproduce rustc, there are a few other in-progress alternate implementations. > I’m not aware of any progress in “sealed rust” or “rust belt” That doesn't mean they haven't progressed. By the way, "Sealed Rust" is now called "Ferrocene" and is expected to GA in late 2022. https://ferrous-systems.com/ferrocene/ https://ferrous-systems.com/ferrocene/ > There are other verified compilers that could be used now, though. This is true, for sure. A compiler being verified is not a panacea.
- the_why_of_y 5y ago
  Firstly, for any of the 4 projects that have been announced by Prossimo so far, a garbage collected language would be unsuitable as it would be rejected by almost all current users of the respective projects. Given that, as you correctly point out there are still lots of options that could be used; for example, Ada/SPARK has been around and freely available via GNAT for a long time. For example, here is a DNS server implemented in Ada/SPARK: http://ironsides.martincarlisle.com/ http://ironsides.martincarlisle.com/ Latest download is 5 years old - can you find a single instance of IRONSIDES running in the wild? IMHO the main advantage that Rust has over other approaches that would technically work to create sufficiently secure software is that it has much lower barriers to entry and a much larger community - the hardest part of getting a technology adopted is marketing, and Rust is currently the only option that can compete with C/C++ here. There is already some promising work on formalizing the semantics of Rust, see for example https://plv.mpi-sws.org/rustbelt/popl18/ https://plv.mpi-sws.org/rustbelt/popl18/ and https://people.mpi-sws.org/~jung/phd/thesis-screen.pdf https://people.mpi-sws.org/~jung/phd/thesis-screen.pdf
- fsociety 5y ago
  > That also ignores known soundness holes, compiler errors, and silliness like how rust binaries leak the file structure they were built on All these issues I've encountered, or heard of, while working on MISRA-compliant code which is expected to run in cars for years without updates. We make do with C, and extensive tests + ASAN/UBSAN/TSAN can take us a long way, but my point is that Rust is a nice incremental step compared to C. I'm not excluding F* from the list of nice incremental steps, and if the developer ecosystem is there maybe that is a compelling option. My other point is that MISRA C helps enforce standards in some of the nasty codebases that run in cars, and trust me they can be scary, but it is only a band-aid and I believe that Rust is generations ahead of it. > but auto industry standards are not reasonable or a language with a garbage collector is not reasonable. We avoided garbage collection because the run-time is harder to predict, and at the same time Java/Android is used a lot in the infotainment units which are now also running some safety-critical code - with a back-up computer thank you standards - and it makes it harder to allocate resources on the embedded system accordingly. I will admit I'm all for Rust and will likely try to seek out jobs which I get to use it in.

tialaramex 5y ago

> MISRA C, model checkers and theorem provers all exist to provide some of these guarantees that are, to my knowledge, widely recognized in applications where “safety” actually entails life safety. So, where do I get the version of curl or similar that in fact provides "some of these guarantees" ? Because ISRG isn't spending money on developing software for the Ford Bronco or US aircraft carriers, it is spending money on curl. MISRA C like a long list of other projects for C or C++ including Bjarne's "Core Guidelines", goes like this: 1. Classify things people will end up needing to do as sinful. 2. Offer them a mechanism to obtain an indulgence, knowing this mechanism will quickly be exhausted. 3. When inevitably this results in tragedy point back at item (1) which absolves you of responsibility. Example #1, MISRA says you mustn't have any unreachable code. Of course deciding whether code is actually reachable requires solving the Halting Problem, so your automated tooling doesn't do that and will either just flag code that might or might not really be unreachable (useless noise that reduces development velocity) or ignore MIRSA here and just leave your programmers to try not to do this, the status quo ante. MISRA often needs to dish out "permits" to violate their guidelines because, in practice, the guidelines are too strict to be usable and somebody's workplace requires the guidelines so... the alternative is incredibly creaky and likely unsafe code that's "compliant" - or a "permit" to just ignore a guideline. This is most common when the language doesn't provide a sane way to do something. Example #2, MISRA forbids hiding variables. If the inner scope has a variable named 'counter' and so does the outer scope, programmers are likely to get confused and mean one when the other is actually in scope, the language compiler won't stop this. But MISRA has to issue a permit because C macros routinely do this and so if your static analysis tool looks at the code it sees lots of such re-use that was (hopefully) harmless. But if you have hygienic macros (Rust declarative macros) then this isn't a problem, the hygienic macro can't accidentally shadow variables. So you don't need these acrobatics in Rust, if you want to ban shadowing, you can do that and not have weird knock-on effects in macros. Example #3 MISRA forbids invariants from appearing as conditionals. MISRA reasons that you couldn't possibly have meant to check that buffer != NULL because you know you set buffer in the constructor, and so this is a coding error. But of course you wrote that because you're worried that a bug elsewhere might null out the buffer and blow up the whole system... So now your static analysis tool is screaming that your defensive coding violate MISRA. Do you go ask the Boss for authority to ignore this rule? Or do you rip out the defensive checks? Tools like F* and WUFFS are different because they've intentionally set their sights low. If you say you want to write the software for your Jet Fighter in WUFFS its authors will carefully explain that this can't be done, and they don't want to help you try. They solve small, well-specified problems in a constrained problem space. They do it very well, you should use them when they're appropriate. They can't be used to replace curl.