[cbsmith]

> C runtimes do add extra issues but that's not relevant to my comment.

I really don't see how it is. If you're running on a desktop platform, you've got a huge exposed surface that is working with raw pointers to proprietary logic. That makes provable correctness a far, far more complex problem.

> I said I largely came up dry on methods to prove correctness of C++ code.

It is easy to implement a smart pointer that the compiler can prove will always do bounds checking before dereferencing. The hard part is proving that all the code that uses raw pointers is doing the same thing.

[nickpsecurity]

"I really don't see how it is. If you're running on a desktop platform, you've got a huge exposed surface that is working with raw pointers to proprietary logic. That makes provable correctness a far, far more complex problem."

The point is that C++ itself is damn-near impossible to analyze on the cheap and without much false positives. That's before I even considered the C interface. Then there's C level problems that have been the reason I've opposed it forever. At least there's tons of stuff to draw on in analysing, transforming, etc that code. I'd go with a C subset or Java/Ada subset with high-integrity runtime any day over C++.

"It is easy to implement a smart pointer that the compiler can prove will always do bounds checking before dereferencing. The hard part is proving that all the code that uses raw pointers is doing the same thing."

I'll take your word on the smart pointers doing bounds-checks as I'm not up-to-date on all the techniques of C++ developers. Academics need to do a fresh take on that with assessments vs particular risks & compared to current languages. Meanwhile, most in safety-critical development that I know of don't use C++ because it's too complex and unsafe per them. I know there's MISRA subset and some other stuff. There are people who use it with thorough testing and source-to-object validation. Mostly not in use, though.

So, do you have any resources showing that C++ code is safe and analysable if one just uses smart pointers? And what tools and subset you use to do that? If you have that and proof it works, then that could help a lot of developers using C that aren't aware of it. I'm being serious as much as I am challenging your claim. If you have it, I'll consider it.

[cbsmith]

> I'll take your word on the smart pointers doing bounds-checks as I'm not up-to-date on all the techniques of C++ developers. Academics need to do a fresh take on that with assessments vs particular risks & compared to current languages.

That's kind of already happened. Stroustrup has done a whole ton of work in that area with Concepts.

> Meanwhile, most in safety-critical development that I know of don't use C++ because it's too complex and unsafe per them.

It turns out that provable correctness invariably involves a fair bit of complexity (you are basically compiling a mathematical proof). People use Haskell and Coq to really do it right, and --surprise-- those turn out to be hard for programmers to learn.

A lot of other, more popular, high level languages are actually terrible for provable correctness, even if they are better for proving memory safety. C++ isn't as effective for the job, but it has the advantage of being great for integrating in with the platform. It is a trade off, but one that is well worth while.

> So, do you have any resources showing that C++ code is safe and analysable if one just uses smart pointers?

This stuff goes back a way, but stemmed from Modern C++ Design. There is a whole world of policy based design where you use the type system (much as with Haskell and Coq) to enforce declarative policies.

The quick thought experiment would be something like this:

    template <class T>
    struct SafeRef {
        void check() { ... }
        operator T&() { check(); return *x; }
        operator const T&() const { check(); return *x; }
    private:
        T* x;
    };

You can override operator-> to make it behave more like a proper pointer. CRTP gives you some pretty powerful ways of getting the job done too.

[nickpsecurity]

"That's kind of already happened. Stroustrup has done a whole ton of work in that area with Concepts."

Wasn't aware of that. It was an interesting read. Thanks for mentioning it.

"It turns out that provable correctness invariably involves a fair bit of complexity"

I wasn't even talking about that. I just looked for static analysis tools that could reliably find common implementation flaws or interface issues with little to no false positives. These already exist for C, Java, Ada, C#, and academic languages. Similarly, some verification or foundation of standard library like Modula-3's or the one for C. I found little to nothing of any of this for C++. So, the C++ verifications would all be visual and manual unless you pay big $$$ for one of few commercial tools.

Unacceptable. Formal methods would make C++ unacceptable for even more reasons.

"This stuff goes back a way, but stemmed from Modern C++ Design."

Same book pjmp recommended. Guess the study should start with it.

"You can override operator-> to make it behave more like a proper pointer. CRTP gives you some pretty powerful ways of getting the job done too."

Interesting example. I think one test of C++'s safety would be whether such methods can provide same protections that Ada provides where applicable to both languages:

http://www.adacore.com/knowledge/technical-papers/safe-secur...

It would need to catch the problems, do it during compile phase, and do it fast enough to be productive. I heard bad things about C++ compile phase in the past, esp for template heavy code. Plus, needs design-by-contract as Eiffel and SPARK have shown. I've seen it done with asserts and object constructors/destructors so that's probably not a problem. The other stuff, esp static analysis for memory & concurrency safety, is where C++ will be judged most.

[cbsmith]

...and just to provide an example of how one does verification with for C: https://galois.com/blog/2013/09/high-assurance-base64/

[nickpsecurity]

I just did it Orange Book B3/A1 style by visual, result, and trace-based correspondence between code and executable specifications. Plus lots of FSM's. Next project I'd add Frama-C and Astree for code-level verification. Plus, CompCert for compilation with more result & trace-based simulation for correspondence.

Good to see new work, though. I follow Galois' stuff a lot because they're very innovative and practical. Harden et al are also using LLVM simulations for correctness but with ACL2.