Schneier on Security

ab praeceptis • May 19, 2017 8:30 PM

Thoth

Two quick remarks.

zephyr? Really? I don't trust the linux foundation any further than I can throw a T-72 tank.

As for security I personally like to go the route of using an STM32 as main proc. and an additional ti 430 basically for security plus funny useful services. While the ti 430fr2 and siblings have got security quite well I trust neither of the two and use them merely for my own way to do things (the triangle, see below).
Of course both can be cracked, particularly by a resourceful opponent but then I can't build my own chips and have to chose from what's available.

Here's what I basically do: I set the STM32 to rdp1 and/but treat it as untrusted device. I use the 430 as poor mans secure chip (which it does way better than the stm32), close it completely down so as to refuse anything and everything (incl. new bootcode) and have it to hold part 1 material of a 2 part algorithm (the second being on the stm32). Additionally all sensitive operations are 2 part, too. As a free throw in I (usually) use the analog circuitry for TRNG generation.

The third part of my triangle is algorithmic. Cracking either one of the chips gives you nothing but a probably bricked chip. Another nice feature of the 430s is the cap lines which enable cheap and simple - and fingerprint or temperature pattern free! - code input by a human. All of that for less than two $ is not to complain about.

Side note: Pretty much all major chip companies nowadays offer /usually expensive) "security chips". I don't trust them. About the only real added value they offer is even better tamper resistance but that isn't worth much to me because an opponent able to crack the chips in my triangle either in or very little below the league that also cracks "security chips". And with my own poor mans solution I *know* the implementation of the algorithms is a) solid and verified and b) not java crap.

ab praeceptis • May 19, 2017 10:01 PM

Thoth

As for zephyr I guess I'll have to agree. Sad situation.

As for "paranoia" solution, I was a fan of "security chips" for quite some time. What made me change my view was mainly two factors, namely a) java plus the need to trust, and b) all them funny protection measures are crackable in pretty every uni lab.

Which leads me back to a). How and why would I trust utterly profit driven corps to do it right rather than just adding "security" mumbo jumbo layers? From all I've seen, profit greed seems to be one of the arch-enemies of security. Them managers will invariably come down on the tech guys and demand what basically boils down to "listen, we don't need to sell security but the image of security which btw is also much more cost effective".
Plus keep in mind that them security chips are an extremely attractive target.

What I do see as an advantage is the "something I have" factor of a sim card. But that needed to be separate from the board and connected only when needed, e.g. at startup.

But then my use cases are different from yours. For your case which I losely summarize as "people, here's something that offers you some decent safety level. Stop entrusting sensitive stuff to your android or windows box!" I do agree with you.

Btw. I wish you success with your company and product! Your work deserves to be rewarded.

ab praeceptis • May 19, 2017 11:35 PM

Maybe let's encrap should have first tried "let's learn parsing urls".

ssl/tls and family - the plague that just never stops providing demonstrations of incompetence ...

(Yes, I'm waiting for someone smart to bring up the "commercial CAs are crappy, too!" 'argument'. As if sh*t-for-free were any tastier than sh*t-for-money)

ab praeceptis • May 20, 2017 1:26 AM

Thot

Maybe it's my strange mixture of stupidity and friendliness but I vaguely assumed that after quite some problems, usually introducing critical risks, with url/uri processing the happy members of the ssl/tls mental asylum might have woken up and started to work more carefully at least regarding things that had already bitten them multiple times ...

Obviously I was too optimistic, indeed.

ab praeceptis • May 21, 2017 11:13 PM

Thoth

From my point of view kotlin is just worthless crap on a large pile of jvm/java related crap that does not even deserve a place on the golden sticker holiday cards.

ab praeceptis • May 22, 2017 12:59 AM

Thoth, all

Indeed. Good that you warn them.

I'd like to add something. If for some reason you absolutely have to use linux - which I strongly advise against - do NOT use any linux with systemd!! A quick search will show you alternatives that are at least not systemd infested.

If you can avoid linux my advice depends on your level of knowledge and time to learn. If you can go the OpenBSD route then you should. If that is too tough for you there is still FreeBSD which is less security focussed than OpenBSD (but still much more secure, solid, and reliable than linux) and quite friendly. Also note that there is even a clickediclick version (I think it's called PC-BSD). Plus, FreeBSD runs most linux programs, too (although with thousands upon thousands of FreeBSD packages you will probably not need any linux stuff).

Again: If any possible avoid systemd infested linux (which is most distributions)!

ab praeceptis • May 22, 2017 1:55 AM

Clive Robinson

I contradict.

For one, the jvm is known to be particularly lousy.

More importantly, however, your argument is flawed in that it boils down to saying that making 1 element in a chain stronger is meaningless. This is grave insofar as it is one of the major common excuses to not care at all.

Looking logically the strength of the chain we're interested in is like with any chain defined by its weakest element - which usually happens to be the link between algorithm and, say, intermediary code.

True, with the way processors and compilers (with all their stages) work the a.m. link is certainly not the only one that is less than perfect; it is, however, usually by far the weakest one. Hence, language (a compiler) that makes it hard rather than easy to produce crap makes the whole chain stronger by a considerable factor.

Just compare the rather rare Eiffel or Ada f*ckups vs the very common C/C++/java f*ckups.

That said, you are right insofar as we certainly need to invest a whole lot more care and work in the other chain links. Happily this has at least begun as efforts in e.g. chip spec/design tools show (e.g. Chisel).

ab praeceptis • May 22, 2017 11:23 PM

mere mortal

You are welcome. It seems that my advice re. PC-BSD/TrueOs was bad as, so it seems, the "friendliness" has a high price in memory (Sorry, read about it but never used it myself). I can tell you, however, that I have practical experience with running FreeBSD in 128 MB or even less (no X). With or without X, no matter, FreeBSD will not need more memory than linux.

As you love "compartmentalization" (as you call it) you might find it interesting that FreeBSD not only has jails of fame but also it's own virtualization, "bhyve" with which I have made very good experiences. It might, however, not yet be the right thing for newbies. For them the good virtualbox support might be more attractive. Also note that virtualization seems to be one of the weak points of OpenBSD.

As for gui/desktop stuff I can't tell much because I'm utterly ignorant in that area and gladly use jwn. I know, however, that XFCE and other typical desktops are available out of the box with FreeBSD (plus there is quite a lot of guides, tutorials etc. for newbies).

ab praeceptis • May 23, 2017 12:19 AM

Nick P

"Datashield" - it's still more of a POC than something useable for production. Also note that for C they provide musl as "standard lib"; now, musl is certainly attractive but it's also rather exotic in terms of being certainly not in wide-spread use and.
Let me quote one paragraph from the paper:
As expected, without DataShield protection the client’s heap was corrupted, but with protection the attack caused a bounds violation and termination of the program.

Well, in many cases a dead server might be more desirable than a vulnerable running happily and ignorantly, but still, that's not really what a good solution looks like.

What I do like, though, is their pragma approach rather than the typical comment approach.

"Distributed System" - largely irrelevant but interesting. My personal advice would be to read it with the eyes of network software security people as the problems are often similar. A future version of cryptoverif, for example, might profit from it.

"ron pressler" - I even took the pain upon me to watch some minutes of his youtube musings. So I certainly demonstrated good will ...

Ron Pressler ... has been advocating methods such as TLA+ on the basis of formal verification being too ...

Uhzm, tla+ is for spec, not for code verif, ...

If true, it means mathematics isn't powerful enough to handle full correctness of large software no matter if we use modules, objects, etc to try to hide the complexity.

I do not see pressler in any position to credibly make statements like that (I try to avoid saying "bullsh*t!").

(also for the rest) Granted, I have not yet done really large projects with my current tool set but that doesn't even matter. And btw. all in all my productivity has not been lower but about the same or even somewhat higher than before working in, say, naked C (plus lots of experience). Simple reason: One must look at the *complete* dev. cycle - which in normal (e.g. C) development usually doesn't even end at GA because de facto the end users typically are doing the final beta test ...

As for the students hating a formal dev. approach, so what; they lack experience and, importantly, they are a product of rather poor education and the habits and views developped there. Looking properly at it one can't but notice that at some point in time one just has to properly spec, so why not doing it right in the first place?

ab praeceptis • May 23, 2017 7:33 PM

Gah

That's true in (a small) part and nonsensical or false in part. For a start, the author of the link is an OpenBSD guy and what he writes pretty much comes down to the old boring "FreeBSD is not OpenBSD!" allegation. I myself, btw, ripped apart one of the more influential/visible "OB is more secure than FB" "analysis and report".

In the end it boils down to "FreeBSD targets *all* users, incl. desktop users and hence *of course* comes with a different basic config than OpenBSD".

FreeBSD offers common virtualization, in particular Virtualbox (which one may consider as seriously imperfect but which happens to be very, very wide-spread and preferred by desktop users), it offers a linux compatibility layer, and many other things that make it much more and more conveniently usable than OpenBSD.

Both have by far more in common than they are different. They are pretty much one and the same thing, with one being targetting to be a secure BSD and the other one to be a friendly desktop BSD.

Is either of them a secure OS? NO, absolutely not. In fact, OpenBSD does not even meet my requirement for intermediate security, let alone the requirement for a secure OS (neither, of course, does FreeBSD).

So, if we use a scale from 0 (ridiculously crackable) to 10 (highly secure), so as to have a reasonable frame of reference rather than relying on fan boy blabla, android would be 0 to 1, windows would be 1 to 2 (the eal golden stickered windows being the 2), linux would be 1 to (rarely) 3, FreeBSD would be 4, OpenBSD 4.5, and some systems most of us have hardly ever heard would be in the 5 to 8 range. And yes, there is no 10 and not even a 9 due to diverse factors like (security wise) lousy hardware (e.g. intel amt), doubtful compilers, doubtful hypervisors, unverified tool(chains), etc.

Being a little more realistic and humble might be helpful.

As I said, none is secure and OpenBSD (ignore the evangelizing blabla) did not even strive to be(come) a secure OS. Their target was to be as safe and secure a BSD Unix as a BSD can be while FreeBSD targeted to be(come) a good quality general BSD with very good gui clicky clicky Joe and Jane usability. From my point of view both grosso modo achieved their goal and are continuing to getting closer. And both are reasonably secure within the frame of common OSs, in part btw. because they cooperate by far more than some X is better than Y sectarian want to make believe. We all profit from that exchange.

ab praeceptis • May 25, 2017 9:15 PM

Nick P, Clive Robinson, Thoth et al.

Today, after lots and lots of research and of work I dare to say that it's not all dark.

The 3 main reasons for my, albeit still modest, hope are the following:

- thanks to Snowden, Assange, Wikileaks and many others we have a changed situation. Sure, there are also factors working against us, the worst one being the smartphone swamp, and Joe and Jane are either blissfully or ignorant or helpless anyway. But generally the situation changed to the better, particularly because have begun to grow up (as I call it). There are more and more people who don't handle IT as the new wild west but who are beginning to understand how important safety and security are.

- More and more available and better hardware, particularly processors. While I like Risc-V it's not even about that specific processor but about having alternatives to x86 and arm and about better chip design and verification.
Unfortunately, the very chips we are supposed to trust most, namely "trusted stuff" like sim and hsm processors are badly tainted, even poisoned, by java but not all hope is lost; maybe sometimes soon companies like nxp or infineon wake up and offer alternative methods of (direct) access rather than having to go through a java crap layer.

- Lots of progress one the software side. Granted, most of it is not yet in a generally and widely usable state but we are on a good way.

Being at that let me report about some of my own experiences.

The task I chose (well the most current one besides my everyday professional work) was a high quality prng (I already hinted at that). The reason is simple: If I had to pick the one "lego" brick that makes or breaks encryption schemes I'd invariably end up looking at prngs. And I understand perfectly well why nsa chose to taint rc4 ...

One of the classical problems is that you can either have a fast prng or a good one, i.e. one that is very hard to predict. There is plenty more or less crappy but quite fast ones (e.g. the xorshift family) and there are quite some cs-prngs of high quality but those tend to be snail-slow (and btw. often do *not* have good random properties). Gladly though that's less bad than it seems because one could - and does - use csprngs to seed (and sometimes also to occasionally reseed) crappy but fast prngs. If there wasn't the problem that pretty all of the fast ones are so utterly crappy (predictable, biased, bad distribution, etc) that they are *very easily* predictable ("crackable").

The algorithm itself showed itself to be impeccable and even elegant (no, it's not mine) but the reference implementation (in C/C++, "of course") has diverse problems; some of them quite grave, most probably not so significant.

This is reporting about my work to implement it in sparked Ada. I myself spotted just 1 (grave) error in the ref. implementation, the rest was spotted by Ada, which I intentionally provoked by "stupidly" translating the C[++] ref. code as verbatim as possible. The kind of errors and problems I found was what I would consider typical for C[++]. Plus the whole thing was brutally lacking in elegance (don't underestimate that! Elegance is a quite reliable indicator of design quality).

So I started all new, based only on the algorithm and completely ignoring the ref. implementation. Result (after just a few days work, most of it thinking): Much more elegant (quite well matching the elegance of the algorithm) and almost no "red" (Gnats error marking).

But it gets better. The Ada compiler also grumbled at me when I had a variable that could be a constant and things like that. Excellent!

When I was all but done and running my test cases (in particular also testing for reference comformity) it soon blew up with a constraint error. It was code generated by Spark to runtime check a precondition. I mention this and find it interesting because it points at a very interesting spot, namely that the designer in me had formulated a precondition that was perfectly right but the programmer in me still had some bad old habits...
Side remark: Currently Spark brings quite many buts and ifs along and the kind of (very low level) code I was working on did not allow for static verification of some parts, so I had to have runtime checks created at least for the development version.

Another result that might be particularly interesting to many: My Ada code runs about as fast a C[++] code but I have to be fair and mention that that not the full truth. To achieve that result I needed quite some experience with Ada (e.g. trying to avoid implicit 2nd stack allocations) and with diverse tricks of the trade (e.g. when and what to inline). But then, the good result could be achieved and was achieved. That's an important message. Using Ada does *not* make your code slow.

All in all I feel confident enough to not just laugh at them if, say a nation state, asked me whether a trustworthy basic OS incl. the major libraries typically neeeded could be created with reasonably low resources and in a reasonable amount of time.

I'm gaining more and more confidence that we might escape into a safer future. But I also see that there is mountains of work before us. Nevertheless, medium gray is still much better than pitch black.

ab praeceptis • May 26, 2017 5:59 AM

Clive Robinson

Haha! Your description of the Victorian boiler makers, and wheelwrights pretty well match major parts of the software industry, too, it seems. "bodge it and cludge which boiled down to work it till it breaks then bolt on a cludge and work it again" puts it quite well, doesn't it.

"as you probably know crypto algorithms have issues when used as PRNGs." - oh yes, and how well I know that. On the other hand, what are we to do (other than using trngs which for some reason are rarely available on mainboards ...)? Them mersenne twisters, xor shifters and linear shifters have good random properties and speed (in good cases) but are utterly simply predictable. The cs-prngs are very hard to predict (well, that's their whole raison d'ètre) but bloody slow and/or plagues by poor random properties.

Funny that you mention state space, which is both an ugly maladie and rarely noticed. Surprising, it seems to me, looking at cache sizes and multithreading systems. In other words: Unless your state doesn't fit in one cache line chances are that you have an attack surface on your algorithms a**. Unless you desire a bad day I suggest to not look at widely used crypto ... (states spaces of kilobytes are quite common (as is memcmp and other bad sins)).

"ARC4" - Oh there are many who made that choice and it seemed not that bad then; nothing to be ashamed of. OpenBSD used it, too. Today we know better. Btw, the prng I've implemented has a state space that fits easily in a cache line and with some effort it fits even in the register set (which, of course, is very strongly desirable).

"prefering hard science graduates over CompSci graduatee" - Hmmm, my personal approach is to go with seasoned CS people but to have some mathematicians on the team, too. In bad cases I end up being the "joint" myself but I've had cases where a CS colleague (with strong math inclination) and a math colleague with solid CS experience/inclination did very well.
The reason for my approach is that we usually absolutely need a good link between the two and also the typically used tools must be "digestible" and produce digestible output, because in the end it ends up in the code. Which btw is another reason why I really love sparked Ada; it brings together the math and the code very comfortably (well, it's on a good way at least). But I get your point.

ab praeceptis • May 26, 2017 8:37 PM

Nick P

Actually I'm a little sad about C. Dross/Y. Moy doing what they are doing because while certainly meaning well they actually risk to add confusion. Let me explain:

That whole verification field is confusing enough and many do not fully understand it. As it also happens to be one of the few major tools in the rotten software world, it is of importance that it be well understood.

I'd feel a need to elaborate on two important points in that regard. And I'll begin with and use as a guiding light Dijkstras often forgotten but immensely important statement that code is the implementation of algorithm. This immediately leads us to my first point: What is code verification about? Answer: It is obviously about code, i.e. about the *implementation* of algorithms - *not* about algorithm verif.

What Dross/Moy demonstrate is understandable from a human point of view. Of course, having developed a powerful new tool, one wants to show its capabilities and to play with it. Quite probably another factor played a role, too, namely a very troublesome attitude mainly from across the ocean (something like "No need to properly think. Just do it. Shoot!").

And yes, Spark has grown to considerable power; one *can* do lots of amazing things with it, as (not only) Dross/Moy demonstrate.
However: That is *not* what code verification is about! It is *not* about algorithm verification!

As I said, the field is complex and we should certainly not mislead those who are just beginners in it. Similarly I can understand that it just seems practical to throw "all that verif stuff" together, particularly when a tool like Spark seems to be able to handle it.

No. We must discern and not cut corners. The question to be answered using Spark is a specific one. It is about the *implementation* - and nothing else. "Is my algorithm sound?" is a question to be looked at with other tools. Is my red-black tree design sound is not a question to be answered using Spark. Spark is about looking at the question "Is my *implementation* correct?"

2nd and related issue: code verification is *obviously* language dependant. Which also relates to your point of Spark looking at and maybe borrowing from Rust. Frankly, I think that that is largely nonsensical (albeit interesting and fun). Why? Simple: Rust has strong roots in the C family and, in fact, one very C-typical construct, namely pointers and the many related problems, has been a major, if not the reason for Rust in the first place. Most of those problems, however, simply do not exist in Ada.

Digging a little deeper one finds that the core problem is not even pointers but their utterly unaccounted willy nilly availability and arbitrary usability along with an utter lack of means to properly deal with them even if one wanted to; C (and family) simply don't offer any means. *That* is the problem, not even pointers per se. I know what I'm talking about; what I just said is the very reason why I looked at Frama-C (which I liked but which isn't powerful enough) and at separation logic tools.

Let us look at an algorithmically trivial problem, namely at a "hex printer", i.e. at code to "print" an unsigned, say 32 bit integer into a hex string. In C that would be something like a

void hexprint(char*buf, uint32_t num);

procedure hex_print(buf : String; num Unsigned_32);

Which leads me to next point: When I said that we must properly understand what we are examining/verifying I left away one decisive point: context - and that's what I'm actually testing above.
Code verification means two things, namely a) implementation (e.g. the procedure itself) and b) context (which includes the interface).

Remember the uni days when they drilled us to provide context, when they drilled us to e.g. specify domain and co-domain for a function? Same thing. hex_print, being code, i.e. meant to be run on real world hardware, is not supposed to work no matter what; it is supposed to provide a well specified service with a well specified context; that may be something simple a 'buf' existing and being at least of size 8 (or 9 in C) or it may be much more complex factors such a temporal or other conditions (like e.g. 'buf' being read or written to from/by another thread).

I agree that Rust has found an interesting and promising approach. However, Rust is only interesting under the premise that one wants to stay withing the C universe - which, frankly, doesn't sound like a smart proposition considering all the problems we have.

But there is good news, too. Gladly only (so my experienced guess) a quite small part of the rich C related problems universe is to do with complex problems. The vast majority are 1 off errors, loop errors, many kinds of buffer errors, etc.

I respect the good intention of the Rust people but as far as I'm concerned it's a lousy compromise. New code should use better languages in the first place and for the huge body of existing C/C++ code we'll need post factum analysers.

I had good reasons to stress in my "report" that Ada a) does not run significantly slower (and usually just as fast as C code) and b) doesn't make us less productive; in fact, if there is a difference at all than it's one to the good side.

That said, I personally chose Ada for many reasons but my intention is not to preach Ada. Eiffel, for example, might be an alternative for many, too. And even C can be acceptable, provided that microsoft doesn't somehow limit vcc to windows and dark-world licensing.

My advice for those who are interested in formal methods and proper software design would be to have a look at tla+ and at B. *Those* are meant to be used to verify ones design (as opposed to code).

ab praeceptis • May 27, 2017 7:24 PM

Nick P

For a start Yannick Moy != Ada(core). Y. Moy, who has a strong background in C/C++, with emphasis on safety and checking, is a senior engineer at adacore and mainly involved with Spark from what I know.

What he says about that intern is focussed on a certain quite specific problem where Rust like pointer may or may not be helpful.
Also kindly note that Ada's unchecked_deallocation is *not* something dangerous or evil (as it may sound); it's merely about deallocating a pointed to object expressly as wished by the programmer.

But the problem goes far deeper. We (safety oriented Ada people) have a "hierarchy" from desirable down to undesirable and pointers ('access types' in Ada lingo) are considered undesirable; sometimes necessary (e.g. at the OS interface) but undesirable. Another example is pointer arithmetic; it's available in Ada, too ("hidden away", of course) but you'll hardly get an Ada developer to use pointer arithmetic without seriously urgent need or a liberal dose of beating him.

On the other hand, people being people and existing software being what it is (e.g. OS or lib Interfaces) pointers are sometimes used, be it out of utter necessity or due to idiocy. It's *that* dark and sad corner Y. Moy is talking about and not about Ada somehow throwing away all its beauty only to follow the Rust creed.

Moreover keep in mind that Moy is mostly about checking, Spark, proving, etc. So, his statement is *not* "Rust does it better. We'll switch" but rather something to the effect of "Rust pointers are attractive for *checking* and bookkeeping. We should look at that".

There are - like everywhere - of course different factions within the Ada community, one of which is the lenient one with e.g. Moy (maybe to a degree also driven by business interests); I myself belong to the other faction, the one that says "Let them die. More often than not pointers are evil and if used at all, that should be left to only the experienced wise masters. If a grasshopper uses them and dies that's just natural selection and a solved problem".

Which brings us to the next point. Sorry if I'm blunt (my english isn't good enough to put it elegantly) but I don't trust or care a rats rear about Rust. Simple reason: To me "open source community" translates pretty directly to "bunch of idiots". Of course, there are usually some bright or even brilliant individuals involved, too, but "democracy", "equality", bla bla etc, quite commonly and reliably is but a recipee for disaster.

"It also eliminates need for separation logic like VCC uses for temporal safety since it does same thing *without any verification effort*."

To me that simply translates to "I don't care. Let them play, I have work to do". Verification is no burden, it's a gift from heaven.
And btw, even if Rust really had solved the pointer problems (which I doubt until I see rigorous proof) so what? There is still plenty enough crap in their C heritage rucksack. And let's not forget the ugly fact that mozilla not only gave us Rust but they also gave us the browser cancer which is their main product as well as the javascript plague. I won't touch anything from mozilla with a pole.

ab praeceptis • May 27, 2017 10:48 PM

Nick P

Y. Moy is a bright and capable man but again: he is not Ada or adacorp. He is not even Spark. That is not meant in any way against Y. Moy but rather to put your story into a frame. What you call "quite a bit of corroboration" still is far away from "Ada/Spark will use Rusts pointers". Also Y. Moy didn't admit anything; he merely mentioned something that is, btw, *not* high up on adacorps ToDo list. Putting an intern at something usually translates to something like "is probably worth a closer look and some experimenting".

You also consistently fail to see the importance of language. This is not some game where one collects safety items and strives to have the best ones. Ada simply has BY FAR less need for safe pointers than C family languages.

One point that immediately struck me was the clear hint at something that tells a lot about the Ada people and reminds of the difference between professionals doing something vs. some amateurs playing around: Math at Inria and a strong desire to have it properly formally verified, both the design and the resulting code.

"In Ada, they can't without garbage collection" - uhm, garbage collection is optional and many Ada compilers don't have it (and I certainly don't miss it). More importantly, though, that demonstrates once more that you might want to pick up on my multiple strong hints about language specificity. That whole garbage collection mindset comes from a certain background, often C and family, but is of far lesser importance for other languages. So, for Rust GC might be seriously attractive but many Ada compilers do not even plan to work on it; it's simply an unimportant gadget.

"The concepts of maximizing potential and ROI means you want to create as many great things as possible with as little effort as possible." - Uhum. And what is "great things"? Unless "great things" means crap (like most code we have that was driven by profit greed and incompetence), if it means at least halfway decent quality we are back at formal methods and languages like Ada oder Eiffel, etc.

And I'm back at my "report" where I - with good reason - mentioned that TDC (total development cost) with Ada is *not* higher than with C and family. This is even way more true if we include maintenance.

So what are you arguing here? That we should throw millions of more hours and billions of more $ at the C family in the hope that one day in the year 2700 it might be able to deliver "great things" of halfway decent quality with not too much effort - say, like what we can do today even with Object Pascal (not even to mention Ada)?

"Forcing long, hard work in separation logic like Microsoft tried to do in Hyper-V is terrible compared to how quickly Redox team threw together a whole OS with same safety guarantees on heaps just using Rust's borrow-checker. Same benefits with fraction of knowledge or work = better solution."

Theory and improper, too. For a start the "long, hard work in separation logic" of microsoft lead to *provably safe* code. I've yet to see that for redox. Moreover you are comparing apples and horses, namely early research work of microsoft vs. much later work (btw quite probably profitting from microsofts earlier work). Furthermore Rust's borrow-checker solves 1 (in words: one) problem only, albeit a major one while microsofts work solves whole problem classes and offers formal verification.

And again: I did concrete work, I solved concrete problems in C, Frama-C, verifast (sep logic) and in sparked Ada. I have concrete experience with concrete work. And the result is that working in Ada is about as fast as in C and much, much more efficient and faster than ACSL annotated C plus Frama-C checking (which btw. is a pita even just to set up) or sep-logic annotated and checked.

That is a tremendously important result because it means that we can build "many great things ... with as little effort as possible." or, more concretely with about the same effort - but with hugely higher quality!

"Rust's temporal safety" - ... is mostly a misnaming. Yes, temporal aspects may play a role under certain circumstances but the thing you are talking about is mostly memory safety. As for temporal safety there is much more needed than merely pointer safety. And btw. Ada offers a lot in that regard since a long time (I'd love to talk about Eiffel, too, but a) my experience with Eiffel is quite limited and b) multitasking of any kind is quite new there).

As we are on a security blog, let me mention an example that is of importance in crypto protocol verification, namely the temporal pi calculus implication, i.e. a statement like "event A implies that there was event B before" which btw can also be transformed for what you meant, i.e. memory safety with multiple tasks -> "event 'grab token' or 'change bit' implies that there was an event 'release token' before".

All in all, yes, Rust probably is better suited than C to create less buggy software but as soon as we talk real safety we can't but talk formal verification, too.

Closing, I have a maybe interesting tip for you: as you like to dig into papers and concepts, you might enjoy a deeper look into the Pony language; you'll even find something similar to Rust's approach plus an amazing evolution towards quite well done and blazingly fast actors.