6 ms·

Note that you can write safe C code. seL4 is written in C! (And verified in Isabelle.) If that is too hard core, PolarSSL is a normal looking C code, which stil

Note that you can write safe C code. seL4 is written in C! (And verified in Isabelle.) If that is too hard core, PolarSSL is a normal looking C code, which still has been proved to lack any buffer overflow. https://trust-in-soft.com/polarssl-verification-kit/ https://trust-in-soft.com/polarssl-verification-kit/ has details. On the other hand, it probably is less effort to rewrite PolarSSL in Rust than doing that proof.

jabot 9y ago
I think the seL4 kernel rather proves that you can write safe haskell, verify it, and then transpile that to C. That's different from directly writing C...
- sanxiyn 9y ago
  Well, you aren't directly writing C anyway. Unless you are https://xkcd.com/378/ https://xkcd.com/378/ -- using tools is perfectly okay. Anyway, PolarSSL is definitely not transpiled. Its source language is C.
  - jabot 9y ago
    http://www.cvedetails.com/vulnerability-list/vendor_id-12001/product_id-22470/year-2015/opec-1/Polarssl-Polarssl.html http://www.cvedetails.com/vulnerability-list/vendor_id-12001... ... and your point is? EDIT: more recent bugs: https://tls.mbed.org/security https://tls.mbed.org/security These bugs include double-free and use-after-free - which are not covered by the original analysis, right?
- agumonkey 9y ago
  in the end the idea is that if you are semantic aware, then everything is safe; it's just operations from exp -> env -> store to env -> store etc etc
  - nine_k 9y ago
    Indeed! You can write safe programs for e.g. the original Turing Machine. But I bet you'll end up writing tools to make creating a safe program of any non-trivial size feasible. A large class of these tools is usually called "programming languages".
bsder 9y ago
So, where does this come in: http://www.securityweek.com/high-severity-vulnerability-found-polarssl-library http://www.securityweek.com/high-severity-vulnerability-foun...
- sanxiyn 9y ago
  Easy, it was out of scope. Quoting the report, "This report states the immunity of the PolarSSL software component to widespread CWEs, provided that PolarSSL is deployed in a context where... The server is configured as to never ask for client-side certificates". Quoting the news, "Servers that don't ask for client certificates are not impacted". TrustInSoft could prove that part of code too. There's nothing special about it. It's just that they didn't bother.
- huhtenberg 9y ago
  It doesn't. It's not a buffer overflow issue.
  - sanxiyn 9y ago
    It's an uninitialized read, and PolarSSL is actually also proven to lack uninitialized reads. It's just that asn1_get_sequence_of was not included in verification (as it is unreachable in verified configuration).
    - unscaled 9y ago
      Which shows you the limit of verification toolsets vs. a verifying compiler. To verify that the code is 100% free of uninitialized reads or uses-after-free the static analyzer would have to scan through all possible permutations. Sure, you can get very close to 100% in practice, but even if you're fine with this level of guarantee, the amount of discipline and cognitive overhead required for doing that in C makes Rust's learning seem like a piece of cake.
blub 9y ago
There are several safe dialects of C. The issue is that almost no one is using them and they're not about to start to either. A lot of infrastructure software has not been built with security in mind, but the game has changed, and this old C software is getting eviscerated. If one looks at the fixes for these buffer overflows in dnsmasq, no other conclusion can be drawn except that holes are plugged in a leaky sieve. This could work for software that's done, eventually. But if something's under maintenance, using plain C is security suicide.
- sanxiyn 9y ago
  I think PolarSSL showed it can be done with reasonable effort and it is not a suicide.
  - jabot 9y ago
    I would really like to see a comparison of the efforts of a) writing a program in a safe language like rust and b) writing the language in C and verifying it with a toolset like the one used by the polarssl guys. Given that the number of C projects that use similar toolsets is... low (?), I'd guess that said comparison would favor rust, but I'm prepared to be surprised :-)
  - blub 9y ago
    Correct me if I'm wrong, but is this Frama-C and ACSL? That doesn't look like plain C to me. In the ACSL manual in Example 2.10, does the programmer have to add the asserts? What if they make a mistake in the annotation?
duneroadrunner 9y ago
> On the other hand, it probably is less effort to rewrite PolarSSL in Rust than doing that proof. It's probably even less effort to convert to SaferCPlusPlus[1] (essentially a memory-safe subset of C++). There's even an tool[2] (under construction, but functional) to do a lot of the conversion for you. [1] shameless plug: https://github.com/duneroadrunner/SaferCPlusPlus https://github.com/duneroadrunner/SaferCPlusPlus [2] https://github.com/duneroadrunner/SaferCPlusPlus-AutoTranslation https://github.com/duneroadrunner/SaferCPlusPlus-AutoTransla...
- pcwalton 9y ago
  SaferCPlusPlus is not memory safe, according to your documentation. For one thing, the "this" pointer problem is pretty much unsolvable in C++.
  - duneroadrunner 9y ago
    > For one thing, the "this" pointer problem is pretty much unsolvable in C++. Well, you could just avoid/prohibit the explicit and implicit use of the "this" pointer. I.e. prohibit non-static member functions[1], right? [1] https://github.com/duneroadrunner/SaferCPlusPlus#practical-limitations https://github.com/duneroadrunner/SaferCPlusPlus#practical-l...
    - pcwalton 9y ago
      Does anyone actually want to program in "C++ with instance methods banned"? Why not just use a language designed for memory safety (which is most of them)? It's a whole lot easier, plus you get an ecosystem of actually safe code.
      - duneroadrunner 9y ago
        > Does anyone actually want to program in "C++ with instance methods banned"? Well, passing a "safe this" pointer as the first parameter to a (static) member function isn't that hard to get used to, is it? But I don't disagree with your gist. If memory-safety is your only concern and you're not trying to salvage an existing codebase, then Rust might be a better choice. But if you're trying to add memory safety to, say, an existing C implementation of SSL, the SaferCPlusPlus route would probably be less effort. Even when non-static member functions are banned. > (which is most of them) Personally, I consider RAII (deterministic destructors) an essential feature for safe, efficient programming at scale. That leaves only two choices, C++ and Rust, right? And if there's a memory-safe C++ option available, there are some arguments for choosing it over Rust.

jabot 9y ago

I think the seL4 kernel rather proves that you can write safe haskell, verify it, and then transpile that to C. That's different from directly writing C...

sanxiyn 9y ago
Well, you aren't directly writing C anyway. Unless you are https://xkcd.com/378/ https://xkcd.com/378/ -- using tools is perfectly okay. Anyway, PolarSSL is definitely not transpiled. Its source language is C.
- jabot 9y ago
  http://www.cvedetails.com/vulnerability-list/vendor_id-12001/product_id-22470/year-2015/opec-1/Polarssl-Polarssl.html http://www.cvedetails.com/vulnerability-list/vendor_id-12001... ... and your point is? EDIT: more recent bugs: https://tls.mbed.org/security https://tls.mbed.org/security These bugs include double-free and use-after-free - which are not covered by the original analysis, right?
agumonkey 9y ago
in the end the idea is that if you are semantic aware, then everything is safe; it's just operations from exp -> env -> store to env -> store etc etc
- nine_k 9y ago
  Indeed! You can write safe programs for e.g. the original Turing Machine. But I bet you'll end up writing tools to make creating a safe program of any non-trivial size feasible. A large class of these tools is usually called "programming languages".

bsder 9y ago

So, where does this come in: http://www.securityweek.com/high-severity-vulnerability-found-polarssl-library http://www.securityweek.com/high-severity-vulnerability-foun...

sanxiyn 9y ago
Easy, it was out of scope. Quoting the report, "This report states the immunity of the PolarSSL software component to widespread CWEs, provided that PolarSSL is deployed in a context where... The server is configured as to never ask for client-side certificates". Quoting the news, "Servers that don't ask for client certificates are not impacted". TrustInSoft could prove that part of code too. There's nothing special about it. It's just that they didn't bother.
huhtenberg 9y ago
It doesn't. It's not a buffer overflow issue.
- sanxiyn 9y ago
  It's an uninitialized read, and PolarSSL is actually also proven to lack uninitialized reads. It's just that asn1_get_sequence_of was not included in verification (as it is unreachable in verified configuration).
  - unscaled 9y ago
    Which shows you the limit of verification toolsets vs. a verifying compiler. To verify that the code is 100% free of uninitialized reads or uses-after-free the static analyzer would have to scan through all possible permutations. Sure, you can get very close to 100% in practice, but even if you're fine with this level of guarantee, the amount of discipline and cognitive overhead required for doing that in C makes Rust's learning seem like a piece of cake.

blub 9y ago

There are several safe dialects of C. The issue is that almost no one is using them and they're not about to start to either. A lot of infrastructure software has not been built with security in mind, but the game has changed, and this old C software is getting eviscerated. If one looks at the fixes for these buffer overflows in dnsmasq, no other conclusion can be drawn except that holes are plugged in a leaky sieve. This could work for software that's done, eventually. But if something's under maintenance, using plain C is security suicide.

sanxiyn 9y ago
I think PolarSSL showed it can be done with reasonable effort and it is not a suicide.
- jabot 9y ago
  I would really like to see a comparison of the efforts of a) writing a program in a safe language like rust and b) writing the language in C and verifying it with a toolset like the one used by the polarssl guys. Given that the number of C projects that use similar toolsets is... low (?), I'd guess that said comparison would favor rust, but I'm prepared to be surprised :-)
- blub 9y ago
  Correct me if I'm wrong, but is this Frama-C and ACSL? That doesn't look like plain C to me. In the ACSL manual in Example 2.10, does the programmer have to add the asserts? What if they make a mistake in the annotation?

duneroadrunner 9y ago

> On the other hand, it probably is less effort to rewrite PolarSSL in Rust than doing that proof. It's probably even less effort to convert to SaferCPlusPlus[1] (essentially a memory-safe subset of C++). There's even an tool[2] (under construction, but functional) to do a lot of the conversion for you. [1] shameless plug: https://github.com/duneroadrunner/SaferCPlusPlus https://github.com/duneroadrunner/SaferCPlusPlus [2] https://github.com/duneroadrunner/SaferCPlusPlus-AutoTranslation https://github.com/duneroadrunner/SaferCPlusPlus-AutoTransla...

pcwalton 9y ago
SaferCPlusPlus is not memory safe, according to your documentation. For one thing, the "this" pointer problem is pretty much unsolvable in C++.
- duneroadrunner 9y ago
  > For one thing, the "this" pointer problem is pretty much unsolvable in C++. Well, you could just avoid/prohibit the explicit and implicit use of the "this" pointer. I.e. prohibit non-static member functions[1], right? [1] https://github.com/duneroadrunner/SaferCPlusPlus#practical-limitations https://github.com/duneroadrunner/SaferCPlusPlus#practical-l...
  - pcwalton 9y ago
    Does anyone actually want to program in "C++ with instance methods banned"? Why not just use a language designed for memory safety (which is most of them)? It's a whole lot easier, plus you get an ecosystem of actually safe code.
    - duneroadrunner 9y ago
      > Does anyone actually want to program in "C++ with instance methods banned"? Well, passing a "safe this" pointer as the first parameter to a (static) member function isn't that hard to get used to, is it? But I don't disagree with your gist. If memory-safety is your only concern and you're not trying to salvage an existing codebase, then Rust might be a better choice. But if you're trying to add memory safety to, say, an existing C implementation of SSL, the SaferCPlusPlus route would probably be less effort. Even when non-static member functions are banned. > (which is most of them) Personally, I consider RAII (deterministic destructors) an essential feature for safe, efficient programming at scale. That leaves only two choices, C++ and Rust, right? And if there's a memory-safe C++ option available, there are some arguments for choosing it over Rust.