Linux Kernel Use-After-Free Remote Code Execution Vulnerability | Hacker News Reader

Linux Kernel Use-After-Free Remote Code Execution Vulnerability

securityfocus.com

97 pointsDiabloD3116 comments

What happened to make this updated? This was patched in March upstream, and it appears it made it into an Android patch release a couple of days ago.

[1] http://git.kernel.org/cgit/linux/kernel/git/torvalds/linux.g...

[2] https://source.android.com/security/bulletin/2016-10-01.html

https://source.android.com/security/bulletin/2016-10-01.html...

Better URL that goes right to the appropriate section.

It was fixed, but not (publicly) recognized as a security issue, so likely not backported + updated by distros in "stable" channels.

No. Stop it. I don't want to hear that we should be re-writing all of our systems code in Rust, or that Oberon and the Wirth family should have won, or that C is crap, and Linux should die, and be re-written, or that this wouldn't have happened if we had all just adopted the Lisp Machine.

We've all heard it already, we all know what you'll say. So skip the smug post, and go do something productive. Like writing a really cool piece of new code, or fixing a use-after-free, or posting something more insightful, or inventing a new type of shoelace that doesn't come untied until you want it to.

Instead of fixing a particular use-after-free, how about making use-after-free impossible?

> Instead of fixing a particular use-after-free, how about making use-after-free impossible?

Yes ..

Does this vulnerability work only on a particular architecture?

The bug is architecture independent, although a particular exploit may work only on a specific architecture.

At what cost to performance? Very rarely are there solutions that exist without tradeoffs.

Many verification systems can understand virtually any proof you can throw at them, so any memory management scheme for which you have a rigorous argument for correctness should be able to operate with no additional runtime overhead. And if you don't have such an argument, you've already lost no matter what language you use.

The main cost to performance is related to multicore proofs. It is an open question on how to work out complete proofs of multithreaded operations.

This is why seL4 does not support internal SMP. You can run an instance per core and assign it a separate memory space like to a VM though.

Great. Instead of telling us, most of whom already know, about it, go do it.

There are no unicorn solutions, however being religously blind to potential net value of fallible but potentially better interoperable alternatives would be irrational. Any rewrite cannot likely be accomplished in one pass (without some really smart code transpiler), but would more likely occur on a gradual migration todo list with a bidirectional interoperable language. The evaluation of such languages would likely involve requesting necessary features such as freestanding compilation, performance profiling/tracing tools and debugger integration, proofs of correctness and GC-less operation, among others. It's not impossible but it would need to be demonstrated that the perceived immense cost is significantly offset by the perceived immense value over "doing things as they've always been done."

And it definitely could be done in one pass because bugs like this do exist, and the language we want to port to should prevent them.

The smug replies on this comment seem to be the ones saying "Don't tell me about Rust".

So, then, why do you think that "We need to rewrite everything in Rust" isn't doing something productive? I've been a C++ and C developer for a long time and have been waiting for some safer language that lets me do what I've been doing in those languages. Knowing that Rust was a realistic option was what inspired me to learn it and write new things in it. If that happens at scale, that's how we actually get things written in a memory-safe language.

> So, then, why do you think that "We need to rewrite everything in Rust" isn't doing something productive?

The Linux kernel didn't get written because people on a forum said "we need to write a complete open source reimplementation of the UNIX kernel," but because Torvalds just went ahead and wrote it. Most things in F/OSS work that way.

GNU had a whole manifesto, though. https://www.gnu.org/gnu/manifesto.en.html (Although, yes, a signifiant body of software existed when the manifesto was published.)

Linus Benedict Torvalds 8/25/91

Hello everybody out there using minix -

I'm doing a (free) operating system (just a hobby, won't be big and professional like gnu) for 386(486) AT clones. This has been brewing since april, and is starting to get ready.

https://groups.google.com/forum/#!msg/comp.os.minix/dlNtH7RR...

I imagine the project is big enough now that anyone who would undertake it would want to be compensated for it. And since that is unlikely to ever pass the cost/benefit ratio for any given corporation, it's unlikely to happen. Not to mention the potential for alienating of the entire existing kernel development group.

It would be much easier to submit patches to slowly upgrade the kernel to a memory safe language, but that would require a lot of political savvy to push through, also making it an unlikely path to be taken. Ultimately, you'd have to convince Linus of the merits, and we all know how much he likes complex languages.

If it hasn't happened already, with another of the dozens of memory safe languages (like ada) which have been on the market for dozens of years, another memory safe language coming (like Rust) along won't change that.

Why do you think that? Or, put another way, why specifically do you think it didn't happen with previous memory-safe languages?

For one, Rust is a different language from the other memory-safe languages that have existed in the past, and in fact incorporates a lot of research in programming languages that didn't exist when Ada was designed. But even if that weren't true, one thing that's changed since the past is we now are slowly understanding how difficult it is to write secure software in C, and how important it is to write secure software. When Unix was first designed we (the entire programming community) didn't know about a lot of security issues, and the lack of Internet meant that it was less important to defend against them. It is probably much more worth rewriting our tools in Ada today than it was ten or twenty or thirty years ago.

> Or, put another way, why specifically do you think it didn't happen with previous memory-safe languages?

IMO, because it's harder to break the rules. Sometimes the rules just need to be broken. There was a recent article about someone attempting to interface with OpenGL in Rust a month or so ago, and it discussed how they ended up giving up, since the things they needed to do didn't mesh well with how Rust expected programs to be written. If interfacing with a driver is so hard, how will interfacing with hardware be easier?

Programming for hardware requires a lot of breaking and bending the rules. How can being memory safe help when you're creating memory spaces as most software knows of it?

Performance is King, low memory overhead is Queen. Even rust can't take those thrones away from C. Not yet, at least. Perhaps not ever (I expect that C++ would have done it, were it possible for a language with the complexity of Rust).

  >  If interfacing with a driver is so hard, how will interfacing with
  > hardware be easier?

It really depends. The key is to identify the proper ways to make the abstraction as safe as possible. This is a fairly new skill, in a new language. Said post was good, and the author has been using Rust for a long time, but one person failing to do so doesn't mean that it's impossible.

I'm still a noob at this kind of thing myself, but I recently wrote a (tiny) driver for a memory-mapped device. My first iteration had tons of unsafe code. My second iteration had three lines of unsafe code. My latest iteration has zero unsafe code, though you do need one call to an unsafe function outside of it in order to construct it. (to create a slice from the raw memory location that's mapped.)

That is, of course, pretty much the simplest possible case. But I believe the pattern will hold, over time, as people learn how to do it.

  > Even rust can't take those thrones away from C.

Rust is faster than C on some microbenchmarks. We'll see what the future holds.

"The revolution will not be televised".

The beginning of the end of use-after-free, buffer overflows, stack smashers, et al will be when we as a community finally accept that C is a terrible language, impossible for ordinary humans to reason about, and must be abandoned. Only when we begin to accept that truth will we all get serious about moving away from it.

For many years the response has been that "C is fine" or some variant of "humans will be better programmers in the future" both of which are demonstrably false.

No one questions the wisdom of paramtaraizing SQL. No one questions the wisdom of not writing your own crypto. Yet despite the mountains of evidence, wasting billions (yes BILLIONS) of man-hours and dollars, and even lives lost there is still resistance to the idea that C needs to die ASAP.

So as long as there are posts like yours our job of educating and persuading isn't finished and that's extremely important if we have a hope of actually making this desperately needed change.

If you still doubt let me go ahead and make a prediction: before the end of the year there will be another RCE exploit in the Linux kernel discovered and a different one will be written, code-reviewed, and committed but not discovered until later (but within 5 years). I'm happy to put $1,000 on this wager.

Actually, it is still possible to use C as a higher than assembly target language for compilers.

While I'm really interested in this for making languages available everywhere (tm), basic things like signed integer overflow being undefined behavior make me question is C is fit for purpose even here.

Since you are generating the C code, you can generate the appropriate checks where needed to avoid such undefined behavior too.

Which is the one thing keeping it in the running.

The problem is this line of reasoning doesn't generally hold up when applied to C codebases (because in practice statistics catches up with you eventually) and C code generators, in effect, happen to contain an admittedly small but rather obfuscated C codebase.

Moreover, you must always include such checks - manually crashing on e.g. null pointers even if you'd be entirely satisfied with a segfault - just to avoid the optimizer potentially going apeshit on your code. Which can have... poor effects on program performance.

If you are writing a code generator, it all depends on the source language. If, for example, your source language doesn't have NULL pointers, then you don't have to waste cycles checking them in C.

Indeed. That's what Nim and Rust (for instance) can do to ease porting to other platforms. Even safety critical applications can be written in C by using tools like FramaC.

https://frama-c.com

I've got no problem admitting that C isn't good enough in most cases, and should probably die. I know that's true. I'm just sick of the annoyingly smug comments about it that pop up like mushrooms on HN. If you're posting here, you're more often than not preaching to the choir.

>The beginning of the end of use-after-free, buffer overflows, stack smashers, et al will be when we as a community finally accept that C is a terrible language, impossible for ordinary humans to reason about, and must be abandoned.

1) All the complaints you have apply equally well to assembly language, yet assembly language is all that the CPU understands. Somebody always has to deal with the low level complexity of writing the foundational software constructs necessary to build safe environments and C is still the most natural mapping to varied assembly languages that we have.

2) Nothing else will fit for many embedded systems. Your choices are C or assembly language. What safe environment/language are you going to fit into a microcontroller with 1kB of RAM?

(And, yes, maybe Rust or one of the other proposed system language replacements will be better than C someday, but that someday isn't today.)

> All the complaints you have apply equally well to assembly language, yet assembly language is all that the CPU understands.

No, machine code is all that the CPU understands. Assembly language is source code that gets converted into machine code by an assembler.

Well that's the thing about C and its ilk; it is an endless wellspring of awful failures and so the voices you are trying to shout down have an unlimited supply of ammo. This will keep happening and you're going to keep hearing about it and the arguments for alternatives will continue to strengthen. That's the reality to which you need to adapt, if you're a reasonable person.

The advocates of these alternatives aren't creating this situation. The unavoidable fact is that our traditional tools have a propensity to propagate bugs that are fabulously difficult to discover. That's one of the lessons of nearly a half century of C. New tools are emerging that solve this problem and their advocates have every reason to say so.

Another lesson C teaches us through its popularity and longevity is that performance will always be critical for systems code; there will never be a day when we can squander cycles and RAM on garbage collectors and reference counts and indirections and all the other bookkeeping and abstractions inherent to so many languages that have utterly failed to displace C for systems programming.

I don't know what the future looks like. Maybe it's Rust. Maybe Linus will get fed up and invent a better language in 4 days. Maybe someone will create an AI system that can spot this sort of bug before it ever gets checked in. All I know for sure is that the current situation is intolerable and yelling at people to shut up about it won't work.

I don't know about that - very little software is written in C these days. Even parts of the Windows and Mac kernels are written in at least C++ and Microsoft had an entire OS written in C# internally. Meanwhile the games industry has been C++ since forever (which still isn't great but better than C) and most business and web software is written in GCd languages.

BTW the kernel is full of reference counts.

> BTW the kernel is full of reference counts.

I think the OP is pointing to languages like Swift/Objective-C where reference counts are used even if you don't really need them, not that ever reference counting anything is a lazy abstraction.

I'm fine with admitting C had flaws. It does need to be replaced for many projects. It's just the smug comments on HN that irritate me, especially because most of us are already in agreement (including me, now), and those who aren't won't be convinced by the sheer power of smugness. In short, I'm not complaining because the people who do this sort of thing are wrong, but because they're not actually helping.

Hence why I support projects done in Go, even if I dislike the design decisions regarding its type system.

Every program written in Go is one program less written in C.

Fair enough.

Hey, you know how to get rid of the smug comments, including this one?

...

Make sure there's less C code around.

Unfortunately, when you get rid of C code, comments don't get deleted.

Now now, some C code is commented.

All right, I'll admit it, I laughed out loud when I heard this. Maybe it's because of my all-too-fresh experiences trying to decipher undocumented C as a newbie (which I still am). It almost makes this thread worth it.

This is a discussion forum, of course you're going to find talking rather than doing here.

Once there's a firm consensus that it's time to move away from C we'll probably stop talking about it. But that consensus has to develop through discussion and argument here and elsewhere (and if you look at the conversations now compared to a year or two ago, I'd say we've made a lot of progress). If you don't believe there's value in talking about technical issues then what are you even doing here?

I guess GP is refering to repetitiveness of same arguments.

A tree thread is good for discovery but not so good for reaching a conclusion/consensus. Flat/linear thread should be used instead.

There's actually a pretty solid consensus here. I'm the only one I've seen arguing about C, and even I agree that it should be moved away from with these sorts of codebases. It's the rest of the world which doesn't have a consensus.

You're welcome to post, of course. I'd just rather you not. There's no sense preaching to the choir.

I'll add to this. Before you can even begin championing your language for kernel development, make sure it can compile to all of the same architectures that C can. Make sure that programs written in your language are as space and time efficient as the equivalent C programs. These are things you can do today, if you feel strongly enough about this cause.

Once your language is at that point, then start building up your arguments to convince Linus and the majority of the core kernel developers that your language is the right choice for continued development.

Until these occur, it's all just pointless speculation.

> to convince Linus and the majority of the core kernel developers

The biggest cost is not them, it's every other C programmer, every other company, the whole industry. It's unrealistic to even think that any significant part of them is going to invest resources into another language just to gain memory safety.

I figure, if you're capable of coming up with an argument which convinces Linus to move away from C, you can use that logic to convince anybody (who is capable of being convinced by logic in the first place).

Here's my attempt at a constructive idea, inspired by all the preemptive C comments:

The l-k devs and the big commercial Linux vendors/users (Google, IBM, Red Hat, Amazon etc) should gang up and start offering big bounties for these. And simultaenously start doing subsystem rewrites in a memory-safe way prioritized by bugs found by bounty program (and other ways). If they're allergic to non-C languages, a safe C subset like SAFEcode or C0 could be used[1].

[1] I'm saying it's possible to have a memory safe C subset with current compiler technology, even though you can point out something missing from C0

Google already pays bounty for a lot of FOSS projects.

And if the bugs you find can be exploited in google products the bounty is _very_ high.

What circumstances are needed for this to be exploitable? Wondering if iptables could mitigate for systems where upgrading the kernel is non-trivial.

Haven't looked at this too closely, but iptables are unlikely to help. The bug appears to be in the recvmmsg() syscall, which is where the packet leaves the kernel and enters the userspace. The syscall itself is not that widely used, only for some unusually optimized UDP servers, you are unlikely to have one running. But you can check with strace just to be sure.

Yep. Though I assume this needs some interesting network traffic to trigger it.

https://codesearch.debian.net/search?q=[^_]recvmmsg\%28[^\%2...

(Many of the results are for code like language runtimes and debugging tools that don't actually use recvmmsg() themselves)

Ouch, it's in chromium though.

I wrote a bit about it: https://blog.lizzie.io/notes-about-cve-2016-7117.html

tl;dr looks like it'd function well a local privilege exploit. not an expert, but as a remote exploit think it would need 1) a service running recvmmsg (which is kind of unlikely) 2) a way to cause recvmsg to error, and 3) a way to cause the service to close its socket in the middle of the recvmmsg call.

Nice writeup!

I was just starting to look into this since people were claiming it was pretty severe and yet I hadn't seen any POC's. Have you made any more progress?

For whatever my opinion is worth (i.e. not much), I would agree with you that remote exploitation of this particular bug would be really difficult.

Website seems to be down. For those that are curious, it's CVE-2016-7117.

Mitre link: https://cve.mitre.org/cgi-bin/cvename.cgi?name=CVE-2016-7117

The commit for the fix is more interesting.

https://git.kernel.org/cgit/linux/kernel/git/torvalds/linux....

At the moment, the link you posted says "This candidate has been reserved by an organization or individual that will use it when announcing a new security problem."

I guess the post on securityfocus (also not reachable) slipped out before end of embargo time?

Isn't the Linux kernel tested with a zeroing storage allocator?

Yes (actually, a poisoning allocator which is the moral equivalent).

This bug was found because a KASAN ( https://www.kernel.org/doc/Documentation/kasan.txt ) assertion triggered during fuzzing.

This functionality appears to have been introduced in linux 2.6.33 with commit a2e272554 .

Looking at http://vault.centos.org/6.8/updates/Source/SPackages/kernel-... it looks like RedHat backported this function but has not applied the fix.

I don't get it, if this was fixed in March, which systems are compromised by this?

Do I need to worry about a fully upgraded ubuntu 14.04 with or without the Hardware Enablement Stack?

Due to the way Linux people handle security fixes, a lot of the time the code fix goes in at first, then people decide it's an exploitable vulnerability, and then they have an embargo period without public discussion so everyone[1] can release a security patch at the same time. So hopefully Ubuntu has a kernel update ready to be released and they will send it out just about now.

Unfortunately in this case Ubuntu's CVE tracker just shows "needs-triage" or "does not exist" for CVE-2016-7117.

[1] Well, most Linux systems don't get timely security patches, like most Android phones or most embedded/iot products, but you get the idea

for those wondering, Debian is mostly not vulnerable, except for the oldstable/LTS release:

https://security-tracker.debian.org/tracker/CVE-2016-7117

It seems that Linux distros are now releasing fixes:

- Debian is prevalently not vulnerable: https://security-tracker.debian.org/tracker/CVE-2016-7117 (except the "oldstable" release)

- for Ubuntu, the situation is more complicated, as it depends on the actual kernel package installed: https://people.canonical.com/~ubuntu-security/cve/2016/CVE-2... For the "linux" kernel package (prob the most common), the situation looks like this at the moment::

        Upstream:	released (4.6~rc1)
        Ubuntu 12.04 LTS (Precise Pangolin):	needed
        Ubuntu 14.04 LTS (Trusty Tahr):	released (3.13.0-86.130)
        Ubuntu Touch 15.04:	DNE
        Ubuntu Core 15.04:	pending (3.19.0-59.65)
        Ubuntu 16.04 LTS (Xenial Xerus):	released (4.4.0-22.39)
        Ubuntu 16.10 (Yakkety Yak):	not-affected (4.4.0-22.39)

- for CentOS/RHEL, my understanding is that fixed kernels have not yet been released: https://bugzilla.redhat.com/show_bug.cgi?id=CVE-2016-7117

Just wait until torvalds wrote a new language. Publish it and made it as a new standard. Again.

So what can one do about this? What amount of panic is appropriate?

Delpoyed boxes: ksplice / kpatch or run updates when available.

And consider mitigations at various tech stack layers.

I haven't found a way to patch a kernel with nontrivial modules without kernel restart. This makes the mechanism only useful to reduce system reboot times after a patch.

EDIT: do not panic as much, nvm, this is in `recvmmsg` not `recvmsg`, which is not used by much software. Definitely not sshd or nginx. I can't find any software I have installed that does.

I think the best advice is not to listen to anyone on HN about this shit except for cperciva

Original response:

----

Reimage everything from scratch if you're a bit paranoid, because in theory someone could have rooted every server running any internet-accessible thing (even just sshd or nginx)

Realistically, update ASAP and figure out from other sources how difficult this is to exploit and how likely it is that anyone actually did get a working RCE

Obligatory comment so nobody else has to: C is a terrible language for security and we must abandon it immediately. Anyone that uses it has clearly not heard of Go/Rust/Haskell. We should just abandon the Linux kernel and start from scratch. And we can unit test the shit out of it to avoid security vulnerabilities. Hasn't Heartbleed taught us anything? MongoDB is web scale. Ron Paul 2012.

The sarcasm is strong with this one...

In fairness I haven't seen anyone make a serious comment like yours yet in this thread.

"in b4 'we should rewrite W in X/Y/Z'" has become the new "we should rewrite W in X/Y/Z".

I didnt up/down vote, but rewriting in something like a performant, secure subset of Go/Rust/X and formally-proving correctness to remove many classes of errors would arguably have immense net value greater than the pain and cost of progressive/gradual rewriting migration from C to something with fewer dangerous corners and far less code to accomplish the same system behavior.

I don't mean to show support for either the "rewrite everything in X/Y/Z" crowd or the "C is all we need forever" crowd (or their non-straw-man equivalents). I just thought the early state of the comments in this thread was funny, is all.

kernel security and later mongodb appearing randomly in a comment is like priesthood and pedophilia randomly associated. It stings of irony.

The defensive tone of this comment is unseemly. C is just a tool, and I assure you, one that feels nothing for you.

I love me some C. Some of the funniest projects I have worked on have been written in C. My comment was sarcastic.

You should have mentioned the official plan of a complete rewrite as a microkernel in message-passing dialect of Visual Basic, which was supposed to land in version 3.0.

https://lkml.org/lkml/2005/3/2/247

oldmanjay did realise that ...

Go, unlikely. It's safer but it has other problems. Haskell is great but it's runtime makes it hard (though not impossible) to use in kernel development.

Rust and ATS seem to be pretty well suited. With Rust getting more and more traction, maybe not all is lost :)

I have extremely hard time believing there can be a viable OS kernel project on Haskell. I mean, yeah, you probably can write OS kernel in Haskell, if you are determined enough. But I don't believe you can make it into a viable project. Rust - maybe, if you can get enough mindshare. Which is also a big if so far...

I think Rust has the mindshare, what it needs is people actually doing it.

Redox is a ground up OS, but I wonder if we shouldn't instead be taking more of an Oxidization approach where we rewrite more and more pieces of an existing OS in Rust piecemeal. This would add some overhead (programmatically not instructionwise) of a lot of context switches though between the C and the Rust code, which is to say it would be a little ugly for a while.

It might be cleaner to go after a microkernel to do this though, like L4 or rumprun.

MkLinux was a popular environment on a portal I worked for in the late 90s. We brought dozens of Macs back into active duty as secondary workstations for the operations team.

> I think Rust has the mindshare, what it needs is people actually doing it.

That's kind of the opposite of having the mindshare, IMO :) Having the mindshare means people would be reaching for it when they need things done, not have to be dragged in, and there's a wide pool of people knowing it.

I'm pretty sure you can write OS kernel in almost any language that can be compiled into runnable code, and probably if you are really determined also in those that are compiled into bytecode. As I said, it's not the main issue.

Unless you are a titan of programming that can do an OS project all by yourself, or have more money than Google, you'll need random people to come to the project, pick up pieces and work on them. The question is, does Rust have pool of people wide enough so that probability of people wanting to work on your project is higher than your needs?

C definitely has a huge pool. So do C++, Java, JS, Python and many other languages. Rust? I'm not sure it does so far. Maybe I'm wrong.

Remember, Rust is just a year old. There are already a few OS projects going in it. All the languages you mentioned are >10 years old.

I think for its age, the success it already enjoys is impressive.

I would then say that it has momentum, not mindshare.

It's not a criticism of the qualities of Rust. It's just an assessment of the current state of affairs. Maybe Rust will gain the mindshare in 3 years. We'll see. I personally think having something better than C but as ubiquitous and supported as C would be awesome. Is it Rust? We'll see in 5 years.

If you plan on writing your OS in Haskell in the usual sense (i.e. your OS executes pure Haskell functions and interprets some sort of IO monad) you're going to end up implementing a full microkernel in another language just to get started. Not to mention it'll be a microkernel with a GC.

The only way I could see a kernel being truly written in Haskell is in a DSL something like atom[1]. Atom is an EDSL represents code that not only doesn't need a garbage collector, but also has a verified constant bound on memory usage. However if that's what you're looking for, you might as well go with an EDSL in a dependently typed language like Idris to make verification easier and extensible.

[1]: https://hackage.haskell.org/package/atom

> I mean, yeah, you probably can write OS kernel in Haskell, if you are determined enough.

Some of my colleagues did, a few years ago.

http://jfla.inria.fr/2007/actes/Presentation/tolmach.pdf

In fact, SEL4 has parts in Haskell. The important things are all in Isabelle though and everything is compiled to C and machine code.

I played around with getting a Rust kernel module to work before. And I eventually got a "hello world" in my dmesg. But what I realized in so doing was that seemingly 90% of the higher level features of Rust were lost to my module -- essentially I got the language memory security features (borrowing and ownership) but with very little standard library help, which made the whole endeavour seem much less practical still than just using C and libc (because I would have to reimplement a lot of that functionality in Rust -- Kernel Rust, if you will).

I think if the Rust communtiy wants to make it somehow to the Linux (or other UNIX or windows) Kernel space, there needs to be an effort to build Kernel Rust, if there isn't one already..

well, you can't use libc for a kernel module either :)

No, but there's 'kernel C' (not an actual/official name) with a large reproduction of much of libc ready for use there. printk() is a good example which actually has a format string implementation (https://www.kernel.org/doc/Documentation/printk-formats.txt)

right, that shouldn't be hard to map to rust I guess

When were you doing this? There's now a large chunk of the standard library[1] that's explicitly designed to be used in bare-metal/zero-dependency situations, and it even includes "fancy" things like the formatting infrastructure[2] (it has to be hooked up to a writable/IO device, but that's just a trait implementation away) and string processing, certainly more than the zero-allocation subset of libc.

[1]: https://doc.rust-lang.org/core/

[2]: https://doc.rust-lang.org/core/fmt/

It has been at least 6 months and it's possible I just missed this! That's quite cool. Thanks! I will give this a try.

Why does ATS not get more traction in discussions like this? That's what it's made for. This is the only mention so far in this comment page.

Not enough publicity, to my mind.

Rust is popular because Mozilla, a well-known company, is developing it for a well-known major project, a web browser.

Go is well-known due to Google, and the fact that many people with an opinion-setting power know who Rob Pike is.

Haskell, well, just spent 20 years being around, sometimes in university curricula.

ATS is only, it seems, known to people who are specifically interested in formally-correct low-level code, on the sparsely-populated intersection of math and hardware geekery.

Seriously, two things: formal verification of correctness is sorely needed and a language platform which has complete, bidirectional C interoperability in targeting both kernel- and user-land which can be gradually migrated to one compilation unit a time and has much more safety, is more succinct, has C feature parity and no/minimal runtime performance hit would be requirements for candidates to change languages, but only after impressing Linus, lieutenants and contributors of undeniable value.