2 ms·

> Rust clearly does Until it exists at the kernel layer, the firmware layer, the runtime library layer, and the application layer, these issues still exist. CV

> Rust clearly does Until it exists at the kernel layer, the firmware layer, the runtime library layer, and the application layer, these issues still exist. CVEs come out weekly for memory errors in Linux, in firmware, in operating system libraries, and in application libraries. We need to think beyond rewriting code in one language or platform, and instead think about technologies that we can apply to all languages and platforms, including C and Rust. > I am saying that Rust clearly can get us further than we are right now. As can bounded model checking, without having to teach developers a new language with new idioms. > If there's something even more accessible, less verbose, and with not such a cobbled together Frankenstein async implementation... Indeed there is. Reach for the bounded model checker that works with your existing language or platform. Pour over the manual, and look at existing practical examples. If you like Rust, feel free to use it. But, if you prefer C/C++, Pascal, Ada, Python, C#, Java, or Modula2, that's fine. Either use an existing bounded model checker for that language or port CProver / GOTO to that platform. Rust developers ported CProver to Rust via Kani, because they also recognize that writing safer code can't be done by language alone. I don't think it's necessary to push people to use different languages or platforms to write safer code. They just need to use or port existing tooling and learn safer coding practices. If I come at firmware developers or old school OS developers with "we need to use Rust", the conversation is immediately shut down and I'm considered a fool. If, instead, I show them tooling that allows them to maintain their existing code base and make it safer, I get much further.

adgjlsfhk1 2y ago
bounded model checking is a new language with new idioms
- nanolith 2y ago
  Respectfully, that's a rather extraordinary claim. There are model checkers that use separate specification languages, but there are also model checkers embedded in the host language. CBMC translates C -- the same language -- to an SMT solver. A different target but the same language. It is true that new idioms will often be discovered along the way of converting existing C to pass the bounded model checker in every branch condition and in every case. However, software that is already relatively safe will require very little modification. I've seen it go both ways. Simpler code bases can pass model checks relatively unscathed. More complex code bases require refactoring to pass model checking. To my point, the code base can remain in C, and can be model checked gradually. It doesn't have to be ported to a different language or platform. But, it will require added assertions and some refactoring to make the execution of code more clear. It's still in C. The specifications are specified in C using regular assertions. The only thing that changes is that one will often use shadow methods -- still written in C but simpler than the functions they are shadowing -- in order to model check other functions. Other bounded model checkers like JBMC, Kani, or PolySpace work in similar ways.

adgjlsfhk1 2y ago

bounded model checking is a new language with new idioms

nanolith 2y ago
Respectfully, that's a rather extraordinary claim. There are model checkers that use separate specification languages, but there are also model checkers embedded in the host language. CBMC translates C -- the same language -- to an SMT solver. A different target but the same language. It is true that new idioms will often be discovered along the way of converting existing C to pass the bounded model checker in every branch condition and in every case. However, software that is already relatively safe will require very little modification. I've seen it go both ways. Simpler code bases can pass model checks relatively unscathed. More complex code bases require refactoring to pass model checking. To my point, the code base can remain in C, and can be model checked gradually. It doesn't have to be ported to a different language or platform. But, it will require added assertions and some refactoring to make the execution of code more clear. It's still in C. The specifications are specified in C using regular assertions. The only thing that changes is that one will often use shadow methods -- still written in C but simpler than the functions they are shadowing -- in order to model check other functions. Other bounded model checkers like JBMC, Kani, or PolySpace work in similar ways.