Hacker News new | past | comments | ask | show | jobs | submit login

This isn't type safe though, namely this part:

   aPerson = list_entry(node, struct Person, list);
while the templated way is.



I'm not sure why that's problematic. It's a simple 1-liner that can be audited manually and reused arbitrarily. If you add it up, the TCB is actually less than relying on the complex template elaborator.


That’s the thing - it has to be audited manually. I’m sure I won’t convince you here of the value of static typing but some people think it is.


I'm a big static typing fan. That's not particularly relevant to this security consideration though, the TCB is the biggest factor. The C++ compiler and toolchain are a far larger TCB than the C toolchain and this one liner. As long as this reuse problem isn't a persistent pattern in a kernel, then the unsafety is less of a problem than introducing the larger TCB.


Sorry, I’m not familiar with what a TCB is, and google isn’t being helpful. do you have a link I could read?


People make mistakes, even with simple one liners. Type checkers don't. Running the compiler is also a lot cheaper than having someone inspect every line of code carefully.


> Type checkers don't.

Sure they do, unless your type checker is formally verified. Are you suggesting there exists a formally verified C++ compiler?

> Running the compiler is also a lot cheaper than having someone inspect every line of code carefully.

Except that's not what I suggested. You only need to audit lines that perform potentially undefined behaviour. The C type checker ensures the rest are fine. I think it's clear this problem is worse in C++ given all of the additional abstractions that interact in surprising ways.

Furthermore, C++ has no formal verification tools, so if you wanted real guarantees, you'd use something like Frama-C or a theorem prover like they did with seL4. Microkernels in C++ have been tried, and in every case they switched back to C for very good reasons.


Are you suggesting that the error rate of type checkers, verified or not, is even in the same ballpark as the error rate of human reviewers?

If I care so much about system correctness that I do the insane amount of work that is formal verification (just look at how many man years sel4 consumed!), I don't write C or C++ at all, I use Spark. There is a reason why you can count the number of formally verified kernels on the fingers of one hand, and it's not because everybody tries to use C++ instead of C.


> Are you suggesting that the error rate of type checkers, verified or not, is even in the same ballpark as the error rate of human reviewers?

Nope, but your unqualified statement was simply false, and in any case, your point isn't really relevant. This single line of code we're discussing is easily verifiable by manual inspection and automated testing. We're not talking about huge swaths of code here, we're talking about a few unsafe primitives, because this kind of reuse isn't typical of a microkernel.

The type safety of a single operation expressed as a template is relatively insignificant compared to the added complexity of C++, particularly considering the "reuse" benefits are non-existent for microkernels, and if all you're left with is some elusive "type safety" for a linked list, that's simply not enough.

This is obvious when you know the history of multiple C++ kernel verification efforts, all of which failed, no matter how simple of a C++ subset was chosen. Many C verification efforts have succeeded, and tools for lightweight formal methods, like Frama-C, make the transition to verification possible with C. C++ is a dead end for this purpose, and the various L4 groups that created L4 kernels in C++ and then rewrote them in C all agree.




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: