IncludeOS: C++ unikernel now free and open source • Hacker News Board

Re: IncludeOS: C++ unikernel now free and open source

#41

Post by cbsmith » Thu, Dec 03, 2015, 5:13 AM UTC

nickpsecurity wrote: post #39

cbsmith wrote: post #37

Earlier quoted context omitted.

> 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 t…

"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 th…

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

Re: IncludeOS: C++ unikernel now free and open source

#42

Post by nickpsecurity » Sun, Dec 06, 2015, 3:07 PM UTC

cbsmith wrote: post #41

nickpsecurity wrote: post #39

Earlier quoted context omitted.

"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 th…

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

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.

Re: IncludeOS: C++ unikernel now free and open source

#43

Post by nickpsecurity » Sun, Dec 06, 2015, 3:31 PM UTC

cbsmith wrote: post #40

nickpsecurity wrote: post #39

Earlier quoted context omitted.

"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 th…

> 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++ be…

"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.